The Lean module lean/FrcMathlib/Spacetime.lean of the paper 7-st (on Mathlib; the index of the library's modules): 4 theorems (0 definitions): 0 with no axioms, 0 at tier 1 (propext, Quot.sound), 4 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 Mathlib2import FrcMathlib.Theme.Lorentz3import FrcMathlib.Keys.Projective4import FrcMathlib.Theme.Chart5import FrcMathlib.Keys.Chart67/-!8# 7-spacetime — the paper module on Mathlib: the row proved on Mathlib's hierarchy under the paper's name (31 October 2026)910The one row of the predicate ledger of *Emergent Lorentzian Space-Time over Finite Holographic Substrate* (tree11`7-spacetime-20261027`) that the core does not reach: no definite space (D5), every three-dimensional subspace of the12register square contains a null vector, by the Chevalley–Warning theorem (`FrcMathlib/Theme/Lorentz.lean`,13`FRC.Lorentz.isotropic_three`). Every name here is an alias; the exact content of the paper is the core's14(`FrcCore/Spacetime.lean` and the themes it cites).15-/1617namespace FRC.Spacetime1819/-! ## Old names (ledger migration convention): the paper's name for the theme's theorem (`FRC.Lorentz.isotropic_three`,20`FrcMathlib/Theme/Lorentz.lean`), which `make_keys.py` follows to the theme so the key `FRC.LedgerML.p07015` is written in21`Keys/Projective.lean`; the predicate below is the key's alias -/2223/-- 7:D5 — **no definite space**: for every prime shell `p`, every `ν` and any three vectors `u, v, w` of `𝔽_p⁴`, some24nonzero coefficient triple gives a null vector of the determinant form `x₀² − x₁² − x₃² + ν x₂²` in their span —25every three-dimensional subspace of the register square contains a null vector (`FRC.Lorentz.isotropic_three`,26`Theme/Lorentz.lean`, by Chevalley–Warning). -/27
theorem isotropic_three {p : ℕ} [Fact p.Prime] (ν : ZMod p) (u v w : Fin 4 → ZMod p) :28 ∃ a : Fin 3 → ZMod p, a ≠ 0 ∧ FRC.Lorentz.Qf ν (a 0 • u + a 1 • v + a 2 • w) = 0 :=29 FRC.Lorentz.isotropic_three ν u v w3031/-- 7:A31, 21:P3 — **the floor's number**: `a₀ = cH₀/2π` lies between `1.04` and `1.05 × 10⁻¹⁰ m s⁻²` at the declared32`c` and `H₀ = 67.4`, 13 % below the fitted `1.20 × 10⁻¹⁰` and 0.65–0.67 of its systematic `0.24 × 10⁻¹⁰`33(`FRC.Chart.floor_value`, `Theme/Chart.lean`, as 21-gravity cites it under `FRC.Gravity.floor_value`); the identity behind the34number, `a₀ τ = c H`, is the core's `FRC.Drift.floor_period`. -/35theorem floor_value (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) :36 (1.04e-10 : ℝ) < c * H0 / (2 * Real.pi) ∧ c * H0 / (2 * Real.pi) < 1.05e-10 ∧37 (0.868 : ℝ) < c * H0 / (2 * Real.pi) / 1.2e-10 ∧ c * H0 / (2 * Real.pi) / 1.2e-10 < 0.870 ∧38 (0.65 : ℝ) < (1.2e-10 - c * H0 / (2 * Real.pi)) / 0.24e-10 ∧39 (1.2e-10 - c * H0 / (2 * Real.pi)) / 0.24e-10 < 0.67 :=40 FRC.Chart.floor_value c H0 hc hH4142-- Ledger predicates of 7-spacetime (generated by make_predicates.py from docs/7-spacetime/7-spacetime-ledger.json; edit the ledger, not this section)43/-- 7:A31 (p21052) — The weak-acceleration floor of registration against the drift is $a_{0}=c/T_H=cH_{0}/2\pi$, with $T_H=2\pi/H_{0}$ the drive period by the angle--count dictionary: $1.04\times10^{-10}$ m\,s$^{-2}$ at $H_{0}=67.4$ km\,s$^{-1}$\,Mpc$^{-1}$, against the fitted $1.20\pm0.24\times10^{-10}$ [chart]. -/44theorem weak_acceleration_floor : ∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 105e-12 ∧ 0.868 < c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 ∧ c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 < 0.870 ∧ 0.65 < (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 ∧ (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 < 0.67 :=45 @FRC.LedgerML.p2105246/-- 7:D5 (p07015) — No definite space: every three-dimensional subspace of the register square contains a null vector. -/47theorem no_definite_space : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (ν : ZMod p) (u v w : Fin (4 : ℕ) → ZMod p), ∃ a, a ≠ (0 : Fin (3 : ℕ) → ZMod p) ∧ FRC.Lorentz.Qf ν (a (0 : Fin (3 : ℕ)) • u + a (1 : Fin (3 : ℕ)) • v + a (2 : Fin (3 : ℕ)) • w) = (0 : ZMod p) :=48 @FRC.LedgerML.p0701549-- end ledger predicates5051end FRC.Spacetime52