-- QLF_MercuryPerihelion.lean -- Mercury perihelion advance Δφ = 6πGM/(c²a(1-e²)) from QLF substrate -- (Mercury_Perihelion.md), composing Newton (Gravity_From_Delay) with -- Schwarzschild weak-field metric (GR_Schwarzschild) for the famous -- 43"/century test of General Relativity. -- -- The substrate composition: -- -- 1. Newton's law F = GMm/r² from holographic event-counting -- (QLF_GravityFromDelay.lean). -- -- 2. Schwarzschild metric weak-field components from substrate -- Cross-Frequency Lorentz + radial event scaling -- (GR_Schwarzschild.md, not yet Lean-anchored individually). -- -- 3. Effective orbital potential gains a 1/r³ correction from -- g_rr ≠ 1: V_eff(r) = -GMm/r + L²/(2mr²) - GM L²/(mc² r³). -- -- 4. Perihelion advance per orbit (standard orbital perturbation -- theory applied to the 1/r³ term): -- -- Δφ = 6πGM/(c² a (1-e²)) = 3π R_s/(a (1-e²)) -- -- where R_s = 2GM/c² is the Schwarzschild radius. -- -- Mercury numerical check: -- M_Sun = 1.989 × 10³⁰ kg, a = 5.791 × 10¹⁰ m, e = 0.2056, -- T = 87.969 days, R_s(Sun) = 2.953 km -- Per-orbit Δφ = 3π × 2953 / (5.791e10 × 0.9577) = 5.02 × 10⁻⁷ rad -- 415 orbits/century × 5.02e-7 × 206265 arcsec/rad ≈ 42.99"/century -- vs Park et al. (2017) measured 42.98 ± 0.04"/century → 0.03% match. -- -- This is the **eighth Lean-anchored fundamental-physics theorem** in -- the QLF tree (after α, m_p/m_e, γ, Dirac, Lamb, g−2, Gravity). -- -- Honest scope. This module Lean-anchors: -- • the Schwarzschild radius R_s = 2GM/c² definition -- • the perihelion-advance formula Δφ = 3π R_s/(a(1-e²)) -- • the equivalent closed form Δφ = 6πGM/(c²a(1-e²)) -- • the dimensionless ratio (Δφ a (1-e²))/(3π) = R_s -- -- It does NOT Lean-anchor: -- • the orbital perturbation analysis itself (standard classical -- mechanics; integration of 1/r³ correction gives the prefactor 6π). -- Substrate-native derivation is Tier-3 open (Mercury_Perihelion.md §5). -- • the substrate derivation of the Schwarzschild metric components -- (sketched in GR_Schwarzschild.md, not yet Lean-anchored). -- • the Mercury observables (M_Sun, a, e, T) as substrate-derived — -- these are astronomical inputs. -- -- Companion to: -- • Mercury_Perihelion.md — structural argument -- • mercury_perihelion_demo.py — numerical demo -- • GR_Schwarzschild.md — substrate metric -- • Gravity_From_Delay.md — Newton's law -- • Cross_Frequency_Lorentz.md — gravitational redshift -- • Kitada_Local_Time_GR.md — Markov-blanket GR programme -- • lean/QLF_GravityFromDelay.lean — Newton substrate Lean -- • lean/QLF_SubstrateLightSpeed.lean — c substrate Lean -- • lean/QLF_EinsteinGeometricFactor.lean — 8π = 4π · 2 import Mathlib.Analysis.SpecialFunctions.Pow.Real namespace QLF /-- **The Schwarzschild radius of a mass M**: `R_s = 2 G M / c²`. This is the substrate radius at which Schwarzschild metric component `g_tt = -(1 - R_s/r)` reaches singular behaviour. For the Sun: `R_s ≈ 2.953 km`. For an electron mass: `R_s ≈ 1.35 × 10⁻⁵⁷ m` (far below Planck length — quantum gravity regime, not classical Schwarzschild). `G` and `c` are substrate-derived in QLF: `G = L_Planck² c³ / ℏ` (substrate event quantum), `c = L_Planck / τ_Planck` (substrate event quantum). `M` is an empirical input for the specific astronomical body. -/ noncomputable def schwarzschild_radius (G M c : ℝ) : ℝ := 2 * G * M / c^2 /-- **Schwarzschild radius identity**: `R_s = 2GM/c²` (definitional). -/ theorem schwarzschild_radius_eq (G M c : ℝ) : schwarzschild_radius G M c = 2 * G * M / c^2 := rfl /-- **Perihelion advance per orbit** for a test mass in Schwarzschild weak-field orbit: Δφ = 3π R_s / (a (1 - e²)) per orbit. Equivalently: `Δφ = 6π G M / (c² a (1 - e²))`. Derivation: in the Schwarzschild metric, the radial geodesic equation gives an effective potential `V_eff = -GMm/r + L²/(2mr²) - GM L²/(mc² r³)`. The 1/r³ correction (relative to Kepler) shifts the apsidal angle by `Δφ` per orbit, computed via standard perturbation theory as Δφ = (3 R_s) / (a (1 - e²)) × 2π × (1/2) = 3π R_s / (a (1 - e²)). The (1 - e²) factor enhances precession for non-circular orbits; for e = 0 (circular): `Δφ = 3π R_s / a`. -/ noncomputable def perihelion_advance_per_orbit (R_s a e : ℝ) : ℝ := 3 * Real.pi * R_s / (a * (1 - e^2)) /-- **Equivalent form**: `Δφ = 6πGM/(c²a(1-e²))`. Substituting `R_s = 2GM/c²` into the perihelion-advance formula above gives this standard textbook form. -/ noncomputable def perihelion_advance_from_GMc (G M c a e : ℝ) : ℝ := 6 * Real.pi * G * M / (c^2 * a * (1 - e^2)) /-- **The two perihelion formulas agree** when R_s = 2GM/c² (assuming c, a, (1 - e²) ≠ 0; physically Newton perihelion is only defined for bound non-degenerate orbits). -/ theorem perihelion_advance_form_equivalence (G M c a e : ℝ) (hc : c ≠ 0) (ha : a ≠ 0) (he : 1 - e^2 ≠ 0) : perihelion_advance_per_orbit (schwarzschild_radius G M c) a e = perihelion_advance_from_GMc G M c a e := by unfold perihelion_advance_per_orbit perihelion_advance_from_GMc schwarzschild_radius have hc2 : c^2 ≠ 0 := pow_ne_zero _ hc field_simp ring /-- **Dimensionless ratio identity**: the perihelion advance per orbit relates linearly to the Schwarzschild radius via the orbital geometry. Specifically: (Δφ × a × (1 - e²)) / (3π) = R_s. This is the perihelion advance expressed as a measurement of R_s. -/ theorem perihelion_advance_extracts_R_s (R_s a e : ℝ) (ha : a ≠ 0) (he : 1 - e^2 ≠ 0) : perihelion_advance_per_orbit R_s a e * a * (1 - e^2) / (3 * Real.pi) = R_s := by unfold perihelion_advance_per_orbit have hpi : Real.pi ≠ 0 := Real.pi_ne_zero field_simp /-- **Per-century precession**: Δφ_century = N_orbits × Δφ_orbit where `N_orbits = T_century / T_orbit`. For Mercury: T_century = 100 × 365.25 days, T_Mercury = 87.969 days, N_orbits ≈ 415.2. Per-century advance ≈ 5.02e-7 × 415.2 rad ≈ 2.08e-4 rad ≈ 42.99 arcsec. -/ noncomputable def perihelion_advance_per_century (delta_phi_orbit T_century T_orbit : ℝ) : ℝ := delta_phi_orbit * (T_century / T_orbit) /-- **Per-century expansion**. -/ theorem perihelion_advance_per_century_eq (delta_phi_orbit T_century T_orbit : ℝ) : perihelion_advance_per_century delta_phi_orbit T_century T_orbit = delta_phi_orbit * T_century / T_orbit := by unfold perihelion_advance_per_century ring /-- **Composition of substrate primitives**: the Mercury perihelion advance assembles from the substrate primitives. Packaging: - Schwarzschild radius `R_s = 2GM/c²` is the substrate metric scale. - Perihelion advance `Δφ = 3π R_s / (a(1-e²))` per orbit follows from substrate Schwarzschild + orbital perturbation theory. - Equivalent form `Δφ = 6πGM/(c²a(1-e²))` substitutes R_s. - Per-century advance scales by N orbits per century. -/ theorem mercury_perihelion_substrate_summary (G M c a e : ℝ) (hc : c ≠ 0) (ha : a ≠ 0) (he : 1 - e^2 ≠ 0) : schwarzschild_radius G M c = 2 * G * M / c^2 ∧ perihelion_advance_per_orbit (schwarzschild_radius G M c) a e = perihelion_advance_from_GMc G M c a e ∧ (∀ R_s, perihelion_advance_per_orbit R_s a e = 3 * Real.pi * R_s / (a * (1 - e^2))) := by refine ⟨rfl, ?_, ?_⟩ · exact perihelion_advance_form_equivalence G M c a e hc ha he · intro R_s rfl /-- **What this module does NOT prove**. - It does NOT derive the orbital-perturbation prefactor `3π` from substrate first principles. Standard classical mechanics gives the 3π via integration of the 1/r³ correction over one Kepler orbit; substrate-native derivation is Tier-3 open. - It does NOT individually Lean-anchor the Schwarzschild metric components `g_tt = -(1 - R_s/r)` and `g_rr = (1 - R_s/r)⁻¹`. These are sketched in `GR_Schwarzschild.md` via Cross-Frequency Lorentz + substrate event scaling; full Lean-anchoring is a sibling module to `QLF_GravityFromDelay`. - It does NOT derive Mercury observables (M_Sun, a, e, T) from substrate. These are astronomical inputs. - It does NOT extend to other GR tests (light bending, Shapiro delay, frame-dragging). Same substrate framework would extend but is open. -/ theorem mercury_perihelion_not_proved_here : True := trivial end QLF