Master.lean — FrcMathlib

1import FrcMathlib.Keys.Chart23/-!4# FrcMathlib.Master — the master ledger's predicate declarations on Mathlib (8 November 2026)56One declaration per master row whose chart clauses a block file binds to Mathlib theorems (`frc/ledgers/master/<theme>.py`,7CHART), `FRC.Master.<name>`, named by the row's declared name (`name:` in `00-master/predicates/index.md`), each the alias of the8row's key `FRC.LedgerML.p<key>` in Mathlib's key files, which `make_keys.py` writes from the same bindings; the key stands in9the docstring. Generated by `make_master.py`; the theorems live in the chart theme, the keys in `Keys/`.10-/1112namespace FRC.Master1314-- Ledger predicates of 00-ledger (generated by make_master.py from docs/00-ledger.json, docs/predictions.json and the key files; edit the ledger, not this file)15/-- 00:A7 (p00009) — Scale, the sole quantitative import: the de Sitter entropy of the observable universe fixes the cardinality exactly, $\Om=4\dS+1$. Its chart numeral is $\dS=\pi(r_H/\ell_P)^2=3.3\times10^{122}$ [chart] at $r_H=c/H_\Lambda$ (14-entr), so $\Om=1.3\times10^{123}$ [chart]. The Carrier congruences are certified by the realisations (B5, C8), not imported. Metrology: L2. -/16theorem scale_import : ∀ (Λ ℓP r S Ω : ℝ), Λ = 1088e-55 → ℓP = 1616255e-41 → r ^ (2 : ℕ) = (3 : ℝ) / Λ → S = Real.pi * (r / ℓP) ^ (2 : ℕ) → Ω = (4 : ℝ) * S + (1 : ℝ) → 331e120 < S ∧ S < 332e120 ∧ 132e121 < Ω ∧ Ω < 133e121 :=17  @FRC.LedgerML.p0000918/-- 00:P1 (p00133) — The acceleration floor tracks the drive rate, $a_0(z)\propto H(z)$: a relation, $\Om$-blind, derived from X1 under the gauge principle (D5); the knee shifts and the Tully--Fisher zero-point evolves as $E(z)^{1/4}$. Falsifier: a floor constant in redshift, or tracking other than $H(z)$. Confrontation (43-muse): MUSE-DARK III excludes a constant floor to $z=1.3$; RC100 implies the local floor by $z\simeq2$, pending refit. -/19theorem floor_tracks_drive_rate : ∀ (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 : ℝ) :=20  @FRC.LedgerML.p0013321/-- 00:P3 (p00180) — \textbf{Flavour} (targets): the Georgi--Jarlskog double ratio $9$; the locks of G17 read in the $\overline{\mathrm{MS}}$ scheme; the $m_1{=}0$ floor, $\sum m_\nu=58.8$ meV at NuFIT 6.0, on the boundary-branch realisation (28:B6). Falsifier: inverted ordering, a degenerate spectrum, or $\sum m_\nu$ off $58.8$ meV beyond the fit's tolerance. Confrontation: the data give $10.4\pm0.5$, an open $15\%$ tension (28:X5). -/22theorem flavour_targets : (∀ (me mmu md ms : ℚ), me = 0.51099895 → mmu = 105.6583755 → md = 4.67 → ms = 93.4 → 10.3 < mmu / me / (ms / md) ∧ mmu / me / (ms / md) < 10.5 ∧ (9 : ℚ) * 1.10 < mmu / me / (ms / md) ∧ mmu / me / (ms / md) < (9 : ℚ) * 1.20) ∧ ∀ (dm21 dm31 : ℝ), dm21 = 749e-7 → dm31 = 2513e-6 → 587e-4 < √dm21 + √dm31 ∧ √dm21 + √dm31 < 589e-4 :=23  @FRC.LedgerML.p0018024/-- 00:P4 (p00091) — No fourth generation, no fifth force, an empty desert, no TeV supersymmetry, no new dark-matter particle, no beyond-SM $(g{-}2)_\mu$, and the proton effectively stable ($\tau_p\gtrsim10^{45}$ yr; G9). Entailed by the closed ladder of the rank-five frame ($\dim\Lambda^{\mathrm{even}}=16$, D6), given the role-to-matter realisation (27:B6, 27:C10) and completeness (A3). Falsifier: any excluded object observed. Confrontation: none observed. -/25theorem empty_desert : (∀ (ainv s2 as b1 b2 b3 MZ : ℝ), ainv = 127.951 → s2 = 0.23121 → as = 0.1179 → b1 = (41 / 10 : ℝ) → b2 = (-19 / 6 : ℝ) → b3 = (-7 : ℝ) → MZ = 91.1876 → |(1 : ℝ) / as - b3 * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2)) - (s2 * ainv - b2 * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2)))| / (s2 * ainv - b2 * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2))) < (1 / 5 : ℝ) ∧ (10 : ℝ) ^ (12 : ℕ) < MZ * Real.exp ((2 : ℝ) * Real.pi * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2))) ∧ MZ * Real.exp ((2 : ℝ) * Real.pi * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2))) < (10 : ℝ) ^ (14 : ℕ)) ∧ (∀ (mp a hbar yr : ℚ), mp = 0.938 → a = (1 / 40 : ℚ) → hbar = 6582e-28 → yr = 3156e4 → (10 : ℚ) ^ (45 : ℕ) ≤ 122e17 ^ (4 : ℕ) / (a ^ (2 : ℕ) * mp ^ (5 : ℕ)) * hbar / yr ∧ (10 : ℚ) ^ (34 : ℕ) < 1e16 ^ (4 : ℕ) / (a ^ (2 : ℕ) * mp ^ (5 : ℕ)) * hbar / yr ∧ ∀ (M M' : ℚ), (0 : ℚ) < M → (0 : ℚ) < M' → M' ^ (4 : ℕ) / (a ^ (2 : ℕ) * mp ^ (5 : ℕ)) * hbar / yr / (M ^ (4 : ℕ) / (a ^ (2 : ℕ) * mp ^ (5 : ℕ)) * hbar / yr) = (M' / M) ^ (4 : ℕ)) ∧ StrictMonoOn (fun x => x / ((1 : ℝ) - Real.exp (-√x))) (Set.Ioi (0 : ℝ)) :=26  @FRC.LedgerML.p0009127/-- 00:P5 (p00201) — \textbf{The eikonal pair}: on the exponential reading (E4) the photon sphere sits at $r_c=2M$, $b_c=2eM$, and the orbital rate equals the Lyapunov rate, $\Omega_c=\lambda=1/(2eM)$, both $3\sqrt3/(2e)$ of Schwarzschild's. The wave operator's $\ell=2$ mode (E13) is $(0.4641-0.0923\,i)/M$ [approx]. Falsifier: the remnant's $(2,2,0)$ oscillation at that mode, $+24\%$ against Kerr. Confrontation: GW250114 [import] excludes that reading; the $(2,2,0)$ reading is open (21:P1). -/28theorem eikonal_pair_phase_mode : (∀ (M : ℝ), (0 : ℝ) < M → (∀ (r : ℝ), r ≠ (0 : ℝ) → HasDerivAt (fun r => r ^ (2 : ℕ) * Real.exp ((4 : ℝ) * M / r)) (Real.exp ((4 : ℝ) * M / r) * ((2 : ℝ) * r - (4 : ℝ) * M)) r) ∧ (∀ (r : ℝ), Real.exp ((4 : ℝ) * M / r) * ((2 : ℝ) * r - (4 : ℝ) * M) = (0 : ℝ) ↔ r = (2 : ℝ) * M) ∧ (∀ (r : ℝ), r ≠ (0 : ℝ) → HasDerivAt (fun r => Real.exp ((4 : ℝ) * M / r) * ((2 : ℝ) * r - (4 : ℝ) * M)) (Real.exp ((4 : ℝ) * M / r) * ((2 : ℝ) - (4 : ℝ) * M * ((2 : ℝ) * r - (4 : ℝ) * M) / r ^ (2 : ℕ))) r) ∧ Real.exp ((4 : ℝ) * M / ((2 : ℝ) * M)) * ((2 : ℝ) - (4 : ℝ) * M * ((2 : ℝ) * ((2 : ℝ) * M) - (4 : ℝ) * M) / ((2 : ℝ) * M) ^ (2 : ℕ)) = (2 : ℝ) * Real.exp (2 : ℝ) ∧ ((2 : ℝ) * M) ^ (2 : ℕ) * Real.exp ((4 : ℝ) * M / ((2 : ℝ) * M)) = ((2 : ℝ) * Real.exp (1 : ℝ) * M) ^ (2 : ℕ) ∧ Real.exp (-((4 : ℝ) * M / ((2 : ℝ) * M))) * ((2 : ℝ) * Real.exp (2 : ℝ)) / ((2 : ℝ) * (((2 : ℝ) * M) ^ (2 : ℕ) * Real.exp ((4 : ℝ) * M / ((2 : ℝ) * M)))) = ((1 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ) * M)) ^ (2 : ℕ) ∧ (1 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ) * M) / ((1 : ℝ) / ((3 : ℝ) * √(3 : ℝ) * M)) = (3 : ℝ) * √(3 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ))) ∧ 1.0462 < (2 : ℝ) * Real.exp (1 : ℝ) / ((3 : ℝ) * √(3 : ℝ)) ∧ (2 : ℝ) * Real.exp (1 : ℝ) / ((3 : ℝ) * √(3 : ℝ)) < 1.0463 ∧ 0.9557 < (3 : ℝ) * √(3 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ)) ∧ (3 : ℝ) * √(3 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ)) < 0.9558 ∧ 2.46 < ((4 : ℝ) * Real.exp (1 : ℝ) - (6 : ℝ) * √(3 : ℝ)) * 5.12 ∧ ((4 : ℝ) * Real.exp (1 : ℝ) - (6 : ℝ) * √(3 : ℝ)) * 5.12 < 2.47 :=29  @FRC.LedgerML.p0020130/-- 00:X1 (p00192) — The synchronisation floor $a_0=cH_0/2\pi$ fixes the acceleration scale parameter-free: the $2\pi$ by the angle--count dictionary (14:B2), the threshold one cycle per drive period (32:B3), $1.04\times10^{-10}$ [chart] at the channel-1 $H_0=67.4$ (X2), tied to $H(z)$, not $\Lambda$ (P1; 21:X1). Below the floor the amplitude reading, given the barrier identification (32:B8, 21:B9), gives the radial acceleration relation unfitted. Falsifiers: 32:B3, 21:P4. -/31theorem cosmology_dark_sector : (∀ (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 H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 1045e-13 :=32  @FRC.LedgerML.p0019233/-- 00:X2 (p00193) — \textbf{The octant record depth and its outputs}: the record depth is bounded by the octant, $\dS/2$ chronons $=13.79$ Gyr ($(\pi/4)r_H/c$, chart), on the octant sector of B14. Zero-freedom: $\Omega_\Lambda=\tanh^2(3\pi/8)=0.684$ (chart; $0.19\sigma$); on the stellar age $13.61\pm0.34$ Gyr, $H_0=68.2\pm1.7$ ($2.4\sigma$ from the ladder); $w=-1$ rigid --- a confirmed drift falsifies $\Lambda\sim1/\Om$. Falsifiers: octant-capped ages, the running floor $a_0(z)\propto H(z)$ (Z7), the ladder bias. -/34theorem octant_record_depth : (∀ (S r c : ℝ), S ≠ (0 : ℝ) → S / (2 : ℝ) / ((4 : ℝ) * S) * ((2 : ℝ) * Real.pi * r / c) = Real.pi / (4 : ℝ) * r / c) ∧ (0.68368 < Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) ∧ Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) < 0.68369 ∧ 0.18 * 7e-3 < 0.685 - Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) ∧ 0.685 - Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) < 0.19 * 7e-3) ∧ (0.186 * 7e-3 < 0.685 - Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) ∧ 0.685 - Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) < 0.19 * 7e-3) ∧ (∀ (t H0 HΛ Ω : ℝ), t * HΛ = Real.pi / (4 : ℝ) → HΛ = H0 * √Ω → Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) → t * H0 = Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ))) ∧ (0.9498 < Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ∧ Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) < 0.9499) ∧ (FRC.Chart.lcdmAge (Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) = Real.pi / (4 : ℝ) ∧ ∀ (Ω : ℝ), (0 : ℝ) ≤ Ω → Ω < (1 : ℝ) → FRC.Chart.lcdmAge Ω = Real.pi / (4 : ℝ) → Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) ∧ (∀ (t H0 : ℝ), t = 1379e7 * (365.25 * (86400 : ℝ)) → t * H0 = Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) → 67.35 < H0 * 30856775814913673e3 ∧ H0 * 30856775814913673e3 < 67.36) ∧ ∀ (t H0 : ℝ), t = 1361e7 * (365.25 * (86400 : ℝ)) → t * H0 = Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) → 68.24 < H0 * 30856775814913673e3 ∧ H0 * 30856775814913673e3 < 68.25 ∧ 1.70 < H0 * 30856775814913673e3 * (0.34 / 13.61) ∧ H0 * 30856775814913673e3 * (0.34 / 13.61) < 1.71 ∧ 2.40 < (73.0 - H0 * 30856775814913673e3) / √(1.7 ^ (2 : ℕ) + 1.0 ^ (2 : ℕ)) ∧ (73.0 - H0 * 30856775814913673e3) / √(1.7 ^ (2 : ℕ) + 1.0 ^ (2 : ℕ)) < 2.42 :=35  @FRC.LedgerML.p0019336/-- 00:X3 (p00087) — The mass--radius chart between the Compton and Schwarzschild walls, closed by the Planck apex and the totality wall $r_H$: the totality on its own horizon, the black-hole reading dissolved (A2). Width $61.0$ dex. The over-closure bound ${\sim}1.8\times10^{8}M_\odot$ is the chart's one derived quantity, a bound, predicting no observed scale (14:C9, X5). A consistency chart, not a channel (L2). Falsifier: a single typical object of the condensed-density sequence heavier than the over-closure bound and not horizon-bound (14:X5). -/37theorem registrable_triangle_realisation : (∀ (S x : ℝ), (0 : ℝ) < x → S = Real.pi * x ^ (2 : ℕ) → x = √(S / Real.pi) ∧ √S = √Real.pi * x) ∧ ∀ (M R G c ρ₀ : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < M → M = ρ₀ * R ^ (3 : ℕ) → R = (2 : ℝ) * G * M / c ^ (2 : ℕ) → (0 : ℝ) < ρ₀ ∧ M ^ (2 : ℕ) = c ^ (6 : ℕ) / ((8 : ℝ) * G ^ (3 : ℕ) * ρ₀) :=38  @FRC.LedgerML.p0008739/-- 00:Y10 (p00148) — $n_s=1$ is the scale-dilation fixed point (Harrison--Zel'dovich [import]). The tilt's committed form is $n_s-1=-\pi^2/\ln\Om$ [chart], $\ln\Om$ the e-fold count of the frame's scale range from $1/\sqrt\Om$ to $\sqrt\Om$, a hypothesis fixed by the measured tilt: $-0.0348$ [approx] at $\ln\Om=283.5$ (A7), $+0.07\sigma$ from Planck 2018's $-0.0351\pm0.0042$ [import]. The count $\tfrac12\ln\Om$ is excluded at $8.2\sigma$. Falsifier: a Planck-resolution deviation from $-\pi^2/\ln\Om$. -/40theorem primordial_tilt_realisation : (3481e-5 < Real.pi ^ (2 : ℕ) / 283.5 ∧ Real.pi ^ (2 : ℕ) / 283.5 < 3482e-5 ∧ 68e-3 * 42e-4 < 351e-4 - Real.pi ^ (2 : ℕ) / 283.5 ∧ 351e-4 - Real.pi ^ (2 : ℕ) / 283.5 < 69e-3 * 42e-4 ∧ 8.2 * 42e-4 < Real.pi ^ (2 : ℕ) / (283.5 / (2 : ℝ)) - 351e-4 ∧ Real.pi ^ (2 : ℕ) / (283.5 / (2 : ℝ)) - 351e-4 < 8.25 * 42e-4) ∧ ∀ (Ω : ℝ), (0 : ℝ) < Ω → Real.log (√Ω / ((1 : ℝ) / √Ω)) = Real.log Ω :=41  @FRC.LedgerML.p0014842-- end ledger predicates4344end FRC.Master45