Newton vs. Lagrange vs. Hamilton: Constructive Stratification of Classical Mechanics (Paper 28, CRM Series)

Paper 28 in the Constructive Reverse Mathematics (CRM) series. Lean 4 formalization proving that the three textbook formulations of classical mechanics -- Newtonian (equation of motion), Lagrangian (variational), and Hamiltonian (phase space) -- are constructively stratified: they require different logical principles. For the discrete harmonic oscillator with N=2 time steps: (1) The Euler-Lagrange equation has a unique explicit solution, provable in BISH. (2) Hamilton's equations have a unique explicit solution in BISH, and the discrete Legendre transform bridging Lagrangian and Hamiltonian formulations is an invertible BISH-level map. (3) The assertion that every continuous function on 0,1 attains its minimum is equivalent to the Fan Theorem (FT). All equation-solving is BISH. All optimization is FT. The bridge between formulations is BISH. Formalized in Lean 4 with Mathlib (621 lines, 6 source files, zero sorry, zero custom axioms). Includes LaTeX companion paper (17 pages). Keywords:constructive reverse mathematics, Fan Theorem, BISH, classical mechanics, Euler-Lagrange equations, Hamilton's equations, Legendre transform, Lean 4, Mathlib, formal verification, variational principles omplete 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: 110.5281/zenodo.18613542 v 3.0 Technical Synthesis of Papers 1–24Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10.5281/zenodo.18527676Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18581707 v 2.0 Historical Synthesis of Papers 1–16Paper 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: Fermion mass hierarchy and scaffolding principle — DOI: 10.5281/zenodo.18600243Paper 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: 110.5281/zenodo.18613542 v 3.0 Technical Synthesis of Papers 1–24 Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18581707 v 2.0 Historical Synthesis of Papers 1–16