The Event Horizon as a Logical Boundary: Schwarzschild Interior Geodesic Incompleteness and LPO in Lean 4

We formalize in Lean 4 a decomposition of Schwarzschild interior physics into constructive content layers. The explicit cycloid geodesic r(eta) = M(1 + cos eta) reaches r = 0 at proper time tau* = pi*M constructively; the Kretschmann scalar K = 48M^2/r^6 is constructively computable for any r > 0; and for any epsilon > 0, there exists an explicit eta with r(eta) < epsilon. All of this is BISH (Height 0). The abstract principle that every bounded monotone decreasing sequence in [0, 2M) converges to a definite real limit -- the completed-limit formulation of geodesic incompleteness -- is equivalent to the Limited Principle of Omniscience (LPO). The event horizon at r = 2M thus demarcates not only the causal boundary from which light cannot escape, but a logical boundary: the exterior geometry (Paper 1) and the interior's finite-time physics are BISH, while the singularity assertion as a completed-limit principle requires exactly LPO. The formalization comprises 1,021 lines across 8 modules with zero sorry statements. One interface assumption (bmc_of_lpo, the Bridges-Vita equivalence imported from Paper 8) is axiomatized with citation. The Classical.choice in the axiom profile arises from Mathlib infrastructure; the constructive calibration is established by proof-content analysis (see Paper 10). Paper 13 in the Constructive Reverse Mathematics Series. Includes complete Lean 4 source code, precompiled PDF (15 pages), and build instructions. Other papers in the Constructive Reverse Mathematics Series (see Zenodo for current files): Paper 1: WithdrawnPaper 2: Bidual gap and WLPO — DOI: 10.5281/zenodo.17107493Paper 3: WithdrawnPaper 4: Quantum spectra axiom calibration — DOI: 10.5281/zenodo.17059483Paper 5: Schwarzschild curvature verification — DOI: 10.5281/zenodo.18489703Paper 6: Heisenberg uncertainty (v2, CRM over Mathlib) — DOI: 10.5281/zenodo.18519836Paper 7: Physical bidual gap, trace-class operators — DOI: 10.5281/zenodo.18527559Paper 8: 1D Ising model and LPO — DOI: 10.5281/zenodo.18516813Paper 9: Ising formulation-invariance — DOI: 10.5281/zenodo.18517570Paper 10: Logical geography of mathematical physics — DOI: 10.5281/zenodo.18527877Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10.5281/zenodo.18527676Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18528793Paper 13: Event horizon as logical boundary — DOI: 10.5281/zenodo.18529007 Note: GitHub repository is not maintained; please see Zenodo for current files.