Keys/Chart.lean — FrcLedger

1import FrcLedger.Theme.Gravity2import FrcLedger.Theme.Quantum3import FrcLedger.Theme.Horizon4import FrcLedger.Theme.Chart5import FrcLedger.Theme.Strong67/-!8# FrcLedger.Keys.Chart — the keyed theorems of the chart theme (ledger migration, task LM19)910One declaration per key, `FRC.LedgerML.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem11that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration12`FRC.<Module>.p<key>` as an alias. Every declaration has the axioms of Mathlib's hierarchy at most (`check_axioms.py`).13-/1415namespace FRC.LedgerML1617-- Keys of the chart theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)18/-- p00009 — 00:A7. 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. -/19theorem p00009 : ∀ (Λ ℓ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 :=20  @FRC.Chart.scale_import21/-- p00133 — 00:P1. The acceleration floor tracks the drive rate, $a_0(z)\propto H(z)$: a relation, $\Om$-blind, derived from L1 under the gravity realisation (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. -/22theorem p00133 : ∀ (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 : ℝ) :=23  @FRC.Chart.running_floor24/-- p00148 — 00:L8. $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 realisation 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$. -/25theorem p00148 : (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 Ω :=26  And.intro @FRC.Chart.tilt_ledger (@FRC.Chart.efold_count)27/-- p00192 — 00:L1. 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$ (L3), 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. -/28theorem p00192 : (∀ (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 :=29  And.intro @FRC.Chart.floor_value (@FRC.Chart.floor_fine)30/-- p00193 — 00:L3. \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. -/31theorem p00193 : (∀ (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 :=32  And.intro @FRC.Chart.octant_chart (And.intro @FRC.Chart.landing_bracket (And.intro @FRC.Chart.landing_fine (And.intro @FRC.Chart.age_rate_locus (And.intro @FRC.Chart.locus_bracket (And.intro @FRC.Chart.octant_inversion (And.intro @FRC.Chart.hubble_landing (@FRC.Chart.hubble_stellar)))))))33/-- p00201 — 00:E14. \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], $0.8\%$ above the eikonal $(\ell+\tfrac12)/(2eM)$. Falsifier: that mode read as the remnant's $(2,2,0)$ oscillation, $+24\%$ against Kerr, excluded by GW250114 [import]. -/34theorem p00201 : (∀ (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 :=35  And.intro @FRC.Strong.eikonal_pair (@FRC.Strong.shadow_bracket)36/-- p14038 — 14:P3. The age--rate locus $t_{\mathrm{age}}H_0=(\pi/4)/\tanh(3\pi/8)=0.950$, exact for the realisation set. Read on the fit-independent stellar age ($13.61\pm0.34$ Gyr): $H_0=68.2\pm1.7$ km/s/Mpc \apx, $0.5\sigma$ from Planck, $0.65\sigma$ from TRGB, $2.4\sigma$ from the Cepheid ladder --- the framework favours the CMB/TRGB value at that significance, and forbids the $\Omega_\Lambda\approx0.76$ by which the rival chart would accommodate the ladder value at the same age. Read on the channel-1 $\Lambda$ it returns the channel-1 $H_0$ (to $0.1\%$): a consistency, not a prediction (C8). Falsifier: a confirmed ladder $H_0$ with the stellar age standing ($t_\star H_0\ge1.0$ against $0.950$). -/37theorem p14038 : (∀ (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 :=38  And.intro @FRC.Chart.age_rate_locus (@FRC.Chart.locus_bracket)39set_option linter.defProp false in40/-- p20032 — 20:E1. The scale-evolution generator: on the shell the scale-shift $x\mapsto\gen^{\,r}x$ is a unitary permutation of $\Fx{\p}$ with the complex characters as eigenvectors; in the analytic chart [chart] the dilation group $U_r=e^{ir\Hh}$ has the self-adjoint generator $\Hh=-i(x\partial_x+\half)$ with generalised eigenfunctions $x^{-\bar\rho}$, $\rho=\half+i\gamma$, the symmetrizing $\half$ the half-turn of B8; the chart assignment is used nowhere as a shell identity. -/41def p20032 := And.intro @FRC.HorizonML.scale_shift (And.intro @FRC.Chart.character_eigen (@FRC.Chart.chi_shift))42set_option linter.defProp false in43/-- p20043 — 20:E12, 00:Z10. \textbf{The shell theorem.} On every shell, with no hypothesis: (i) $v$ expands in the constant mode and the nonterminal modes of the quarter-turn meridian; (ii) every readout lies on $\Tr=1$, real part $2^{-1}=2\kp+1=-\pi$; (iii) the scale-shift has the modes as eigenvectors, eigenphases $2\pi j/(\p-1)$ independent of $v$. No off-line mode; true of every vector, the Davenport--Heilbronn vector included. -/44def p20043 := And.intro @FRC.Chart.chi_inversion (And.intro @FRC.Chart.chi_shift (And.intro @FRC.HorizonML.scale_shift (And.intro @FRC.HorizonML.readout_on_line (@FRC.HorizonML.readout_slot_index))))45set_option linter.defProp false in46/-- p20044 — 20:E13. Shell-basis completeness is not a clause of E12: the $\p-1$ complex characters are an orthogonal basis of $\mathbb C^{\Fx{\p}}$ ($\lVert\chi_j\rVert^{2}=\p-1$; finite Parseval), true of every vector, the trivial character carrying the mean $\psi(\p-1)/(\p-1)$; the $\Fp$-valued power characters are never orthonormal and do not expand $v$; completeness for the zero set of $\zeta$ is D5, a different clause. -/47def p20044 := And.intro @FRC.Chart.chi_orthogonal (And.intro @FRC.Chart.chi_parseval (And.intro @FRC.Chart.chi_inversion (@FRC.HorizonML.power_characters_not_orthonormal)))48/-- p20047 — 20:F1. \textbf{Turing's count on the shell.} On every cell $C_y\le N^{\mathrm{crit}}_y\le\mathcal N_y$ (A7); the cell is clean when $\mathcal N_y=N^{\mathrm{crit}}_y$, and $C_y=\mathcal N_y$ certifies it, every zero simple. The shell estimates $\mathcal N$ by the comb count (Appendix~\ref{app:comb}; uncertified) and reads $C$ from the main sum's sign changes (A10), zeros on the line. An off-line zero is a phantom, $\mathcal N_y-N^{\mathrm{crit}}_y>0$. -/49theorem p20047 : ∀ {a b : ℝ}, a < b → (completedRiemannZeta ((1 / 2 : ℂ) + ↑a * Complex.I)).re * (completedRiemannZeta ((1 / 2 : ℂ) + ↑b * Complex.I)).re < (0 : ℝ) → ∃ t, a < t ∧ t < b ∧ riemannZeta ((1 / 2 : ℂ) + ↑t * Complex.I) = (0 : ℂ) :=50  @FRC.Chart.zero_of_sign_change51set_option linter.defProp false in52/-- p20080 — 20:D8. The strip: the Euler product excludes zeros with real part at least one, and the functional equation confines the nontrivial zeros to the open strip in Klein-four orbits of size two on the line and four off it; the Davenport--Heilbronn vector, without the product, is not multiplicative and has an off-line zero. No core witness: the statement is analytic. -/53def p20080 := @FRC.Chart.zeros_in_strip54set_option linter.defProp false in55/-- p21016 — 21:C1. The linearised dynamics is the gradient flow of a coherence free energy --- its current derived from the pair tally conditional on channel unity (Lemma~\ref{lem:pairtally}) --- and a locked cluster of cardinality $m$ couples with coefficient exactly $m$. -/56def p21016 := @FRC.Strong.locked_sum57/-- p21019 — 21:C4. The equivalence principle as an identity; the bias field is clock rate, giving the redshift $\Delta f/f=Gm/rc^2$; the turnaround radius against the Hubble drive. -/58theorem p21019 : ∀ (u : ℝ), (0 : ℝ) ≤ u → u ≤ (1 : ℝ) → |(1 : ℝ) - Real.exp (-u) - u| ≤ u ^ (2 : ℕ) :=59  @FRC.Strong.redshift_linear60/-- p21020 — 21:C5. The magnitude $G=\hbar c/m_P^2$, frame-covariant (a relativity principle for scale); gravity's weakness is cardinality dilution. -/61theorem p21020 : (∀ (S : ℕ) [Fact (Nat.Prime ((4 : ℕ) * S + (1 : ℕ)))], ∃ r, r ^ (2 : ℕ) = ↑S ∧ ((2 : ZMod ((4 : ℕ) * S + (1 : ℕ))) * r) ^ (2 : ℕ) = (-1 : ZMod ((4 : ℕ) * S + (1 : ℕ)))) ∧ ∀ (m Ω : ℝ), (0 : ℝ) < Ω → (m / √Ω) ^ (2 : ℕ) = m ^ (2 : ℕ) / Ω :=62  And.intro @FRC.GravML.hbar_register (@FRC.Strong.dilution)63/-- p21022 — 21:C7. Channel unity forces the spatial bias to equal the temporal one, $\gamma=1$, restoring the full light deflection $4Gm/c^2b$. -/64theorem p21022 : (∀ (β γ : ℚ), (((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 : ℚ)))) ∧ ∀ (U : ℝ), |U| ≤ (1 / 2 : ℝ) → |Real.exp (-((2 : ℝ) * U)) - (((1 : ℝ) - U / (2 : ℝ)) / ((1 : ℝ) + U / (2 : ℝ))) ^ (2 : ℕ) - U ^ (3 : ℕ) / (6 : ℝ)| ≤ (3 : ℝ) * U ^ (4 : ℕ) ∧ |Real.exp ((2 : ℝ) * U) - ((1 : ℝ) + U / (2 : ℝ)) ^ (4 : ℕ) - U ^ (2 : ℕ) / (2 : ℝ)| ≤ (3 : ℝ) * |U| ^ (3 : ℕ) :=65  And.intro @FRC.GravML.cover_forcing (@FRC.Strong.pn_series)66/-- p21023 — 21:C8. The exponential isotropic metric by multiplicative composition, with $\beta=\gamma=1$: deflection, Shapiro delay, and perihelion at their observed values. -/67theorem p21023 : (∀ (β γ : ℚ), (((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 : ℚ)))) ∧ ∀ (U : ℝ), |U| ≤ (1 / 2 : ℝ) → |Real.exp (-((2 : ℝ) * U)) - (((1 : ℝ) - U / (2 : ℝ)) / ((1 : ℝ) + U / (2 : ℝ))) ^ (2 : ℕ) - U ^ (3 : ℕ) / (6 : ℝ)| ≤ (3 : ℝ) * U ^ (4 : ℕ) ∧ |Real.exp ((2 : ℝ) * U) - ((1 : ℝ) + U / (2 : ℝ)) ^ (4 : ℕ) - U ^ (2 : ℕ) / (2 : ℝ)| ≤ (3 : ℝ) * |U| ^ (3 : ℕ) :=68  And.intro @FRC.GravML.cover_forcing (@FRC.Strong.pn_series)69/-- p21026 — 21:C11. The nonlinear completion forced: the exact cut-flux law (transfer antisymmetry) plus the winding grading forbid independent static self-sourcing, the clock-comparison cocycle makes the exponential reading unique (exactly the character $\gen^{-\Delta n}$, $e^{-u}$ its observer lift), and Deser's bootstrap does not apply because what gravitates is winding rate. -/70theorem p21026 : ∀ (a b : ℝ), Real.exp (-(a + b)) = Real.exp (-a) * Real.exp (-b) ∧ (∀ (U : ℝ), (-2 : ℝ) < U → U < (2 : ℝ) → Real.exp (-((2 : ℝ) * Real.artanh (U / (2 : ℝ)))) = ((1 : ℝ) - U / (2 : ℝ)) / ((1 : ℝ) + U / (2 : ℝ))) ∧ ((1 : ℝ) - (1 / 2 : ℝ)) / ((1 : ℝ) + (1 / 2 : ℝ)) ≠ (((1 : ℝ) - (1 / 2 : ℝ) / (2 : ℝ)) / ((1 : ℝ) + (1 / 2 : ℝ) / (2 : ℝ))) ^ (2 : ℕ) :=71  @FRC.Strong.exponential_reading72/-- p21027 — 21:C12. The exact saturating static profile and its slip core at $r_*=\sqrt{Gm}$: horizonless, operationally black at $r_f=r_s/\ln\Omega$ --- the exact statement the cut form, $4\pi r^{2}$ its [chart] reading; the $r_f$-anchored claims stated in the substrate coordinate, $r_*<r_f<M$ for $M>(\ln\Omega/2)^{2}$ Planck masses (master E10). -/73theorem p21027 : ∀ (M L Ω : ℝ), (0 : ℝ) < M → (0 : ℝ) < L → L = Real.log Ω → (0 : ℝ) < Ω → Real.exp ((2 : ℝ) * M / ((2 : ℝ) * M / L)) = Ω ∧ (√M < (2 : ℝ) * M / L ↔ (L / (2 : ℝ)) ^ (2 : ℕ) < M) ∧ ((2 : ℝ) * M / L < M ↔ (2 : ℝ) < L) :=74  @FRC.Strong.operational_cut75/-- p21030 — 21:C15. The radiative sector: the quarter-turn conjugate momentum makes the dynamics a wave equation: two helicity-$\pm2$ gravitons at speed $c$, quadrupole radiation; gauge leaves two polarisations. -/76theorem p21030 : ∀ (k : ℝ), (2 : ℝ) - (2 : ℝ) * Real.cos k = (4 : ℝ) * Real.sin (k / (2 : ℝ)) ^ (2 : ℕ) :=77  @FRC.Strong.dispersion_symbol78/-- p21033 — 21:C18. The primordial spectrum: $n_s=1$ the scale-dilation fixed point; the tilt's committed form $-\pi^{2}/\ln\Omega$, $\ln\Omega$ the e-fold count of the frame's scale range, the realisation of master L8, with the measured tilt its falsifier ($\tfrac12\ln\Omega$ excluded at $8.2\sigma$; the linearity condition undefined on a shell); the wrapped chart fixing the low large-angle power. -/79theorem p21033 : (∀ (n : ℝ), (∀ (k : ℝ), (0 : ℝ) < k → k ^ (3 : ℕ) * k ^ n = (1 : ℝ)) ↔ n = (-3 : ℝ)) ∧ 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 :=80  And.intro @FRC.Strong.scale_invariance_iff (@FRC.Chart.tilt_ledger)81/-- p21042 — 21:X2. \textbf{No dark-matter particle.} The radial acceleration relation is a registration crossover of the resolution floor, not evidence for undetected mass: galactic dynamics require no dark sector beyond the floor already fixed by $\Omega$. -/82theorem p21042 : Filter.Tendsto (fun t => t / ((1 : ℝ) - Real.exp (-t))) (nhdsWithin (0 : ℝ) (Set.Ioi (0 : ℝ))) (nhds (1 : ℝ)) :=83  @FRC.Strong.crossover_deep_limit84/-- p21048 — 21:X8. \textbf{The weakness of gravity} is cardinality dilution, not a hierarchy to be tuned. -/85theorem p21048 : ∀ (m Ω : ℝ), (0 : ℝ) < Ω → (m / √Ω) ^ (2 : ℕ) = m ^ (2 : ℕ) / Ω :=86  @FRC.Strong.dilution87/-- p21049 — 21:P1. Strong-field signatures at or outside the photon sphere: shadow $+4.6\%$, eikonal ringdown $-4.4\%$ (the $(2,2,0)$ reading open, GW250114 the exposure; master E13, E14), ISCO frequency $-6.9\%$ with accretion efficiency $5.48\%$ (against $5.72\%$): one origin, jointly falsifiable, conditional on Theorem~\ref{thm:branch}'s inputs alone. -/88theorem p21049 : (∀ (Gm r : ℝ), (0 : ℝ) < Gm → (0 : ℝ) < r → (2 : ℝ) * Real.exp (1 : ℝ) * Gm ≤ r * Real.exp ((2 : ℝ) * Gm / r) ∧ (r * Real.exp ((2 : ℝ) * Gm / r) = (2 : ℝ) * Real.exp (1 : ℝ) * Gm ↔ r = (2 : ℝ) * Gm)) ∧ (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) ∧ (∀ (r : ℝ), (2 : ℝ) < r → HasDerivAt (fun r => (2 : ℝ) / r + (2 : ℝ) * Real.log r - Real.log (r - (2 : ℝ))) ((r ^ (2 : ℕ) - (6 : ℝ) * r + (4 : ℝ)) / (r ^ (2 : ℕ) * (r - (2 : ℝ)))) r ∧ ((3 : ℝ) + √(5 : ℝ)) ^ (2 : ℕ) - (6 : ℝ) * ((3 : ℝ) + √(5 : ℝ)) + (4 : ℝ) = (0 : ℝ) ∧ (2 : ℝ) < (3 : ℝ) + √(5 : ℝ) ∧ ((3 : ℝ) + √(5 : ℝ) - (1 : ℝ)) / ((3 : ℝ) + √(5 : ℝ) - (2 : ℝ)) = ((3 : ℝ) + √(5 : ℝ)) / (4 : ℝ)) ∧ 547e-4 < (1 : ℝ) - √(Real.exp (-((2 : ℝ) / ((3 : ℝ) + √(5 : ℝ)))) * ((3 : ℝ) + √(5 : ℝ)) / (4 : ℝ)) ∧ (1 : ℝ) - √(Real.exp (-((2 : ℝ) / ((3 : ℝ) + √(5 : ℝ)))) * ((3 : ℝ) + √(5 : ℝ)) / (4 : ℝ)) < 548e-4 ∧ 571e-4 < (1 : ℝ) - √(8 / 9 : ℝ) ∧ (1 : ℝ) - √(8 / 9 : ℝ) < 572e-4 :=89  And.intro @FRC.Strong.photon_sphere (And.intro @FRC.Strong.shadow_bracket (And.intro @FRC.Strong.isco (@FRC.Strong.isco_efficiency)))90/-- p21050 — 21:P7. Floor-surface signatures: no prompt echoes (the exact profile horizonless with no reflecting surface, C12; the round-trip delay to $r_f$ carrying $e^{2u(r_f)}=\Omega$) and no evaporation bursts; a reported echo detection at the stated precision falsifies the construction. -/91theorem p21050 : ∀ (M L Ω : ℝ), (0 : ℝ) < M → (0 : ℝ) < L → L = Real.log Ω → (0 : ℝ) < Ω → Real.exp ((2 : ℝ) * M / ((2 : ℝ) * M / L)) = Ω ∧ (√M < (2 : ℝ) * M / L ↔ (L / (2 : ℝ)) ^ (2 : ℕ) < M) ∧ ((2 : ℝ) * M / L < M ↔ (2 : ℝ) < L) :=92  @FRC.Strong.operational_cut93/-- p21051 — 21:P2. Preferred-frame effects at $O(1/\sqrt\Omega)=O(10^{-62})$ ($3\times10^{-62}$ at $\Omega=1.3\times10^{123}$): the drive's in-principle signature, far below current $10^{-5}$ bounds. -/94theorem p21051 : 27e-63 < (1 : ℝ) / √13e122 ∧ (1 : ℝ) / √13e122 < 28e-63 :=95  @FRC.Strong.preferred_frame_scale96/-- p21052 — 21:P3. The weak-acceleration floor $a_0=cH_0/2\pi=1.04\times10^{-10}\,\mathrm{m\,s^{-2}}$ at the entailed $H_0=67.4$ \cite{entropy}, against the fitted $1.20\pm0.24\times10^{-10}$: $13\%$ low, $0.7\sigma$ of the systematic-dominated error, no free parameter; the $2\pi$ the dictionary's full cycle (14:B2), the one-cycle-per-period threshold the realisation 32:B3 with its discrete falsifier. -/97theorem p21052 : ∀ (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 :=98  @FRC.Chart.floor_value99/-- p21053 — 21:P4. The radial acceleration relation, $g_{\mathrm{obs}}=g_N/(1-e^{-\sqrt{g_N/a_0}})$, no fitted function beyond the barrier identification (B9), the form the data selected across the four observed acceleration decades, its approach to Newton the discriminant ($0.05$ at $g_N\approx5a_0$ against the simple rational interpolant); the deep limit gives the baryonic Tully--Fisher relation $v^4=GMa_0$. -/100theorem p21053 : (∀ (t : ℝ), (0 : ℝ) < t → (0 : ℝ) < (1 : ℝ) - Real.exp (-t) ∧ (1 : ℝ) ≤ t / ((1 : ℝ) - Real.exp (-t)) ∧ (t ≤ (1 : ℝ) → t / ((1 : ℝ) - Real.exp (-t)) ≤ (1 : ℝ) / ((1 : ℝ) - (3 : ℝ) * t / (4 : ℝ))) ∧ ∀ (G M r a₀ v : ℝ), (0 : ℝ) < r → (0 : ℝ) ≤ G * M → (0 : ℝ) ≤ a₀ → v ^ (2 : ℕ) = √(G * M / r ^ (2 : ℕ) * a₀) * r → v ^ (4 : ℕ) = G * M * a₀) ∧ Filter.Tendsto (fun t => (1 : ℝ) - Real.exp (-t)) Filter.atTop (nhds (1 : ℝ)) ∧ (∀ (w : ℝ), (0 : ℝ) < w → w < (1 : ℝ) → w * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) ^ (2 : ℕ) - (2 : ℝ) * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) + w = (0 : ℝ) ∧ (0 : ℝ) < ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w < (1 : ℝ) ∧ (1 : ℝ) < ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ∀ (x : ℝ), w * x ^ (2 : ℕ) - (2 : ℝ) * x + w = (0 : ℝ) → x = ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∨ x = ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w) ∧ 1.11966 < (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) ∧ (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) < 1.11967 ∧ 1.17082 < (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) ∧ (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) < 1.17083 ∧ 511e-4 < (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) - (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) ∧ (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) - (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) < 512e-4 :=101  And.intro @FRC.Strong.crossover_limits (And.intro @FRC.Strong.crossover_newton_limit (And.intro @FRC.Strong.registration_root (@FRC.Strong.interpolant_discriminant)))102/-- p21054 — 21:P5. The floor tracks the expansion, $a_0(z)\propto H(z)$ (BTFR zero-point $\propto E(z)^{1/4}$); high-$z$ rotation curves decisive. -/103theorem p21054 : ∀ (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 : ℝ) :=104  @FRC.Chart.running_floor105/-- p21055 — 21:P6. The 2PN periastron excess $\delta\dot\omega/\dot\omega\approx1.5\times10^{-6}$ for PSR~J0737$-$3039, today degenerate with the mass refit; decisive either way once an independent observable fixes $M_{\mathrm{tot}}$ at $10^{-6}$. Independent of the coherent-fraction falsifier of \citep{quantum}; the ledger carries both. -/106theorem p21055 : ∀ (U : ℝ), |U| ≤ (1 / 2 : ℝ) → |Real.exp (-((2 : ℝ) * U)) - (((1 : ℝ) - U / (2 : ℝ)) / ((1 : ℝ) + U / (2 : ℝ))) ^ (2 : ℕ) - U ^ (3 : ℕ) / (6 : ℝ)| ≤ (3 : ℝ) * U ^ (4 : ℕ) ∧ |Real.exp ((2 : ℝ) * U) - ((1 : ℝ) + U / (2 : ℝ)) ^ (4 : ℕ) - U ^ (2 : ℕ) / (2 : ℝ)| ≤ (3 : ℝ) * |U| ^ (3 : ℕ) :=107  @FRC.Strong.pn_series108/-- p21060 — 21:P8. The primordial tilt $n_s-1=-\pi^{2}/\ln\Omega=-0.0348$ [approx] at $\ln\Omega=283.5$ (the master's scale import), against Planck 2018 $-0.0351\pm0.0042$ ($+0.07\sigma$); $0.24\%$ per factor two in $S$; the neighbouring count $\tfrac12\ln\Omega$ excluded at $8.2\sigma$. -/109theorem p21060 : 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 :=110  @FRC.Chart.tilt_ledger111/-- p21062 — 21:C13. Area-law entropy $S=c_S'A_f/\ell_P^2$: the $\tfrac14$ the $Q_4$ gauge quotient counted on the shell ($S/A=\kap/\p $ exactly), the Carrier identity $S=(\Omega-1)/4$ at the coherence-horizon shell the same quarter (a consistency, not a closure); the count read as the coordinate area at the operational cut (B7); the identification of the entropy with the channel count (master D15); an exact merger area law $\Delta A=2M_1M_2$ on the count face of the mass; a phase-slip (Hawking-scaling) emission suppressed below one quantum per Hubble time. -/112theorem p21062 : (∀ (κ : ℕ), (4 : ℕ) * (κ * ((4 : ℕ) * κ + (2 : ℕ))) + (1 : ℕ) = ((4 : ℕ) * κ + (1 : ℕ)) ^ (2 : ℕ) ∧ κ * ((4 : ℕ) * κ + (2 : ℕ)) * ((4 : ℕ) * κ + (1 : ℕ)) = κ * (((4 : ℕ) * κ + (1 : ℕ)) * ((4 : ℕ) * κ + (2 : ℕ))) ∧ (4 : ℕ) * (κ * ((4 : ℕ) * κ + (2 : ℕ))) * ((4 : ℕ) * κ + (1 : ℕ)) = ((4 : ℕ) * κ + (1 : ℕ)) * ((4 : ℕ) * κ + (2 : ℕ)) * ((4 : ℕ) * κ)) ∧ (∀ (M₁ M₂ δ : ℤ), (M₁ + M₂) * (M₁ + M₂ + (1 : ℤ)) - M₁ * (M₁ + (1 : ℤ)) - M₂ * (M₂ + (1 : ℤ)) = (2 : ℤ) * M₁ * M₂ ∧ (M₁ + M₂ - δ) * (M₁ + M₂ - δ + (1 : ℤ)) - M₁ * (M₁ + (1 : ℤ)) - M₂ * (M₂ + (1 : ℤ)) = (2 : ℤ) * M₁ * M₂ - ((2 : ℤ) * (M₁ + M₂) + (1 : ℤ)) * δ + δ ^ (2 : ℕ) ∧ ((0 : ℤ) ≤ δ → δ ≤ (2 : ℤ) * (M₁ + M₂) + (1 : ℤ) → (M₁ + M₂ - δ) * (M₁ + M₂ - δ + (1 : ℤ)) - M₁ * (M₁ + (1 : ℤ)) - M₂ * (M₂ + (1 : ℤ)) ≤ (2 : ℤ) * M₁ * M₂) ∧ ((27811 : ℤ) + (1596 : ℤ)) * ((27811 : ℤ) + (1596 : ℤ) + (1 : ℤ)) - (27811 : ℤ) * ((27811 : ℤ) + (1 : ℤ)) - (1596 : ℤ) * ((1596 : ℤ) + (1 : ℤ)) = (88772712 : ℤ)) ∧ (∀ (rs L : ℝ), rs ≠ (0 : ℝ) → L ≠ (0 : ℝ) → (rs / L / rs) ^ (2 : ℕ) = (1 : ℝ) / L ^ (2 : ℕ)) ∧ 124e-7 < (1 : ℝ) / 283.5 ^ (2 : ℕ) ∧ (1 : ℝ) / 283.5 ^ (2 : ℕ) < 125e-7 :=113  And.intro @FRC.GravML.count_face (And.intro @FRC.GravML.merger_area_law (And.intro @FRC.Strong.capacity_ratio (@FRC.Strong.capacity_ratio_numeral)))114/-- p21064 — 21:C19. The registration crossover made exact: the killed walk is the noise sector, first passage the masking event, the window attribution the framed-rational tally ratio $g_N/f$, and the orbital response now derived (Theorem~\ref{thm:twoshift} with the registered-inertia identity); it rests on the masking barrier (B9) and the corpus's unified sampling clause (master D10), shared with \citep{quantum}. -/115theorem p21064 : (∀ (w : ℝ), (0 : ℝ) < w → w < (1 : ℝ) → w * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) ^ (2 : ℕ) - (2 : ℝ) * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) + w = (0 : ℝ) ∧ (0 : ℝ) < ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w < (1 : ℝ) ∧ (1 : ℝ) < ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ∀ (x : ℝ), w * x ^ (2 : ℕ) - (2 : ℝ) * x + w = (0 : ℝ) → x = ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∨ x = ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w) ∧ (∀ (t : ℝ), (0 : ℝ) < t → (0 : ℝ) < (1 : ℝ) - Real.exp (-t) ∧ (1 : ℝ) ≤ t / ((1 : ℝ) - Real.exp (-t)) ∧ (t ≤ (1 : ℝ) → t / ((1 : ℝ) - Real.exp (-t)) ≤ (1 : ℝ) / ((1 : ℝ) - (3 : ℝ) * t / (4 : ℝ))) ∧ ∀ (G M r a₀ v : ℝ), (0 : ℝ) < r → (0 : ℝ) ≤ G * M → (0 : ℝ) ≤ a₀ → v ^ (2 : ℕ) = √(G * M / r ^ (2 : ℕ) * a₀) * r → v ^ (4 : ℕ) = G * M * a₀) ∧ Filter.Tendsto (fun t => t / ((1 : ℝ) - Real.exp (-t))) (nhdsWithin (0 : ℝ) (Set.Ioi (0 : ℝ))) (nhds (1 : ℝ)) :=116  And.intro @FRC.Strong.registration_root (And.intro @FRC.Strong.crossover_limits (@FRC.Strong.crossover_deep_limit))117set_option linter.defProp false in118/-- p22005 — 22:A5. The window discipline, committed: the coherence horizon $\sqrt\Omega$, the decidability horizon $\Omega^{1/4}$, and the committed cardinality $\Omega\sim1.3\times10^{123}$ [chart] (the corpus's scale import, master A7) --- declared inputs of the programme, their cost recorded in the $\Omega$ ledger. -/119def p22005 := @FRC.Chart.omega_floors120/-- p22033 — 22:C17. Exact Tsirelson saturation: the singlet law $E(\Delta)=\cos(\pi\Delta/40)$ [chart], $S=2(\zeta_8+\zeta_8^{-1})$, $S^2=8$, the exhaustive $80^3$ sweep never exceeding it [chart]; no-signalling and the composite reduction commute. -/121theorem p22033 : (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹ = ↑√(2 : ℝ) ∧ (2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹) = ↑((2 : ℝ) * √(2 : ℝ)) ∧ ((2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹)) ^ (2 : ℕ) = (8 : ℂ)) ∧ ∀ (Δ : ℕ), (Complex.exp (↑((2 : ℝ) * Real.pi * ↑Δ / (80 : ℝ)) * Complex.I)).re = Real.cos (Real.pi * ↑Δ / (40 : ℝ)) :=122  And.intro @FRC.Chart.tsirelson_real (@FRC.Chart.singlet_law)123/-- p22035 — 22:C19. The gravitational channel entangles exactly, $C^2=\sin^2(\varphi/2)$ [chart], with the pure-channel complementarity $V^2+C^2=1$. -/124theorem p22035 : (∀ (φ : ℝ), (Complex.exp (↑(φ / (2 : ℝ)) * Complex.I) + Complex.exp (-(↑(φ / (2 : ℝ)) * Complex.I))) / (2 : ℂ) = ↑(Real.cos (φ / (2 : ℝ))) ∧ (Complex.exp (↑(φ / (2 : ℝ)) * Complex.I) - Complex.exp (-(↑(φ / (2 : ℝ)) * Complex.I))) / ((2 : ℂ) * Complex.I) = ↑(Real.sin (φ / (2 : ℝ))) ∧ Real.cos (φ / (2 : ℝ)) ^ (2 : ℕ) + Real.sin (φ / (2 : ℝ)) ^ (2 : ℕ) = (1 : ℝ) ∧ Real.sin (0 / 2 : ℝ) = (0 : ℝ)) ∧ ∀ (φ : ℝ), (0 : ℝ) < φ → φ < (2 : ℝ) * Real.pi → Real.sin (φ / (2 : ℝ)) ≠ (0 : ℝ) :=125  And.intro @FRC.Chart.channel_chart (@FRC.Chart.channel_entangles)126/-- p22041 — 22:C25. The measurement problem dissolved: Kochen--Specker poses no separate threat because values exist only as Subject-relative quotient phases, carried together with the Tsirelson strength $2\sqrt2$ [chart]. -/127theorem p22041 : FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹ = ↑√(2 : ℝ) ∧ (2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹) = ↑((2 : ℝ) * √(2 : ℝ)) ∧ ((2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹)) ^ (2 : ℕ) = (8 : ℂ) :=128  @FRC.Chart.tsirelson_real129/-- p22050 — 22:X7. \textbf{The Tsirelson boundary} is attained as a ring identity, $S=2(\zeta_8+\zeta_8^{-1})=2\sqrt2$ [chart], so a relational finite substrate carries full quantum correlation strength, not merely quantum vocabulary. -/130theorem p22050 : FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹ = ↑√(2 : ℝ) ∧ (2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹) = ↑((2 : ℝ) * √(2 : ℝ)) ∧ ((2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹)) ^ (2 : ℕ) = (8 : ℂ) :=131  @FRC.Chart.tsirelson_real132/-- p22052 — 22:P1. Gravitationally induced entanglement at exactly the Newtonian rate [chart], $V^2+C^2=1$ on the pure channel: equal force but unequal entanglement --- a source gravitates by its full mass while the systematic conditional phase, the calibrated discriminator, is carried by the coherent sectors alone, the fully incoherent channel separable at generic (nondegenerate) geometry. The one dated forward prediction. -/133theorem p22052 : ∀ (φ : ℝ), (Complex.exp (↑(φ / (2 : ℝ)) * Complex.I) + Complex.exp (-(↑(φ / (2 : ℝ)) * Complex.I))) / (2 : ℂ) = ↑(Real.cos (φ / (2 : ℝ))) ∧ (Complex.exp (↑(φ / (2 : ℝ)) * Complex.I) - Complex.exp (-(↑(φ / (2 : ℝ)) * Complex.I))) / ((2 : ℂ) * Complex.I) = ↑(Real.sin (φ / (2 : ℝ))) ∧ Real.cos (φ / (2 : ℝ)) ^ (2 : ℕ) + Real.sin (φ / (2 : ℝ)) ^ (2 : ℕ) = (1 : ℝ) ∧ Real.sin (0 / 2 : ℝ) = (0 : ℝ) :=134  @FRC.Chart.channel_chart135/-- p22054 — 22:P3. The Tsirelson value $S=2\sqrt2$ exact [chart] and the network behaviour of complex (not real) quantum theory: vacuum dispersion, $S\neq2\sqrt2$, or non-quantum network behaviour each falsify. -/136theorem p22054 : FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹ = ↑√(2 : ℝ) ∧ (2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹) = ↑((2 : ℝ) * √(2 : ℝ)) ∧ ((2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹)) ^ (2 : ℕ) = (8 : ℂ) :=137  @FRC.Chart.tsirelson_real138/-- p22056 — 22:P5. Quantum computation succeeds as standard quantum mechanics prescribes at every accessible depth; the first deviation, if any, is quantised at the unit-core ceiling $k^*=408$ ($204$ for $\sqrt\Omega$) [chart], not gradual. -/139theorem p22056 : (∀ (Λ ℓP r S Ω : ℝ), Λ = 1088e-55 → ℓP = 1616255e-41 → r ^ (2 : ℕ) = (3 : ℝ) / Λ → S = Real.pi * (r / ℓP) ^ (2 : ℕ) → Ω = (4 : ℝ) * S + (1 : ℝ) → (2 : ℝ) ^ (408 : ℕ) < Ω ∧ Ω / (4 : ℝ) < (2 : ℝ) ^ (408 : ℕ) ∧ (2 : ℝ) ^ (204 : ℕ) < √Ω ∧ √Ω / (4 : ℝ) < (2 : ℝ) ^ (204 : ℕ)) ∧ ∀ (m : ℕ), ¬(2 : GaussianInt) ∣ FRC.QuantumML.gi ^ m * FRC.QuantumML.onePlusI :=140  And.intro @FRC.Chart.ceiling_bracket (@FRC.QuantumML.gaussian_minimal)141set_option linter.defProp false in142/-- p22061 — 22:Z2. The committed $\Omega$ anchor and the binding floor: the carrier scale is fixed by the verified Riemann height through $\Omega^{1/4}$ [chart], and a single off-line zero below $\Omega^{1/4}$ falsifies from a desk. -/143def p22061 := @FRC.Chart.omega_floors144set_option linter.defProp false in145/-- p26010 — 26:B4. The continuum reading [chart]: the dilation generator $\HH=-\mathrm i(x\partial_x+\tfrac12)$ has $x^{-1/2+\mathrm i\nu}$ as eigenfunction of eigenvalue $\nu$ on $x>0$, so the frequency index is the spectrum of $\HH$ in the chart of the scale shift (20:E1). -/146def p26010 := @FRC.Chart.dilation_eigen147/-- p26011 — 26:B5. The Gauss sum couples the two turns: multiplication by a unit permutes the units; $\sum_{t\neq0}\psi(tc)$ is $-1$ for $c\neq0$ and $P-1$ for $c=0$; $\sum_u\chi(u)=0$ for $\chi\neq1$; hence $\lvert g(\chi)\rvert^{2}=P$ for every nontrivial $\chi$ on the shell ($\Om$ on the Carrier). -/148theorem p26011 : (∀ {F : Type u_1} [Field F] [Fintype F] {R' : Type u_2} [CommRing R'] [IsDomain R'] {χ : MulChar F R'}, χ ≠ (1 : MulChar F R') → ∀ {ψ : AddChar F R'}, ψ.IsPrimitive → gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card F)) ∧ ∀ {F : Type u_3} [Field F] [Fintype F] {χ : MulChar F ℂ}, χ ≠ (1 : MulChar F ℂ) → ∀ {ψ : AddChar F ℂ}, ψ.IsPrimitive → gaussSum χ ψ * star (gaussSum χ ψ) = ↑(Fintype.card F) ∧ Complex.normSq (gaussSum χ ψ) = ↑(Fintype.card F) :=149  And.intro @FRC.HorizonML.gauss_product (@FRC.Chart.gauss_modulus)150/-- p26013 — 26:C2. The family's size and the table beyond the horizon [chart]: at the anchor $2^{204}<\sqrt\Om<2^{205}$, so the shells of the family $P^{2}<\Om$ have at most $205$ bits; $2^{102}<\Om^{1/4}<2^{103}$, so a decision table with one entry per $204$-bit input exceeds the absolute horizon and lies below $\sqrt\Om$. -/151theorem p26013 : ∀ (Λ ℓP r S Ω : ℝ), Λ = 1088e-55 → ℓP = 1616255e-41 → r ^ (2 : ℕ) = (3 : ℝ) / Λ → S = Real.pi * (r / ℓP) ^ (2 : ℕ) → Ω = (4 : ℝ) * S + (1 : ℝ) → (2 : ℝ) ^ (204 : ℕ) < √Ω ∧ √Ω < (2 : ℝ) ^ (205 : ℕ) ∧ (2 : ℝ) ^ (102 : ℕ) < √√Ω ∧ √√Ω < (2 : ℝ) ^ (103 : ℕ) :=152  @FRC.Chart.family_bits153/-- p38010 — 38:B2. The radial ladder: shells at $R\sin(2a\pi/13)$ [chart]; capacity $4a<\p\Leftrightarrow a\le\kap$. -/154theorem 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 :=155  @FRC.Chart.ladder_monotone156/-- p38048 — 38:X3. \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)$. -/157theorem 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 :=158  @FRC.Chart.floor_value159/-- p38049 — 38:P1. 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). -/160theorem 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 : ℝ) :=161  And.intro @FRC.Chart.floor_value (@FRC.Chart.running_floor)162-- end keys163164end FRC.LedgerML165