Theme/Gravity.lean — FrcLedger

1import Mathlib23/-!4# FrcLedger.Theme.Gravity — the gravity theme on Mathlib: the exact faces of 21-gravity (10 October 2026)56The exact Mathlib variants of 21-gravity's rows, moved from the paper module `FrcLedger/Gravity.lean` (which keeps7every old name as an alias): the Carrier register on a field with `4S + 1 = 0` — the calibration congruence, the8register value `G = 2S`, the action quantum as the quarter-turn pair (21:A1, C2, C5, C16); the count face of the area9law and the merger law on `ℤ` (21:C13); the cover forcing and the PPN triangle over `ℚ` (21:A9, C7, C8, C25); the10mass–energy channel as a gcd (21:A9); the central difference's anti-self-adjointness and the finite Fourier11shift theorem on `ZMod N` (21:C9, C20). No reals here (gate G09): the chart readings are `Theme/Strong.lean`'s. The core12proves the same faces with no axioms (`FrcCore/Theme/Gravity.lean`, `Theme/Drift.lean`, `Theme/Lattice.lean`,13`Theme/Shift.lean`); these are their Mathlib counterparts on the classical hierarchy.14-/1516namespace FRC.GravML1718/-! ## The Carrier register (21:A1, C2, C5, C16) -/19section register2021variable {K : Type*} [Field K]2223/-- 21:C16, 21:A1 — the calibration congruence: on the Carrier chart `4S + 1 = 0` the full cycle `2π ↦ 4S` is24`−1` and `(4S)² = 1`, one residue relation. -/25theorem calibration_congruence (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) :26    ((4 * S : ℕ) : K) = -1 ∧ ((4 * S : ℕ) : K) ^ 2 = 1 := by27  push_cast at hΩ ⊢28  exact ⟨by linear_combination hΩ, by linear_combination (4 * (S : K) - 1) * hΩ⟩2930/-- 21:C2, 21:C5, 21:C16 — the register value of the Newton constant, `G = 2S`, on the Carrier chart31`4S + 1 = 0`: `2G = −1` (the half-cycle); `(−2) G = 1`, the face convention `4π ↦ −2` with `G = (−2)⁻¹`; the32Gauss count `(2 · 4S) G = 1`; `c² = 2⁻¹ = 2S + 1` and `G = −c²` (the chart ratio `4π/2π = 2` is read as33`(−2)/(−1)`). The uniqueness of the linear solution is `Dimensions.G_unique`. -/34theorem newton_register (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) :35    2 * ((2 * S : ℕ) : K) = -1 ∧ (-2) * ((2 * S : ℕ) : K) = 1 ∧36    (2 * ((4 * S : ℕ) : K)) * ((2 * S : ℕ) : K) = 1 ∧37    2 * ((2 * S + 1 : ℕ) : K) = 1 ∧ ((2 * S + 1 : ℕ) : K) = 2⁻¹ ∧38    ((2 * S : ℕ) : K) = -((2 * S + 1 : ℕ) : K) := by39  push_cast at hΩ ⊢40  refine ⟨by linear_combination hΩ, by linear_combination -hΩ,41    by linear_combination (4 * (S : K) - 1) * hΩ, by linear_combination hΩ, ?_,42    by linear_combination hΩ⟩43  exact eq_inv_of_mul_eq_one_left (by linear_combination hΩ)4445/-- On the Carrier `𝔽_Ω`, `Ω = 4S + 1` prime, `2 ≠ 0` (`Ω` is odd). -/46theorem carrier_two_ne_zero (S : ℕ) [hp : Fact (Nat.Prime (4 * S + 1))] :47    (2 : ZMod (4 * S + 1)) ≠ 0 := by48  rw [show (2 : ZMod (4 * S + 1)) = ((2 : ℕ) : ZMod (4 * S + 1)) by norm_cast, Ne,49    ZMod.natCast_eq_zero_iff]50  intro hd51  have h1 : 4 * S + 1 ≤ 2 := Nat.le_of_dvd (by norm_num) hd52  have h2 : 2 ≤ 4 * S + 1 := hp.out.two_le53  omega5455/-- In any field with `4S + 1 = 0` and `2 ≠ 0`, a quarter-turn `i² = −1` gives a square root of `S`,56`r = i/2`, with `(2r)² = −1`. -/57theorem hbar_of_quarter_turn {K : Type*} [Field K] (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0)58    (h2 : (2 : K) ≠ 0) (i : K) (hi : i ^ 2 = -1) :59    ∃ r : K, r ^ 2 = (S : K) ∧ (2 * r) ^ 2 = -1 := by60  push_cast at hΩ61  have h4 : (2⁻¹ : K) ^ 2 * 4 = 1 := by field_simp; norm_num62  refine ⟨i * 2⁻¹, ?_, ?_⟩63  · calc (i * 2⁻¹) ^ 2 = i ^ 2 * (2⁻¹) ^ 2 := by ring64      _ = -1 * (2⁻¹) ^ 2 := by rw [hi]65      _ = (S : K) := by linear_combination (-(2⁻¹ : K) ^ 2) * hΩ + (S : K) * h466  · have : 2 * (i * 2⁻¹) = i := by field_simp67    rw [this, hi]6869/-- 21:C5, 21:C16, 21:A1 — the action quantum as the quarter-turn pair: on every Carrier `Ω = 4S + 1` prime, `S`70is a square (`S = (i/2)²` with `i² = −1`, since `4S = −1`), so `ħ = 2√S` has `ħ² = 4S = −1` — `ħ` is one of the71quarter-turn pair `±i`. -/72theorem hbar_register (S : ℕ) [Fact (Nat.Prime (4 * S + 1))] :73    ∃ r : ZMod (4 * S + 1), r ^ 2 = (S : ZMod (4 * S + 1)) ∧ (2 * r) ^ 2 = -1 := by74  obtain ⟨i, hi⟩ : IsSquare (-1 : ZMod (4 * S + 1)) := ZMod.exists_sq_eq_neg_one_iff.mpr (by omega)75  exact hbar_of_quarter_turn S (ZMod.natCast_self _) (carrier_two_ne_zero S) i (by rw [sq]; exact hi.symm)7677end register7879/-! ## The count face and the cover forcing (21:A9, C7, C8, C13, C25) -/80section count8182/-- 21:C13 — the count face of the area law on a symmetry-complete shell `p = 4κ + 1`: with `S = (p² − 1)/4`,83i.e. `4S + 1 = p²` for `S = κ(4κ + 2)`, and the coordinate area `A = p(p + 1)`, the ratio `S/A = κ/p` holds84exactly (`Sp = κA`) and `S = (A/4)(1 − 1/p)` (`4Sp = A(p − 1)`) — the Bekenstein quarter as the `Q₄` quotient. -/85theorem count_face (κ : ℕ) :86    4 * (κ * (4 * κ + 2)) + 1 = (4 * κ + 1) ^ 2 ∧87    (κ * (4 * κ + 2)) * (4 * κ + 1) = κ * ((4 * κ + 1) * (4 * κ + 2)) ∧88    4 * (κ * (4 * κ + 2)) * (4 * κ + 1) = ((4 * κ + 1) * (4 * κ + 2)) * (4 * κ) :=89  ⟨by ring, by ring, by ring⟩9091/-- 21:C13 — the merger area law on the count face, `A = M(M + 1)`: `ΔA = 2M₁M₂` exactly under additive mass,92the paper's instance `27 811 + 1 596 → 29 407` giving `ΔA = 88 772 712`; with a radiated `δ` the count gives93`ΔA = 2M₁M₂ − (2(M₁ + M₂) + 1)δ + δ²`, at most the additive value for `0 ≤ δ ≤ 2(M₁ + M₂) + 1` — the area94statement an inequality (the coefficient `−2(M₁ + M₂)δ` is the `A = M²` form; on the count face the linear95term carries the extra `−δ`). -/96theorem merger_area_law (M₁ M₂ δ : ℤ) :97    (M₁ + M₂) * (M₁ + M₂ + 1) - M₁ * (M₁ + 1) - M₂ * (M₂ + 1) = 2 * M₁ * M₂ ∧98    (M₁ + M₂ - δ) * (M₁ + M₂ - δ + 1) - M₁ * (M₁ + 1) - M₂ * (M₂ + 1)99      = 2 * M₁ * M₂ - (2 * (M₁ + M₂) + 1) * δ + δ ^ 2 ∧100    (0 ≤ δ → δ ≤ 2 * (M₁ + M₂) + 1 →101      (M₁ + M₂ - δ) * (M₁ + M₂ - δ + 1) - M₁ * (M₁ + 1) - M₂ * (M₂ + 1) ≤ 2 * M₁ * M₂) ∧102    (27811 + 1596) * (27811 + 1596 + 1) - 27811 * (27811 + 1) - 1596 * (1596 + 1) = (88772712 : ℤ) := by103  refine ⟨by ring, by ring, ?_, by norm_num⟩104  intro h0 h1105  nlinarith [mul_nonneg h0 (sub_nonneg.mpr h1)]106107/-- 21:A9, 21:C25, 21:C7, 21:C8 — the cover forcing: the apsidal coefficient `2 − β + 2γ` against the108PPN-free deficit `3/2` equals the two-face ratio `2` exactly when `2γ − β = 1`, with deviation109`(2/3)(2γ − β − 1)`; channel unity `γ = 1` makes the deflection factor `(1 + γ)/2` equal to `1` (the full110`4Gm/c²b`) and, together with the forcing, gives `β = 1`, the perihelion factor `(2 + 2γ − β)/3` then `1`. -/111theorem cover_forcing (β γ : ℚ) :112    ((2 - β + 2 * γ) / (3 / 2) = 2 ↔ 2 * γ - β = 1) ∧113    (2 - β + 2 * γ) / (3 / 2) - 2 = 2 / 3 * (2 * γ - β - 1) ∧114    (γ = 1 → (1 + γ) / 2 = 1 ∧ (2 * γ - β = 1 → β = 1 ∧ (2 + 2 * γ - β) / 3 = 1)) := by115  refine ⟨?_, by ring, ?_⟩116  · constructor <;> intro h <;> linarith117  · rintro rfl118    exact ⟨by norm_num, fun h => ⟨by linarith, by linarith⟩⟩119120/-- 38:C8 — the face-ratio identity of the parametrised post-Newtonian family (Statement *The physical floors*,12138-s13): with the apsidal coefficient `2 − β + 2γ` and the `β, γ`-free clock-deficit coefficient `3/2`, the face122ratio is `(2/3)(2 + 2γ − β)`, equal to `2` exactly when `2γ − β = 1`, with deviation `(2/3)(2γ − β − 1)`; the123exponential metric `β = γ = 1` satisfies it; in Brans–Dicke theory (`β = 1`, `γ = (1 + ω)/(2 + ω)`) the combination124is `2γ − β − 1 = −2/(2 + ω)`, nonzero at every finite coupling, deviation `−4/(3(2 + ω))`, and below every `ε` past125`ω = 2/ε` (the general-relativistic limit, stated over `ℚ`). The coefficients themselves are the continuum chart's (the series of the126isotropic metric, `o1_gr_chart.py`); the algebra is exact over `ℚ`. -/127theorem ppn_faces (β γ : ℚ) :128    (2 - β + 2 * γ) / (3 / 2) = 2 / 3 * (2 + 2 * γ - β) ∧129    (2 / 3 * (2 + 2 * γ - β) = 2 ↔ 2 * γ - β = 1) ∧130    2 / 3 * (2 + 2 * γ - β) - 2 = 2 / 3 * (2 * γ - β - 1) ∧131    (2 * (1 : ℚ) - 1 = 1) ∧132    (∀ ω : ℚ, 2 + ω ≠ 0 → 2 * ((1 + ω) / (2 + ω)) - 1 - 1 = -2 / (2 + ω) ∧133      2 / 3 * (2 * ((1 + ω) / (2 + ω)) - 1 - 1) = -4 / (3 * (2 + ω)) ∧ -2 / (2 + ω) ≠ 0) ∧134    (∀ ε : ℚ, 0 < ε → ∃ W : ℚ, ∀ ω : ℚ, W < ω → |(-2 : ℚ) / (2 + ω)| < ε) := by135  refine ⟨by ring, ⟨fun h => by linarith, fun h => by linarith⟩, by ring, by norm_num, fun ω hω => ⟨?_, ?_, ?_⟩, ?_⟩136  · field_simp; ring137  · field_simp; ring138  · exact div_ne_zero (by norm_num) hω139  · intro ε hε140    refine ⟨2 / ε, fun ω hω => ?_⟩141    have h2 : 0 < 2 / ε := by positivity142    have hpos : 0 < 2 + ω := by linarith143    rw [abs_div, abs_neg, abs_of_pos hpos, abs_of_pos (by norm_num : (0 : ℚ) < 2), div_lt_iff₀ hpos]144    have : 2 / ε < ω := hω145    rw [div_lt_iff₀ hε] at this146    linarith147148/-- 38:C12, 38:C7 — the registration dictionary on a hosted pair: matching the temporal face `κ/(2S)` to the149circular-orbit clock deficit `(3/2) r_g/p_sl` forces `p_sl = 3 (S/κ) r_g`, under which the angular face reads150`3 r_g/p_sl = κ/S` automatically: one relation, homogeneous of degree `0`, fixing the ratio `p_sl/r_g = 3S/κ` —151`58` at `(13, 233)` (`κ = 3`, `S = 58`: `p_sl = S r_g`), `174` at `(5, 233)`; the two faces `κ/S : κ/(2S) = 2`. -/152theorem registration_dictionary (κ S rg psl : ℚ) (hκ : κ ≠ 0) (hS : S ≠ 0) (hrg : rg ≠ 0) (hpsl : psl ≠ 0) :153    ((3 / 2) * (rg / psl) = κ / (2 * S) ↔ psl = 3 * (S / κ) * rg) ∧154    (psl = 3 * (S / κ) * rg → 3 * rg / psl = κ / S ∧ psl / rg = 3 * S / κ) ∧155    (κ / S) / (κ / (2 * S)) = 2 ∧ 3 * (58 : ℚ) / 3 = 58 ∧ 3 * (58 : ℚ) / 1 = 174 := by156  refine ⟨⟨fun h => ?_, fun h => ?_⟩, fun h => ⟨?_, ?_⟩, ?_, by norm_num, by norm_num⟩157  · field_simp at h ⊢; linarith158  · subst h; field_simp159  · subst h; field_simp160  · subst h; field_simp161  · field_simp162163/-- 21:A9 — the mass–energy channel `C_{p−1} ∩ C_{2(p+1)} = Q₄`: on every shell `p ≡ 1 (mod 4)`,164`gcd(p − 1, 2(p + 1)) = 4`; the subgroup reading — in the cyclic unit group of `𝔽_{p²}` (order `(p − 1)(p + 1)`)165the subgroups of orders `p − 1` and `2(p + 1)` meet in the subgroup of order `gcd` — is not formalised here. -/166theorem channel_q4 (p : ℕ) (hp : p % 4 = 1) : Nat.gcd (p - 1) (2 * (p + 1)) = 4 := by167  obtain ⟨κ, rfl⟩ : ∃ κ, p = 4 * κ + 1 := ⟨p / 4, by omega⟩168  have h1 : 4 * κ + 1 - 1 = 4 * κ := by omega169  have h2 : 2 * (4 * κ + 1 + 1) = 4 * (1 + 2 * κ) := by ring170  rw [h1, h2, Nat.gcd_mul_left, Nat.gcd_add_mul_right_right, Nat.gcd_one_right]171172end count173174/-! ## The lattice on `ZMod N` (21:C9, C20) -/175section lattice176177variable {N : ℕ} [NeZero N] {R : Type*} [CommRing R]178179/-- 21:C9 — anti-self-adjointness of the central difference on the cycle `ℤ/N`: with180`(Δf)(x) = f(x + 1) − f(x − 1)`, `Σ_x f(x)(Δg)(x) = −Σ_x (Δf)(x) g(x)` — `Δᵀ = −Δ`, the identity that carries181the discrete Fierz–Pauli gauge invariance (the package proves the four-term functional's invariance as an exact182integer identity; the paper's `½` in `D_μ = (T_μ − T_μ⁻¹)/2` scales both sides alike). The one-sided183difference `(δf)(x) = f(x + 1) − f(x)` has adjoint the negative *backward* difference,184`Σ_x f(x)(δg)(x) = −Σ_x (f(x) − f(x − 1)) g(x)` — the package's failing control is that this is not `−δ`. -/185theorem central_difference_adjoint (f g : ZMod N → R) :186    ∑ x, f x * (g (x + 1) - g (x - 1)) = -∑ x, (f (x + 1) - f (x - 1)) * g x ∧187    ∑ x, f x * (g (x + 1) - g x) = -∑ x, (f x - f (x - 1)) * g x := by188  have h1 : ∑ x, f x * g (x + 1) = ∑ x, f (x - 1) * g x := by189    rw [← Equiv.sum_comp (Equiv.addRight (1 : ZMod N)) (fun x => f (x - 1) * g x)]190    simp191  have h2 : ∑ x, f x * g (x - 1) = ∑ x, f (x + 1) * g x := by192    rw [← Equiv.sum_comp (Equiv.subRight (1 : ZMod N)) (fun x => f (x + 1) * g x)]193    simp194  constructor195  · simp only [mul_sub, sub_mul, Finset.sum_sub_distrib, h1, h2]; ring196  · simp only [mul_sub, sub_mul, Finset.sum_sub_distrib, h1]; ring197198/-- The finite Fourier transform on the cycle, against a character `ζ` with `ζ^N = 1`:199`(F f)(k) = Σ_x f(x) ζ^{xk}`. -/200def dft (ζ : R) (f : ZMod N → R) (k : ZMod N) : R := ∑ x, f x * ζ ^ (x.val * k.val)201202omit [NeZero N] in203/-- A root of unity is insensitive to the reduction of its exponent modulo `N`. -/204theorem pow_val_mod (ζ : R) (hζ : ζ ^ N = 1) (m k : ℕ) : ζ ^ ((m % N) * k) = ζ ^ (m * k) := by205  conv_rhs => rw [← Nat.mod_add_div m N]206  rw [add_mul, pow_add, mul_assoc, pow_mul, pow_mul, hζ, one_pow, mul_one]207208omit [NeZero N] in209/-- A root of unity is insensitive to the reduction of a factor of its exponent modulo `N`. -/210theorem pow_mul_val_mod (ζ : R) (hζ : ζ ^ N = 1) (k m : ℕ) : ζ ^ (k * (m % N)) = ζ ^ (k * m) := by211  rw [mul_comm, pow_val_mod ζ hζ, mul_comm]212213/-- 21:C20 — the finite Fourier shift theorem in both forms, the kick of the two-shift law: the kick, a214character `ζ^{ax}` multiplying `f` in position, shifts the transform, `F(ζ^{a·} f)(k) = (F f)(k + a)`; dually,215shifting `f` by `a` multiplies its transform by the character, `F(f(· − a))(k) = ζ^{ak} (F f)(k)`. -/216theorem shift_theorem (ζ : R) (hζ : ζ ^ N = 1) (f : ZMod N → R) (a k : ZMod N) :217    dft ζ (fun x => ζ ^ (a.val * x.val) * f x) k = dft ζ f (k + a) ∧218    dft ζ (fun x => f (x - a)) k = ζ ^ (a.val * k.val) * dft ζ f k := by219  constructor220  · unfold dft221    apply Finset.sum_congr rfl222    intro x _223    dsimp only224    rw [ZMod.val_add, pow_mul_val_mod ζ hζ, mul_add, pow_add, mul_comm a.val x.val]225    ring226  · unfold dft227    rw [Finset.mul_sum, ← Equiv.sum_comp (Equiv.addRight a)]228    apply Finset.sum_congr rfl229    intro x _230    simp only [Equiv.coe_addRight, add_sub_cancel_right]231    rw [ZMod.val_add, pow_val_mod ζ hζ, add_mul, pow_add]232    ring233234end lattice235236end FRC.GravML237