The Mathlib module lean/FrcLedger/Keys/Gravity.lean of the framework's chart theme, the readings against the continuum that the master's rows L1, L3, L8 and P1 stake (ledger migration, task LM30): 9 theorems (0 definitions): 0 with no axioms, 0 at tier 1 (propext, Quot.sound), 9 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (violet, Mathlib; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcLedger.Theme.Gravity23/-!4# FrcLedger.Keys.Gravity — the keyed theorems of the gravity theme (ledger migration, task LM19)56One declaration per key, `FRC.LedgerML.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem7that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration8`FRC.<Module>.p<key>` as an alias. Every declaration has the axioms of Mathlib's hierarchy at most (`check_axioms.py`).9-/1011namespace FRC.LedgerML1213-- Keys of the gravity theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)14/-- p21001 — 21:A1. The finite substrate: the torsor Carrier, coordinatized by a frame as $\F_\Omega$, its cardinality the Carrier identity $\Omega=4S+1$ with the measured $S\sim10^{122}$ (Planck units) locating the coherence horizon, with the phase cycle $C_{\Omega-1}$, the quarter-turn core $Q_4$, the drive (time is scale-dilation, each Subject's own), the coherence horizon $\sqrt\Omega$, and the resolution floor $1/\sqrt\Omega$. -/15
theorem p21001 : (∀ {K : Type u_1} [Field K] (S : ℕ), ↑((4 : ℕ) * S + (1 : ℕ)) = (0 : K) → ↑((4 : ℕ) * S) = (-1 : K) ∧ ↑((4 : ℕ) * S) ^ (2 : ℕ) = (1 : K)) ∧ ∀ (S : ℕ) [Fact (Nat.Prime ((4 : ℕ) * S + (1 : ℕ)))], ∃ r, r ^ (2 : ℕ) = ↑S ∧ ((2 : ZMod ((4 : ℕ) * S + (1 : ℕ))) * r) ^ (2 : ℕ) = (-1 : ZMod ((4 : ℕ) * S + (1 : ℕ))) :=16 And.intro @FRC.GravML.calibration_congruence (@FRC.GravML.hbar_register)17/-- p21009 — 21:A9. The minimal-instance results consumed: the two-face count of the drift (angular $\kap/S$, temporal $\kap/(2S)$, ratio $2$ the double cover), the registration dictionary $p_{\mathrm{sl}}=3(S/\kap)\,r_g$ with the forcing $2\gamma-\beta=1$, and the mass--energy channel $C_{\p-1}\cap C_{2(\p+1)}=Q_4$. -/18theorem p21009 : (∀ (β γ : ℚ), (((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) = (2 : ℚ) ↔ (2 : ℚ) * γ - β = (1 : ℚ)) ∧ ((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) - (2 : ℚ) = (2 / 3 : ℚ) * ((2 : ℚ) * γ - β - (1 : ℚ)) ∧ (γ = (1 : ℚ) → ((1 : ℚ) + γ) / (2 : ℚ) = (1 : ℚ) ∧ ((2 : ℚ) * γ - β = (1 : ℚ) → β = (1 : ℚ) ∧ ((2 : ℚ) + (2 : ℚ) * γ - β) / (3 : ℚ) = (1 : ℚ)))) ∧ ∀ (p : ℕ), p % (4 : ℕ) = (1 : ℕ) → (p - (1 : ℕ)).gcd ((2 : ℕ) * (p + (1 : ℕ))) = (4 : ℕ) :=19 And.intro @FRC.GravML.cover_forcing (@FRC.GravML.channel_q4)20set_option linter.defProp false in21/-- p21017 — 21:C2. Newton's law $F=-Gm_1m_2/r^2$ with $G=1/4\pi\varkappa$ [chart] (register value $G=2S$): the $r^{-2}$ from harmonicity in the three frame freedoms, the product $m_1m_2$ from coherent additivity. -/22def p21017 := @FRC.GravML.newton_register23/-- p21024 — 21:C9. The discrete Fierz--Pauli functional, exactly gauge-invariant and the unique adjacency-local stiffness on the shell (the spin-one case is unique-Maxwell). -/24theorem p21024 : ∀ {N : ℕ} [NeZero N] {R : Type u_1} [CommRing R] (f g : ZMod N → R), ∑ x, f x * (g (x + (1 : ZMod N)) - g (x - (1 : ZMod N))) = -∑ x, (f (x + (1 : ZMod N)) - f (x - (1 : ZMod N))) * g x ∧ ∑ x, f x * (g (x + (1 : ZMod N)) - g x) = -∑ x, (f x - f (x - (1 : ZMod N))) * g x :=25 @FRC.GravML.central_difference_adjoint26set_option linter.defProp false in27/-- p21031 — 21:C16. The order-one constants are determined: $c_S'=\tfrac14$ (the $Q_4$ gauge quotient, counted on an instantiated shell and carried by the Carrier identity), the floor's $2\pi$ the full cycle of the angle--count dictionary (14:B2), its threshold the realisation 32:B3, the recurring constant the solid angle $4\pi$, reducing in the Carrier register to the calibration congruence $(4S)^{2}\equiv1$ (one residue relation). -/28def p21031 := And.intro @FRC.GravML.calibration_congruence (@FRC.GravML.newton_register)29/-- p21035 — 21:C20. The two-shift update law: kick (finite Fourier shift by the source character) composed with metaplectic transport gives $\Delta^{2}_{\tau}q=-\nabla u$ with $m$ cancelling --- registered inertia and the equivalence principle inside one derived law. -/30theorem p21035 : ∀ {N : ℕ} [NeZero N] {R : Type u_1} [CommRing R] (ζ : R), ζ ^ N = (1 : R) → ∀ (f : ZMod N → R) (a k : ZMod N), FRC.GravML.dft ζ (fun x => ζ ^ (a.val * x.val) * f x) k = FRC.GravML.dft ζ f (k + a) ∧ FRC.GravML.dft ζ (fun x => f (x - a)) k = ζ ^ (a.val * k.val) * FRC.GravML.dft ζ f k :=31 @FRC.GravML.shift_theorem32/-- p21040 — 21:C25. The PPN triangle closed by two routes: channel unity gives $\gamma=1$ (C7), the instance cover forces $2\gamma-\beta=1$ (A9), jointly $\beta=1$ --- Proposition~\ref{prop:ppn} reached independently, the deviation $\tfrac23(2\gamma-\beta-1)$ its falsifier. -/33theorem p21040 : ∀ (β γ : ℚ), (((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) = (2 : ℚ) ↔ (2 : ℚ) * γ - β = (1 : ℚ)) ∧ ((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) - (2 : ℚ) = (2 / 3 : ℚ) * ((2 : ℚ) * γ - β - (1 : ℚ)) ∧ (γ = (1 : ℚ) → ((1 : ℚ) + γ) / (2 : ℚ) = (1 : ℚ) ∧ ((2 : ℚ) * γ - β = (1 : ℚ) → β = (1 : ℚ) ∧ ((2 : ℚ) + (2 : ℚ) * γ - β) / (3 : ℚ) = (1 : ℚ))) :=34 @FRC.GravML.cover_forcing35/-- p38022 — 38:C7. The two faces of the leak: angular $\kap/\dS$ (the curl), temporal $\kap/(2\dS)$ (the ring, on $C_{464}$); ratio exactly $2$, the double cover. -/36theorem p38022 : ∀ (κ S rg psl : ℚ), κ ≠ (0 : ℚ) → S ≠ (0 : ℚ) → rg ≠ (0 : ℚ) → psl ≠ (0 : ℚ) → ((3 / 2 : ℚ) * (rg / psl) = κ / ((2 : ℚ) * S) ↔ psl = (3 : ℚ) * (S / κ) * rg) ∧ (psl = (3 : ℚ) * (S / κ) * rg → (3 : ℚ) * rg / psl = κ / S ∧ psl / rg = (3 : ℚ) * S / κ) ∧ κ / S / (κ / ((2 : ℚ) * S)) = (2 : ℚ) ∧ (3 : ℚ) * (58 : ℚ) / (3 : ℚ) = (58 : ℚ) ∧ (3 : ℚ) * (58 : ℚ) / (1 : ℚ) = (174 : ℚ) :=37 @FRC.GravML.registration_dictionary38/-- p38023 — 38:C8. The face-ratio identity, orbit-free (both sides' scales cancel): the pair's two faces (C7) have ratio exactly $2$; read in the comparison chart of the laboratory dictionary (C12), the parametrised isotropic metric [approx: continuum chart], the identity forces $2\gamma-\beta=1$, a combination measured to $10^{-4}$ (Cassini, lunar laser ranging) and so discriminating no metric the data have not already selected; Brans--Dicke's $2\gamma-\beta-1=-2/(2+\omega)$ is the same fact read in one family. -/39theorem p38023 : ∀ (β γ : ℚ), ((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) = (2 / 3 : ℚ) * ((2 : ℚ) + (2 : ℚ) * γ - β) ∧ ((2 / 3 : ℚ) * ((2 : ℚ) + (2 : ℚ) * γ - β) = (2 : ℚ) ↔ (2 : ℚ) * γ - β = (1 : ℚ)) ∧ (2 / 3 : ℚ) * ((2 : ℚ) + (2 : ℚ) * γ - β) - (2 : ℚ) = (2 / 3 : ℚ) * ((2 : ℚ) * γ - β - (1 : ℚ)) ∧ (2 : ℚ) * (1 : ℚ) - (1 : ℚ) = (1 : ℚ) ∧ (∀ (ω : ℚ), (2 : ℚ) + ω ≠ (0 : ℚ) → (2 : ℚ) * (((1 : ℚ) + ω) / ((2 : ℚ) + ω)) - (1 : ℚ) - (1 : ℚ) = (-2 : ℚ) / ((2 : ℚ) + ω) ∧ (2 / 3 : ℚ) * ((2 : ℚ) * (((1 : ℚ) + ω) / ((2 : ℚ) + ω)) - (1 : ℚ) - (1 : ℚ)) = (-4 : ℚ) / ((3 : ℚ) * ((2 : ℚ) + ω)) ∧ (-2 : ℚ) / ((2 : ℚ) + ω) ≠ (0 : ℚ)) ∧ ∀ (ε : ℚ), (0 : ℚ) < ε → ∃ W, ∀ (ω : ℚ), W < ω → |(-2 : ℚ) / ((2 : ℚ) + ω)| < ε :=40 @FRC.GravML.ppn_faces41-- end keys4243end FRC.LedgerML44