Constructive Calibration of the Fontaine-Mazur Conjecture: Lean 4 Formalization (Paper 47)

Title: Constructive Calibration of the Fontaine-Mazur Conjecture: Lean 4 Formalization (Paper 47) Description: Lean 4 + Mathlib formalization of the constructive reverse mathematics (CRM) calibration of the Fontaine-Mazur Conjecture (Paper 47 in the CRM series). The five conditions of Fontaine-Mazur — unramified, de Rham, geometric origin, trace rationality, and polarization — stratify across the omniscience hierarchy: FM1 (Unramified) is equivalent to LPO over Qₚ via encoding pattern. FM2 (de Rham) is equivalent to LPO over Qₚ via 1x1 matrix encoding. FM3 (Geometric origin) is BISH — Faltings comparison + rational skeleton restore decidability. FM4 (Traces): geometric traces decidable (BISH), abstract traces require LPO. FM5 (Polarization): p-adic u-invariant blocks Hermitian forms in dim ≥ 3. The archive contains the complete Lean 4 bundle (7 source files, ~1016 lines, 26 custom axioms, 0 sorry), the LaTeX source, and compiled PDF. Build: lake build → 0 errors, 0 warnings, 1774 jobs. Requires Lean 4. 29. 0-rc1 and Mathlib.