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 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.