Constructive Stratification of the Standard Model Yukawa RG: Numerical Tests and Lean 4 Formalization

Title: Constructive Stratification of the Standard Model Yukawa RG: Numerical Tests and Lean 4 Formalization Description (for Zenodo): Paper 18 in the Constructive Reverse Mathematics for Mathematical Physics series. Ten numerical investigations (Phases A–B) test whether removing LPO idealizations from the Standard Model Yukawa renormalization group reveals BISH-level mechanisms for the fermion mass hierarchy. All ten yield negative results: the SM's infrared dynamics do not determine the mass hierarchy in any parameterization, at any loop order, or at any discretization scale tested. A Lean 4 formalization (~900 lines, 5 theorems verified against Mathlib) establishes the sharp constructive stratification: BISH < WLPO (thresholds) < LPO (eigenvalue crossings) < full Classical The one-loop Yukawa RG flow is BISH: polynomial Picard iteration preserves ℚ[t] at every finite step (Theorem 1) and converges with an explicit Cauchy modulus (Theorem 2). Step-function thresholds cost WLPO (Theorem 5), and CKM eigenvalue-crossing detection costs LPO (Theorem 4). Physical mechanisms — polynomial beta functions, smooth threshold matching, diagonalization with mass gaps — are uniformly BISH; omniscience enters only through textbook idealizations. Contents: Unified paper (23 pages, LaTeX source + compiled PDF) Phase A: One-loop numerical investigation (Python, ~600 lines, 10 plots) Phase B: Two-loop numerical investigation (Python, ~600 lines, 5 plots) Phase C: Lean 4 formalization bundle (902 lines, 5 files, 0 errors, 0 warnings, 0 sorries) Dependencies: Python 3.9+, NumPy, SciPy, Matplotlib; Lean 4 v4.28.0-rc1, Mathlib Previous papers with Lean 4 formalizations: Papers 2, 6, 7, 8, 23, 28. Complete Paper List 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.18626637 [v 4.0 Technical Synthesis of Papers 1–24]Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10.5281/zenodo.18527676Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18626652 [v 2.0 Historical Synthesis of Papers 1–16]Paper 13: Event horizon as logical boundary — DOI: 10.5281/zenodo.18529007Paper 14: Quantum decoherence — DOI: 10.5281/zenodo.18569068Paper 15: Noether theorem — DOI: 10.5281/zenodo.18572494Paper 16: Technical note: Born rule — DOI: 10.5281/zenodo.18575377Paper 17: Bekenstein-Hawking formula — DOI: 10.5281/zenodo.18597306Paper 18: Constructive Stratification of the Standard Model Yukawa RG-> 10.5281/zenodo.18626839 (version 2)Paper 19: WKB tunneling and LLPO — DOI: 10.5281/zenodo.18602596Paper 20: Observable-dependent logical cost, 1D Ising magnetization and WLPO — DOI: 10.5281/zenodo.18603079Paper 21: Bell nonlocality and LLPO — DOI: 10.5281/zenodo.18603251Paper 22: Markov's Principle and radioactive decay — DOI: 10.5281/zenodo.18603503 Paper 23: Fan Theorem and optimization — DOI: 10.5281/zenodo.18604312 Paper 24: Kochen-Specker contextuality and LLPO — DOI: 10.5281/zenodo.18604317 Paper 25: Ergodic Theorems and Laws of Large Numbers against Countable and Dependent Choice — DOI: 10.5281/zenodo.18615453 Paper 26 Bidual Gap Detection Is WLPO-Complete: Gödel Sequences — DOI 10.5281/zenodo.18615457 Paper 27: IVT as the mechanism behind LLPO in Bell physics — DOI: 10.5281/zenodo.18615459 Paper 28: Classical Mechanics. 10.5281/zenodo.18616620 Summary Papers: Paper 10: Logical geography of mathematical physics — DOI: 10.5281/zenodo.18626637 [v 3.0 Technical Synthesis of Papers 1–24] Paper 12: Constructive history of mathematical physics — 10.5281/zenodo.18626652 [v 2.0 Historical Synthesis of Papers 1–16] Note: GitHub repository is not maintained; please see Zenodo for current files.