S13.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Chart3import FrcLedger.Theme.Gravity4import FrcLedger.Keys.Chart5import FrcLedger.Keys.Gravity67/-!8# 38-s13 — the paper module on Mathlib: the chart rows' declarations under the paper's name (12 October 2026)910Rows of the predicate ledger of *The Light Cone of the Minimal Pair* (tree `38-s13-20260801`) whose content is read11against the continuum: the face-ratio identity and the Brans–Dicke exclusion over `ℚ` (C8), the registration12dictionary (C12, C7) — both `FrcLedger/Theme/Gravity.lean` (`FRC.GravML.ppn_faces`, `registration_dictionary`) — and13the floor and its running (P1, X3) and the radial ladder (B2) in `FrcLedger/Theme/Chart.lean` (`FRC.Chart.floor_value`,14`running_floor`, the master's L1 and P1; `ladder_monotone`). Every name here is an alias; the exact content of the paper is the core's (`FrcCore/S13.lean`15and the themes it cites).16-/1718namespace FRC.S131920open Real2122/-! ## Old names (12 October 2026): every declaration of this module is an alias of a theme's (`FRC.GravML`, `FRC.Chart`),23under the paper's name -/2425/-- 38:C8 — the face-ratio identity of the PPN family and the Brans–Dicke exclusion (`FRC.GravML.ppn_faces`,26`Theme/Gravity.lean`). -/27theorem ppn_faces (β γ : ℚ) :28    (2 - β + 2 * γ) / (3 / 2) = 2 / 3 * (2 + 2 * γ - β) ∧29    (2 / 3 * (2 + 2 * γ - β) = 2 ↔ 2 * γ - β = 1) ∧30    2 / 3 * (2 + 2 * γ - β) - 2 = 2 / 3 * (2 * γ - β - 1) ∧31    (2 * (1 : ℚ) - 1 = 1) ∧32    (∀ ω : ℚ, 2 + ω ≠ 0 → 2 * ((1 + ω) / (2 + ω)) - 1 - 1 = -2 / (2 + ω) ∧33      2 / 3 * (2 * ((1 + ω) / (2 + ω)) - 1 - 1) = -4 / (3 * (2 + ω)) ∧ -2 / (2 + ω) ≠ 0) ∧34    (∀ ε : ℚ, 0 < ε → ∃ W : ℚ, ∀ ω : ℚ, W < ω → |(-2 : ℚ) / (2 + ω)| < ε) :=35  FRC.GravML.ppn_faces β γ3637/-- 38:C12, 38:C7 — the registration dictionary `p_sl = 3 (S/κ) r_g` and the two faces38(`FRC.GravML.registration_dictionary`, `Theme/Gravity.lean`). -/39theorem registration_dictionary (κ S rg psl : ℚ) (hκ : κ ≠ 0) (hS : S ≠ 0) (hrg : rg ≠ 0) (hpsl : psl ≠ 0) :40    ((3 / 2) * (rg / psl) = κ / (2 * S) ↔ psl = 3 * (S / κ) * rg) ∧41    (psl = 3 * (S / κ) * rg → 3 * rg / psl = κ / S ∧ psl / rg = 3 * S / κ) ∧42    (κ / S) / (κ / (2 * S)) = 2 ∧ 3 * (58 : ℚ) / 3 = 58 ∧ 3 * (58 : ℚ) / 1 = 174 :=43  FRC.GravML.registration_dictionary κ S rg psl hκ hS hrg hpsl4445/-- 38:P1, 38:X3, 38:C11 — the floor `a₀ = cH₀/2π` at `H₀ = 67.4 km s⁻¹ Mpc⁻¹` (`FRC.Chart.floor_value`,46`Theme/Chart.lean`; the master's L1). -/47theorem floor_value (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) :48    (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.05e-10 ∧49    (0.868 : ℝ) < c * H0 / (2 * π) / 1.2e-10 ∧ c * H0 / (2 * π) / 1.2e-10 < 0.870 ∧50    (0.65 : ℝ) < (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 ∧51    (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 < 0.67 :=52  FRC.Chart.floor_value c H0 hc hH5354/-- 38:P1 — the running floor tracks the registered rate, `a₀(z)/a₀(0) = H(z)/H(0)` (`FRC.Chart.running_floor`,55`Theme/Chart.lean`; the master's P1). -/56theorem running_floor (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ) (hc : 0 < c) (hG : 0 < G) (hM : 0 < M)57    (h0 : 0 < H 0) (hz : 0 < H z) (ha : ∀ z, a z = c * H z / (2 * π)) (hv0 : 0 < v 0) (hvz : 0 < v z)58    (htf : ∀ z, v z ^ 4 = G * M * a z) :59    a z / a 0 = H z / H 0 ∧ v z / v 0 = (H z / H 0) ^ (1 / 4 : ℝ) :=60  FRC.Chart.running_floor c G M H a v z hc hG hM h0 hz ha hv0 hvz htf6162/-- 38:B2 [chart] — the radial ladder `R sin(2aπ/13)`, `a = 1, 2, 3`, positive, increasing, inside the rim63(`FRC.Chart.ladder_monotone`, `Theme/Chart.lean`). -/64theorem ladder_monotone (R : ℝ) (hR : 0 < R) :65    0 < R * Real.sin (2 * π / 13) ∧ R * Real.sin (2 * π / 13) < R * Real.sin (4 * π / 13) ∧66    R * Real.sin (4 * π / 13) < R * Real.sin (6 * π / 13) ∧ R * Real.sin (6 * π / 13) < R :=67  FRC.Chart.ladder_monotone R hR686970-- Ledger predicates of 38-s13 (generated by make_predicates.py from docs/38-s13/38-s13-ledger.json; edit the ledger, not this section)71/-- 38:B2 (p38010) — The radial ladder: shells at $R\sin(2a\pi/13)$ [chart]; capacity $4a<\p\Leftrightarrow a\le\kap$. -/72theorem p38010 : ∀ (R : ℝ), (0 : ℝ) < R → (0 : ℝ) < R * Real.sin ((2 : ℝ) * Real.pi / (13 : ℝ)) ∧ R * Real.sin ((2 : ℝ) * Real.pi / (13 : ℝ)) < R * Real.sin ((4 : ℝ) * Real.pi / (13 : ℝ)) ∧ R * Real.sin ((4 : ℝ) * Real.pi / (13 : ℝ)) < R * Real.sin ((6 : ℝ) * Real.pi / (13 : ℝ)) ∧ R * Real.sin ((6 : ℝ) * Real.pi / (13 : ℝ)) < R :=73  @FRC.LedgerML.p3801074/-- 38:C7 (p38022) — 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. -/75theorem 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 : ℚ) :=76  @FRC.LedgerML.p3802277/-- 38:C8 (p38023) — 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. -/78theorem 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 : ℚ) + ω)| < ε :=79  @FRC.LedgerML.p3802380/-- 38:X3 (p38048) — \textbf{The acceleration floor $a_{0}=cH_{0}/2\pi$ is the drive seen in the chart}: the leak's cyclic rate is the drive's own, one cycle per drive period $\Om-1$ chronons $=2\pi/H_{0}$, and its acceleration face is the floor (C10; C11, the realisation); at the instance $a_{0}=c/(\Om-1)$. -/81theorem p38048 : ∀ (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 :=82  @FRC.LedgerML.p3804883/-- 38:P1 (p38049) — The registration floor $a_{0}=cH_{0}/2\pi$, read from the pair's $\kap$-free per-chronon leak rate (C11): parameter-free, tracking $H(z)$. Falsifier: a measured floor off $cH_{0}/2\pi$ beyond the $H_{0}$ uncertainty, or one not tracking $H(z)$ (\S\ref{sec:predictions}, item 5; the dark sector's L1). -/84theorem p38049 : (∀ (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) ∧ ∀ (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < M → (0 : ℝ) < H (0 : ℝ) → (0 : ℝ) < H z → (∀ (z : ℝ), a z = c * H z / ((2 : ℝ) * Real.pi)) → (0 : ℝ) < v (0 : ℝ) → (0 : ℝ) < v z → (∀ (z : ℝ), v z ^ (4 : ℕ) = G * M * a z) → a z / a (0 : ℝ) = H z / H (0 : ℝ) ∧ v z / v (0 : ℝ) = (H z / H (0 : ℝ)) ^ (1 / 4 : ℝ) :=85  @FRC.LedgerML.p3804986-- end ledger predicates8788end FRC.S1389