import Mathlib /-! Generated by `lean/make_web.py` from `FrcLedger/Gravity.lean` with `FrcLedger/Theme/Chart`, `FrcLedger/Theme/Strong`, `FrcLedger/Theme/Gravity`, `FrcLedger/Theme/Horizon`, `FrcLedger/Keys/Chart`, `FrcLedger/Keys/Gravity` inlined — one self-contained file for the Lean web editor. Edit the modules, not this file. -/ /-! inlined: FrcLedger/Theme/Chart.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Chart — the chart theme: the readings against the continuum (ledger migration, task LM30) The chart theme holds the readings of the finite results against the continuum, the only theme with the reals (`frc/themes.py`, rank 30). It serves the chart clauses of the master's scale import (00:A7, `scale_import`; the ledger's `ln Ω` for L8, `ln_omega_ledger`), its cosmology and prediction rows: the floor `a₀ = cH₀/2π` (00:L1), the octant record depth and its outputs (00:L3), the primordial tilt (00:L8) and the running floor (00:P1). The chart's numerals — the speed of light, the megaparsec, the Julian year, the fitted values and their errors — are declared data. The octant's theorems moved here from 14-entropy and the floor's from 21-gravity (6 October 2026); those modules keep the old names as aliases. Classical (tier 2) on Mathlib's hierarchy. Every bracket is certified from `π` to six places (`Real.pi_gt_d6`, `Real.pi_lt_d6`), `e` to nine (`Real.exp_one_gt_d9`, `Real.exp_one_lt_d9`) and the Taylor tail of `exp` (`Real.exp_bound`, `Real.exp_bound'`). The realisation content behind each reading — that the octant is the record depth, that the floor is the synchronisation threshold, that `ln Ω` is the tilt's e-fold count — is the rows' realisation clause, not formal content. -/ namespace FRC.Chart open Real /-! ## The scale import's chart numerals (00:A7; 14:A1, C1) -/ section scale /-- 00:A7 [chart] — the scale import's numerals: with the fit's `Λ = 1.088 × 10⁻⁵² m⁻²` (Planck 2018) and the Planck length `ℓ_P = 1.616255 × 10⁻³⁵ m` declared [data], the de Sitter radius `r_H = c/H_Λ`, `r_H² = 3/Λ`, gives `S = π (r_H/ℓ_P)²` between `3.31` and `3.32 × 10¹²²` (the row's `3.3 × 10¹²²`) and `Ω = 4S + 1` between `1.32` and `1.33 × 10¹²³` (the row's `1.3 × 10¹²³`). That the datum fixes the cardinality is the import; nothing here derives the datum. -/ theorem scale_import (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35) (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) : (3.31e122 : ℝ) < S ∧ S < 3.32e122 ∧ (1.32e123 : ℝ) < Ω ∧ Ω < 1.33e123 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hK : S = π * (3 / (Λ * ℓP ^ 2)) := by rw [hS, div_pow, hr2]; subst hΛ hℓ; field_simp subst hΛ hℓ have hKpos : (0 : ℝ) < 3 / (1.088e-52 * (1.616255e-35) ^ 2) := by positivity have hSlo : (3.3160599e122 : ℝ) < S := by rw [hK]; have := mul_lt_mul_of_pos_right hpi1 hKpos; norm_num at this ⊢; linarith have hShi : S < (3.3160611e122 : ℝ) := by rw [hK]; have := mul_lt_mul_of_pos_right hpi2 hKpos; norm_num at this ⊢; linarith subst hΩ refine ⟨by linarith, by linarith, by linarith, by linarith⟩ set_option exponentiation.threshold 512 in /-- 00:L8 [chart] — the ledger's `ln Ω = 283.5`, the numeral the tilt reads, derived from the scale import: with the same `Λ`, `ℓ_P`, `r_H² = 3/Λ`, `S = π (r_H/ℓ_P)²` and `Ω = 4S + 1`, `ln Ω` lies between `283.50` and `283.51`. The logarithm is bracketed by `409 ln 2` (`Real.log_two_gt_d9`, `log_two_lt_d9`) and `1 − 1/m ≤ ln m ≤ m − 1` on the mantissa `m = Ω/2⁴⁰⁹`. -/ theorem ln_omega_ledger (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35) (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) : (283.50 : ℝ) < Real.log Ω ∧ Real.log Ω < 283.51 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hK : S = π * (3 / (Λ * ℓP ^ 2)) := by rw [hS, div_pow, hr2]; subst hΛ hℓ; field_simp subst hΛ hℓ have hKpos : (0 : ℝ) < 3 / (1.088e-52 * (1.616255e-35) ^ 2) := by positivity have hSlo : (3.3160599e122 : ℝ) < S := by rw [hK]; have := mul_lt_mul_of_pos_right hpi1 hKpos; norm_num at this ⊢; linarith have hShi : S < (3.3160611e122 : ℝ) := by rw [hK]; have := mul_lt_mul_of_pos_right hpi2 hKpos; norm_num at this ⊢; linarith subst hΩ have hΩpos : (0 : ℝ) < 4 * S + 1 := by linarith have hmpos : (0 : ℝ) < (4 * S + 1) / 2 ^ 409 := by positivity have hlog : Real.log (4 * S + 1) = 409 * Real.log 2 + Real.log ((4 * S + 1) / 2 ^ 409) := by have e : (4 * S + 1 : ℝ) = 2 ^ 409 * ((4 * S + 1) / 2 ^ 409) := by field_simp conv_lhs => rw [e] rw [Real.log_mul (by positivity) (by positivity), Real.log_pow]; push_cast; ring have hl1 := Real.log_two_gt_d9 have hl2 := Real.log_two_lt_d9 have hm1 : (1.0032614 : ℝ) < (4 * S + 1) / 2 ^ 409 := by rw [lt_div_iff₀ (by positivity)]; norm_num; linarith have hm2 : (4 * S + 1) / 2 ^ 409 < (1.0032619 : ℝ) := by rw [div_lt_iff₀ (by positivity)]; norm_num; linarith have hup := Real.log_le_sub_one_of_pos hmpos have hlo := Real.one_sub_inv_le_log_of_pos hmpos have hinv : 1 / ((4 * S + 1) / 2 ^ 409) < 1 / (1.0032614 : ℝ) := one_div_lt_one_div_of_lt (by norm_num) hm1 rw [inv_eq_one_div] at hlo have hA : (0.00325 : ℝ) < Real.log ((4 * S + 1) / 2 ^ 409) := by have : (1 : ℝ) - 1 / 1.0032614 > 0.00325 := by norm_num linarith have hB : Real.log ((4 * S + 1) / 2 ^ 409) < (0.003262 : ℝ) := by linarith rw [hlog] exact ⟨by linarith, by linarith⟩ end scale /-! ## The octant record depth and its outputs (00:L3; 14:C5, C7, P3) -/ section octant /-- 00:L3, 14:C5 [chart] — the chart conversion of the octant: the count `S/2` out of the `4S`-cycle, read on the meridian circle `2π r_H/c`, is the depth `(π/4) r_H/c`. -/ theorem octant_chart (S r c : ℝ) (hS : S ≠ 0) : (S / 2) / (4 * S) * (2 * π * r / c) = (π / 4) * r / c := by rcases eq_or_ne c 0 with rfl | hc · simp · field_simp /-- The octant's rate factor `tanh(3π/8)` is positive. -/ theorem tanh_octant_pos : 0 < tanh (3 * π / 8) := by rw [Real.tanh_eq_sinh_div_cosh] exact div_pos (Real.sinh_pos_iff.2 (by positivity)) (Real.cosh_pos _) /-- 00:L3, 14:P3 [ΛCDM] — the algebraic locus: with `t H_Λ = π/4` (the octant), `H_Λ = H₀ √Ω_Λ` and `Ω_Λ = tanh²(3π/8)`, `t H₀ = (π/4)/tanh(3π/8)`; the numeral `0.950` is bracketed in `locus_bracket`. -/ theorem age_rate_locus (t H0 HΛ Ω : ℝ) (hoct : t * HΛ = π / 4) (hΛ : HΛ = H0 * √Ω) (hΩ : Ω = tanh (3 * π / 8) ^ 2) : t * H0 = (π / 4) / tanh (3 * π / 8) := by have hpos := tanh_octant_pos rw [hΩ, Real.sqrt_sq hpos.le] at hΛ rw [eq_div_iff hpos.ne', ← hoct, hΛ]; ring /-- 00:L3, 14:A8 [ΛCDM] — the rival chart's age identity as the import it is: in flat matter-plus-`Λ` the product of the age and the asymptotic rate is `t₀H_Λ = (2/3) artanh √Ω_Λ`, a function of the one fitted parameter; outside `[0, 1)` the value is junk. Moved here from 14-entropy (task LM30's repair, 7 October 2026), which keeps the name. -/ noncomputable def lcdmAge (Ω : ℝ) : ℝ := 2 / 3 * artanh (√Ω) /-- 00:L3, 14:C7, 14:X3 [ΛCDM] — the octant inversion: the rival chart's identity gives `t₀H_Λ = π/4` at `Ω_Λ = tanh²(3π/8)` and, for `0 ≤ Ω_Λ < 1`, only there. Moved here from 14-entropy, which keeps the name. -/ theorem octant_inversion : lcdmAge (tanh (3 * π / 8) ^ 2) = π / 4 ∧ ∀ Ω : ℝ, 0 ≤ Ω → Ω < 1 → lcdmAge Ω = π / 4 → Ω = tanh (3 * π / 8) ^ 2 := by have hpos := tanh_octant_pos constructor · unfold lcdmAge rw [Real.sqrt_sq hpos.le, Real.artanh_tanh]; ring · intro Ω h0 h1 h unfold lcdmAge at h have hart : artanh (√Ω) = 3 * π / 8 := by linarith have hΩ : √Ω ∈ Set.Ioo (-1 : ℝ) 1 := by refine ⟨by linarith [Real.sqrt_nonneg Ω], ?_⟩ rw [Real.sqrt_lt' one_pos]; simpa using h1 have := Real.tanh_artanh hΩ rw [hart] at this rw [this, Real.sq_sqrt h0] /-- `tanh x = (e^{2x} − 1)/(e^{2x} + 1)`. -/ theorem tanh_eq_exp_two_mul (x : ℝ) : tanh x = (exp (2 * x) - 1) / (exp (2 * x) + 1) := by rw [Real.tanh_eq, Real.exp_neg, two_mul, Real.exp_add] have h := Real.exp_pos x field_simp /-- The Taylor brackets of `e^t` at the two ends of `t = 3π/4 − 2`: seven terms of the series with the tail bound of Mathlib's `Real.exp_bound`. -/ theorem exp_tail_bounds : (1.427884 : ℝ) < exp 0.356194 ∧ exp (0.35619475 : ℝ) < 1.4278857 := by constructor · have h := abs_le.1 (Real.exp_bound (x := 0.356194) (by rw [abs_of_pos (by norm_num)]; norm_num) (n := 7) (by norm_num)) rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.356194)] at h have h1 := h.1 norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢ linarith · have h := Real.exp_bound' (x := 0.35619475) (by norm_num) (by norm_num) (n := 7) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢ linarith /-- `e^{3π/4}` bracketed: `10.55071 < e^{3π/4} < 10.55073`, from `π` to six places, `e` to nine, and the Taylor tail. -/ theorem exp_three_pi_four_bounds : (10.55071 : ℝ) < exp (3 * π / 4) ∧ exp (3 * π / 4) < 10.55073 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have he1 := Real.exp_one_gt_d9 have he2 := Real.exp_one_lt_d9 have ht := exp_tail_bounds have hsplit : exp (3 * π / 4) = exp 1 * exp 1 * exp (3 * π / 4 - 2) := by rw [← Real.exp_add, ← Real.exp_add]; congr 1; ring have hlo : exp 0.356194 < exp (3 * π / 4 - 2) := Real.exp_lt_exp.2 (by linarith) have hhi : exp (3 * π / 4 - 2) < exp 0.35619475 := Real.exp_lt_exp.2 (by linarith) have hpos : (0 : ℝ) < exp 1 := Real.exp_pos 1 rw [hsplit] constructor · nlinarith [mul_pos hpos hpos, Real.exp_pos (3 * π / 4 - 2)] · nlinarith [mul_pos hpos hpos, Real.exp_pos (3 * π / 4 - 2)] /-- `tanh(3π/8)` bracketed: `0.82685 < tanh(3π/8) < 0.826851`, from `exp_three_pi_four_bounds`. -/ theorem tanh_octant_bounds : (0.82685 : ℝ) < tanh (3 * π / 8) ∧ tanh (3 * π / 8) < 0.826851 := by obtain ⟨hE1, hE2⟩ := exp_three_pi_four_bounds have htanh : tanh (3 * π / 8) = (exp (3 * π / 4) - 1) / (exp (3 * π / 4) + 1) := by rw [tanh_eq_exp_two_mul]; congr 2 <;> ring_nf have hden : (0 : ℝ) < exp (3 * π / 4) + 1 := by linarith constructor · rw [htanh, lt_div_iff₀ hden]; linarith · rw [htanh, div_lt_iff₀ hden]; linarith /-- 00:L3, 14:P3 — the locus's numeral bracketed: `0.9498 < (π/4)/tanh(3π/8) < 0.9499`, the paper's `0.950`. -/ theorem locus_bracket : (0.9498 : ℝ) < (π / 4) / tanh (3 * π / 8) ∧ (π / 4) / tanh (3 * π / 8) < 0.9499 := by obtain ⟨hl, hu⟩ := tanh_octant_bounds have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hpos : (0 : ℝ) < tanh (3 * π / 8) := by linarith constructor · rw [lt_div_iff₀ hpos]; nlinarith · rw [div_lt_iff₀ hpos]; nlinarith /-- The locus to six places: `0.949866 < (π/4)/tanh(3π/8) < 0.949868`, for the rates read on it. -/ theorem locus_fine : (0.949866 : ℝ) < (π / 4) / tanh (3 * π / 8) ∧ (π / 4) / tanh (3 * π / 8) < 0.949868 := by obtain ⟨hl, hu⟩ := tanh_octant_bounds have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hpos : (0 : ℝ) < tanh (3 * π / 8) := by linarith constructor · rw [lt_div_iff₀ hpos]; nlinarith · rw [div_lt_iff₀ hpos]; nlinarith /-- 00:L3, 14:C7, 14:X3 — the landing bracketed: `0.68368 < tanh²(3π/8) < 0.68369` (the numeral `0.684`) is certified from `π` to six places, `e` to nine and the Taylor tail; and, with the Planck numerals `0.685 ± 0.007` taken as data, the deviation lies between `0.18σ` and `0.19σ`. -/ theorem landing_bracket : (0.68368 : ℝ) < tanh (3 * π / 8) ^ 2 ∧ tanh (3 * π / 8) ^ 2 < 0.68369 ∧ 0.18 * 0.007 < 0.685 - tanh (3 * π / 8) ^ 2 ∧ 0.685 - tanh (3 * π / 8) ^ 2 < 0.19 * 0.007 := by obtain ⟨hl, hu⟩ := tanh_octant_bounds have hsq1 : (0.82685 : ℝ) ^ 2 < tanh (3 * π / 8) ^ 2 := by apply pow_lt_pow_left₀ hl (by norm_num) (by norm_num) have hsq2 : tanh (3 * π / 8) ^ 2 < (0.826851 : ℝ) ^ 2 := by apply pow_lt_pow_left₀ hu (by linarith) (by norm_num) norm_num at hsq1 hsq2 refine ⟨by linarith, by linarith, by linarith, by linarith⟩ /-- 00:L3 — the deviation fixed to the row's rounded `0.19σ`: between `0.186σ` and `0.19σ` below Planck's `0.685 ± 0.007` (data). -/ theorem landing_fine : 0.186 * 0.007 < 0.685 - tanh (3 * π / 8) ^ 2 ∧ 0.685 - tanh (3 * π / 8) ^ 2 < (0.19 * 0.007 : ℝ) := by obtain ⟨h1, h2, _, h4⟩ := landing_bracket exact ⟨by linarith, h4⟩ /-- 00:L3 [chart] — the channel-1 consistency: read on the depth `t = 13.79` Gyr (the row's depth numeral, a Julian year of `365.25` days; data), the locus `t H₀ = (π/4)/tanh(3π/8)` gives `67.35 < H₀ < 67.36` km s⁻¹ Mpc⁻¹ (the megaparsec `3.0856775814913673 × 10¹⁹` km; data): the channel-1 rate `67.4` to `0.1 %` (14:P3, "a consistency, not a prediction"). -/ theorem hubble_landing (t H0 : ℝ) (ht : t = 13.79e9 * (365.25 * 86400)) (hloc : t * H0 = (π / 4) / tanh (3 * π / 8)) : (67.35 : ℝ) < H0 * 3.0856775814913673e19 ∧ H0 * 3.0856775814913673e19 < 67.36 := by obtain ⟨hl, hu⟩ := locus_fine have htpos : (0 : ℝ) < t := by rw [ht]; norm_num have hH : H0 = (π / 4) / tanh (3 * π / 8) / t := by rw [eq_div_iff htpos.ne', mul_comm, hloc] constructor · rw [hH, ht, div_mul_eq_mul_div, lt_div_iff₀ (by norm_num)]; nlinarith · rw [hH, ht, div_mul_eq_mul_div, div_lt_iff₀ (by norm_num)]; nlinarith /-- 00:L3, 14:P3 [chart] — the locus read on the fit-independent stellar age `t★ = 13.61 ± 0.34` Gyr (data; a Julian year of `365.25` days): `68.24 < H₀ < 68.25` km s⁻¹ Mpc⁻¹ (the row's `68.2`); the age's error carried to the rate, `H₀ · 0.34/13.61`, lies between `1.70` and `1.71` (the row's `±1.7`); and the Cepheid ladder's `73.0 ± 1.0` (data), errors combined with `±1.7`, lies between `2.40σ` and `2.42σ` above it (the row's `2.4σ`). -/ theorem hubble_stellar (t H0 : ℝ) (ht : t = 13.61e9 * (365.25 * 86400)) (hloc : t * H0 = (π / 4) / tanh (3 * π / 8)) : (68.24 : ℝ) < H0 * 3.0856775814913673e19 ∧ H0 * 3.0856775814913673e19 < 68.25 ∧ (1.70 : ℝ) < H0 * 3.0856775814913673e19 * (0.34 / 13.61) ∧ H0 * 3.0856775814913673e19 * (0.34 / 13.61) < 1.71 ∧ (2.40 : ℝ) < (73.0 - H0 * 3.0856775814913673e19) / √(1.7 ^ 2 + 1.0 ^ 2) ∧ (73.0 - H0 * 3.0856775814913673e19) / √(1.7 ^ 2 + 1.0 ^ 2) < 2.42 := by obtain ⟨hl, hu⟩ := locus_fine have htpos : (0 : ℝ) < t := by rw [ht]; norm_num have hH : H0 = (π / 4) / tanh (3 * π / 8) / t := by rw [eq_div_iff htpos.ne', mul_comm, hloc] have h1 : (68.24 : ℝ) < H0 * 3.0856775814913673e19 := by rw [hH, ht, div_mul_eq_mul_div, lt_div_iff₀ (by norm_num)]; nlinarith have h2 : H0 * 3.0856775814913673e19 < (68.25 : ℝ) := by rw [hH, ht, div_mul_eq_mul_div, div_lt_iff₀ (by norm_num)]; nlinarith have hs1 : (1.9723 : ℝ) < √(1.7 ^ 2 + 1.0 ^ 2) := by rw [Real.lt_sqrt (by norm_num)]; norm_num have hs2 : √(1.7 ^ 2 + 1.0 ^ 2 : ℝ) < 1.9724 := by rw [Real.sqrt_lt' (by norm_num)]; norm_num have hspos : (0 : ℝ) < √(1.7 ^ 2 + 1.0 ^ 2) := by linarith refine ⟨h1, h2, by nlinarith, by nlinarith, ?_, ?_⟩ · rw [lt_div_iff₀ hspos]; nlinarith · rw [div_lt_iff₀ hspos]; nlinarith end octant /-! ## The floor and its running (00:L1, P1; 21:P3) -/ section floor /-- 00:L1, 21:P3 — the weak-acceleration floor `a₀ = cH₀/2π` at the entailed `H₀ = 67.4 km s⁻¹ Mpc⁻¹` (the speed of light and the megaparsec declared numerals [data]): `a₀` lies between `1.04` and `1.05 × 10⁻¹⁰ m s⁻²`; against the fitted `1.20 × 10⁻¹⁰` it is between `13.0 %` and `13.2 %` low, and the deficit is between `0.65` and `0.67` of the systematic `0.24 × 10⁻¹⁰` (the text's `13 %`, `0.7σ`). -/ theorem floor_value (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) : (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.05e-10 ∧ (0.868 : ℝ) < c * H0 / (2 * π) / 1.2e-10 ∧ c * H0 / (2 * π) / 1.2e-10 < 0.870 ∧ (0.65 : ℝ) < (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 ∧ (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 < 0.67 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 subst hc hH have hA : (1.042e-10 : ℝ) < 299792458 * (67.4e3 / 3.0856775814913673e22) / (2 * π) := by rw [lt_div_iff₀ (by positivity)]; nlinarith have hB : 299792458 * (67.4e3 / 3.0856775814913673e22) / (2 * π) < (1.0423e-10 : ℝ) := by rw [div_lt_iff₀ (by positivity)]; nlinarith refine ⟨by linarith, by linarith, ?_, ?_, ?_, ?_⟩ · rw [lt_div_iff₀ (by norm_num)]; linarith · rw [div_lt_iff₀ (by norm_num)]; linarith · rw [lt_div_iff₀ (by norm_num)]; linarith · rw [div_lt_iff₀ (by norm_num)]; linarith /-- 00:L1 — the floor fixed to the row's rounded `1.04 × 10⁻¹⁰`: at the channel-1 rate `H₀ = 67.4 km s⁻¹ Mpc⁻¹`, `1.04 × 10⁻¹⁰ < a₀ < 1.045 × 10⁻¹⁰ m s⁻²`. -/ theorem floor_fine (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) : (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.045e-10 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 subst hc hH constructor · rw [lt_div_iff₀ (by positivity)]; nlinarith · rw [div_lt_iff₀ (by positivity)]; nlinarith /-- 00:P1 [chart] — the running floor: if the floor is read at every redshift on the registered rate, `a₀(z) = cH(z)/2π`, and the deep-regime Tully–Fisher law `v⁴ = G M a₀` holds at fixed baryonic mass `M`, then `a₀(z)/a₀(0) = H(z)/H(0) = E(z)` and the zero-point evolves as `v(z)/v(0) = E(z)^{1/4}`; the rates and speeds are asked positive at `0` and `z` only. The law `v⁴ = G M a₀` is the deep regime's import. That the floor tracks the registered rate (the gravity realisation, 00:D5) is the row's realisation clause, not formal content. -/ theorem running_floor (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ) (hc : 0 < c) (hG : 0 < G) (hM : 0 < M) (h0 : 0 < H 0) (hz : 0 < H z) (ha : ∀ z, a z = c * H z / (2 * π)) (hv0 : 0 < v 0) (hvz : 0 < v z) (htf : ∀ 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 : ℝ) := by have hpi := Real.pi_pos have hratio : a z / a 0 = H z / H 0 := by rw [ha z, ha 0]; field_simp refine ⟨hratio, ?_⟩ have ha0 : 0 < a 0 := by rw [ha 0]; positivity have h4 : (v z / v 0) ^ 4 = H z / H 0 := by rw [div_pow, htf z, htf 0, ← hratio]; field_simp rw [← h4, show (1 / 4 : ℝ) = ((4 : ℕ) : ℝ)⁻¹ by norm_num] exact (Real.pow_rpow_inv_natCast (div_pos hvz hv0).le (by norm_num)).symm end floor /-! ## The radial ladder of the minimal pair (38:B2) -/ section ladder /-- 38:B2 [chart] — the radial ladder of the sky: the shell radii `R sin(2aπ/13)`, `a = 1, 2, 3`, are positive, strictly increasing, and inside the rim `R` (the chart flattening of the latitude circles; the capacity `4a < p ⇔ a ≤ κ` is the core's `FRC.Pair.window`). -/ theorem ladder_monotone (R : ℝ) (hR : 0 < R) : 0 < R * Real.sin (2 * π / 13) ∧ R * Real.sin (2 * π / 13) < R * Real.sin (4 * π / 13) ∧ R * Real.sin (4 * π / 13) < R * Real.sin (6 * π / 13) ∧ R * Real.sin (6 * π / 13) < R := by have hpi := Real.pi_pos have mono : ∀ x y : ℝ, 0 ≤ x → x < y → y ≤ π / 2 → Real.sin x < Real.sin y := fun x y hx hxy hy => Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith) hy hxy refine ⟨mul_pos hR (Real.sin_pos_of_pos_of_lt_pi (by positivity) (by linarith)), ?_, ?_, ?_⟩ · exact mul_lt_mul_of_pos_left (mono _ _ (by positivity) (by linarith) (by linarith)) hR · exact mul_lt_mul_of_pos_left (mono _ _ (by positivity) (by linarith) (by linarith)) hR · have h := mono (6 * π / 13) (π / 2) (by positivity) (by linarith) le_rfl rw [Real.sin_pi_div_two] at h calc R * Real.sin (6 * π / 13) < R * 1 := mul_lt_mul_of_pos_left h hR _ = R := mul_one R end ladder /-! ## The primordial tilt (00:L8) -/ section tilt /-- 00:L8 [chart] — the tilt at the ledger's `ln Ω = 283.5` (`ln_omega_ledger`, from the scale import 00:A7; data): `n_s − 1 = −π²/ln Ω` has magnitude between `0.03481` and `0.03482` (the row's `−0.0348`); against Planck 2018's `−0.0351 ± 0.0042` (data) the deviation is between `+0.068σ` and `+0.069σ` (the row's `+0.07σ`); the count `½ ln Ω` gives `−π²/(ln Ω/2)`, off by between `8.2σ` and `8.25σ` (the row's exclusion at `8.2σ`). That `ln Ω` is the e-fold count of the frame's scale range is the row's realisation clause, not formal content. -/ theorem tilt_ledger : (0.03481 : ℝ) < π ^ 2 / 283.5 ∧ π ^ 2 / 283.5 < 0.03482 ∧ (0.068 * 0.0042 : ℝ) < 0.0351 - π ^ 2 / 283.5 ∧ 0.0351 - π ^ 2 / 283.5 < 0.069 * 0.0042 ∧ (8.2 * 0.0042 : ℝ) < π ^ 2 / (283.5 / 2) - 0.0351 ∧ π ^ 2 / (283.5 / 2) - 0.0351 < 8.25 * 0.0042 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hsq1 : (3.141592 : ℝ) ^ 2 < π ^ 2 := pow_lt_pow_left₀ hpi1 (by norm_num) (by norm_num) have hsq2 : π ^ 2 < (3.141593 : ℝ) ^ 2 := pow_lt_pow_left₀ hpi2 (by linarith) (by norm_num) norm_num at hsq1 hsq2 refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ · rw [lt_div_iff₀ (by norm_num)]; linarith · rw [div_lt_iff₀ (by norm_num)]; linarith · have : π ^ 2 / 283.5 < (0.0351 - 0.068 * 0.0042 : ℝ) := by rw [div_lt_iff₀ (by norm_num)]; norm_num; linarith linarith · have : (0.0351 - 0.069 * 0.0042 : ℝ) < π ^ 2 / 283.5 := by rw [lt_div_iff₀ (by norm_num)]; norm_num; linarith linarith · have : (8.2 * 0.0042 + 0.0351 : ℝ) < π ^ 2 / (283.5 / 2) := by rw [lt_div_iff₀ (by norm_num)]; norm_num; linarith linarith · have : π ^ 2 / (283.5 / 2) < (8.25 * 0.0042 + 0.0351 : ℝ) := by rw [div_lt_iff₀ (by norm_num)]; norm_num; linarith linarith /-- 00:L8 — the e-fold count of the frame's scale range: from `1/√Ω` to `√Ω` the logarithm spans `ln Ω`. -/ theorem efold_count (Ω : ℝ) (hΩ : 0 < Ω) : Real.log (√Ω / (1 / √Ω)) = Real.log Ω := by have hs : 0 < √Ω := Real.sqrt_pos.2 hΩ have e : √Ω / (1 / √Ω) = Ω := by rw [div_div_eq_mul_div, div_one, Real.mul_self_sqrt hΩ.le] rw [e] end tilt /-! ## 20-rh: the complex characters of the cycle, the characters as eigenvectors of the scale-shift, and the von Mangoldt weight (20:E1, E12, E13, C5, C2; task LM36) Moved here from 20-rh's `FrcLedger/Rh.lean` under the same names; that module keeps the old names as aliases. The exact shell arithmetic of the same rows is the horizon theme's (`Theme/Horizon.lean`, `FRC.HorizonML`). -/ section characters open Complex Finset variable {n : ℕ} [NeZero n] /-- The `j`-th chart mode of the cycle `C_n`: `χ_j(m) = e^{2πi·jm/n}`. On the shell, `m` is the discrete logarithm of the residue `g^m` and `n = p − 1`. -/ noncomputable def chi (j m : ZMod n) : ℂ := ZMod.stdAddChar (j * m) /-- The coefficient of `v` on the mode `χ_j`: `⟨v, χ_j⟩ = Σ_m v(m) χ_j(m)̄`. -/ noncomputable def coef (v : ZMod n → ℂ) (j : ZMod n) : ℂ := ∑ m, v m * (starRingEnd ℂ) (chi j m) lemma chi_conj (j m : ZMod n) : (starRingEnd ℂ) (chi j m) = ZMod.stdAddChar (-(j * m)) := by rw [chi, AddChar.map_neg_eq_conj] /-- 20:E13 — orthogonality of the chart modes: `Σ_m χ_j(m) χ_k(m)̄ = n·[j = k]`, each of squared norm `n = p − 1` (with `chi_inversion`, the `p − 1` characters are an orthogonal basis of `ℂ^{F^×}`; the orthonormal system is `χ_j/√n`). -/ theorem chi_orthogonal (j k : ZMod n) : ∑ m, chi j m * (starRingEnd ℂ) (chi k m) = if j = k then (n : ℂ) else 0 := by have : ∀ m, chi j m * (starRingEnd ℂ) (chi k m) = ZMod.stdAddChar (m * (j - k)) := fun m => by rw [chi_conj, chi, ← AddChar.map_add_eq_mul] congr 1; ring simp_rw [this] rw [AddChar.sum_mulShift _ (ZMod.isPrimitive_stdAddChar n), ZMod.card] simp only [sub_eq_zero] split_ifs <;> simp /-- 20:E12, 20:E1 — clause (iii): the scale-shift `m ↦ m + 1` (the residue `g^m ↦ g^{m+1}`) has every chart mode as an eigenvector, with eigenphase `e^{2πi·j/n}` independent of the vector: `χ_j(m + 1) = e^{2πi j/n} χ_j(m)`. -/ theorem chi_shift (j m : ZMod n) : chi j (m + 1) = ZMod.stdAddChar j * chi j m ∧ ZMod.stdAddChar (j : ZMod n) = Complex.exp (2 * Real.pi * I * j.val / n) := by constructor · rw [chi, chi, mul_add, mul_one, AddChar.map_add_eq_mul, mul_comm] · rw [ZMod.stdAddChar_apply, ZMod.toCircle_apply] /-- 20:E12, 20:E13 — clause (i): Fourier inversion on the cycle, `v = (1/n) Σ_j ⟨v, χ_j⟩ χ_j`, with the constant mode carrying the mean, `⟨v, χ_0⟩ = Σ_m v(m)`, so the nontrivial modes carry `v − v̄·1`. -/ theorem chi_inversion (v : ZMod n → ℂ) : (∀ m, v m = (n : ℂ)⁻¹ * ∑ j, coef v j * chi j m) ∧ coef v 0 = ∑ m, v m ∧ ∀ m, v m - (n : ℂ)⁻¹ * ∑ m', v m' = (n : ℂ)⁻¹ * ∑ j ∈ univ.erase 0, coef v j * chi j m := by have hn : (n : ℂ) ≠ 0 := by exact_mod_cast NeZero.ne n have hkey : ∀ m, ∑ j, coef v j * chi j m = (n : ℂ) * v m := by intro m simp only [coef, sum_mul] rw [sum_comm] have : ∀ m', ∑ j, v m' * (starRingEnd ℂ) (chi j m') * chi j m = v m' * ∑ j, chi j m * (starRingEnd ℂ) (chi j m') := fun m' => by rw [mul_sum]; exact sum_congr rfl fun j _ => by ring simp_rw [this] have horth : ∀ m', ∑ j, chi j m * (starRingEnd ℂ) (chi j m') = if m' = m then (n : ℂ) else 0 := by intro m' have : ∀ j, chi j m * (starRingEnd ℂ) (chi j m') = ZMod.stdAddChar (j * (m - m')) := fun j => by rw [chi_conj, chi, ← AddChar.map_add_eq_mul] congr 1; ring simp_rw [this] rw [AddChar.sum_mulShift _ (ZMod.isPrimitive_stdAddChar n), ZMod.card] by_cases h : m' = m · subst h; simp · rw [ite_eq_right (fun e => h (sub_eq_zero.1 e).symm), ite_eq_right h]; simp simp_rw [horth] simp [mul_comm] have hmean : coef v 0 = ∑ m, v m := by simp only [coef, chi, zero_mul, AddChar.map_zero_eq_one, map_one, mul_one] refine ⟨fun m => ?_, hmean, fun m => ?_⟩ · rw [hkey, ← mul_assoc, inv_mul_cancel₀ hn, one_mul] · have hsplit := sum_erase_add univ (fun j => coef v j * chi j m) (mem_univ 0) rw [hkey] at hsplit have h0 : coef v 0 * chi 0 m = ∑ m', v m' := by rw [hmean, chi, zero_mul, AddChar.map_zero_eq_one, mul_one] rw [h0] at hsplit have : ∑ j ∈ univ.erase 0, coef v j * chi j m = (n : ℂ) * v m - ∑ m', v m' := by linear_combination hsplit rw [this, mul_sub, ← mul_assoc, inv_mul_cancel₀ hn, one_mul] /-- 20:E13, 20:C5 — Parseval on the cycle: `Σ_j |⟨v, χ_j⟩|² = n Σ_m |v(m)|²`; the chart modes are complete. -/ theorem chi_parseval (v : ZMod n → ℂ) : ∑ j, normSq (coef v j) = n * ∑ m, normSq (v m) := by have h := (chi_inversion v).1 apply Complex.ofReal_injective push_cast simp_rw [← Complex.mul_conj] have hc : ∀ j, (starRingEnd ℂ) (coef v j) = ∑ m, (starRingEnd ℂ) (v m) * chi j m := fun j => by simp only [coef, map_sum, map_mul, Complex.conj_conj] calc ∑ j, coef v j * (starRingEnd ℂ) (coef v j) = ∑ j, ∑ m, (starRingEnd ℂ) (v m) * (coef v j * chi j m) := by refine sum_congr rfl fun j _ => ?_ rw [hc, mul_sum]; exact sum_congr rfl fun m _ => by ring _ = ∑ m, (starRingEnd ℂ) (v m) * ∑ j, coef v j * chi j m := by rw [sum_comm]; exact sum_congr rfl fun m _ => by rw [mul_sum] _ = ∑ m, (starRingEnd ℂ) (v m) * ((n : ℂ) * v m) := by refine sum_congr rfl fun m _ => ?_ congr 1 have hn : (n : ℂ) ≠ 0 := by exact_mod_cast NeZero.ne n have := h m rw [this, ← mul_assoc, mul_inv_cancel₀ hn, one_mul] _ = (n : ℂ) * ∑ m, v m * (starRingEnd ℂ) (v m) := by rw [mul_sum]; exact sum_congr rfl fun m _ => by ring /-- 20:C5 — mean-square flatness: for a mean-removed vector `u ≠ 0` on the cycle (`Σ_m u(m) = 0`), the normalised correlations `r_j = |⟨u, χ_j⟩|/(‖u‖ ‖χ_j‖)` with the nonconstant modes satisfy `Σ_{j≠0} r_j² = 1` exactly, so their mean square over the `n − 1 = p − 2` nonconstant modes is `1/(p − 2)`: the root-mean-square correlation is `1/√(p − 2)`. -/ theorem flatness (u : ZMod n → ℂ) (hmean : ∑ m, u m = 0) (hu : u ≠ 0) : ∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m)) = 1 ∧ (∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m))) / ((n : ℝ) - 1) = 1 / ((n : ℝ) - 1) := by have hpos : 0 < ∑ m, normSq (u m) := by obtain ⟨m, hm⟩ : ∃ m, u m ≠ 0 := by by_contra h; push Not at h; exact hu (funext h) exact sum_pos' (fun m _ => normSq_nonneg _) ⟨m, mem_univ _, normSq_pos.2 hm⟩ have hn : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne n) have hden : (n : ℝ) * ∑ m, normSq (u m) ≠ 0 := (mul_pos hn hpos).ne' have h0 : coef u 0 = 0 := by rw [(chi_inversion u).2.1, hmean] have hsplit := sum_erase_add univ (fun j => normSq (coef u j)) (mem_univ 0) rw [chi_parseval, h0, normSq_zero, add_zero] at hsplit have h1 : ∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m)) = 1 := by rw [← sum_div, hsplit, div_self hden] exact ⟨h1, by rw [h1]⟩ end characters section eigen /-- 20:E12, 20:E1 — the multiplicative characters of the shell are eigenvectors of the scale-shift in the abstract reading: `χ(g^r x) = χ(g)^r χ(x)` for every `χ : F^× →* ℂ^×`. -/ theorem character_eigen {F : Type*} [Field F] (χ : Fˣ →* ℂˣ) (g x : Fˣ) (r : ℕ) : χ (g ^ r * x) = χ g ^ r * χ x := by rw [map_mul, map_pow] end eigen /-! ## The resonance: the von Mangoldt weight (row C2) -/ section resonance open ArithmeticFunction Finset /-- 20:C2 — `Λ = μ ∗ log` exactly on the divisor lattice: `Λ(n) = Σ_{d ∣ n} μ(d) log(n/d)`; and the support of `Λ` is the prime powers. (Hardy's limit `R_L → (φ(n)/n) Λ(n)` is the import A3.) -/ theorem vonMangoldt_moebius (m : ℕ) : vonMangoldt m = ∑ d ∈ m.divisors, (moebius d : ℝ) * Real.log ((m : ℝ) / d) ∧ (vonMangoldt m ≠ 0 ↔ IsPrimePow m) := by refine ⟨?_, vonMangoldt_ne_zero_iff⟩ rw [← moebius_mul_log_eq_vonMangoldt, mul_apply, Nat.sum_divisorsAntidiagonal (fun a b => (moebius : ArithmeticFunction ℝ) a * ArithmeticFunction.log b)] refine sum_congr rfl fun d hd => ?_ simp only [intCoe_apply, log_apply] rw [Nat.cast_div (Nat.dvd_of_mem_divisors hd) (by exact_mod_cast (Nat.pos_of_mem_divisors hd).ne')] end resonance /-! ## The strip (20:D8): the Euler product excludes zeros with real part at least one, and the functional equation confines the nontrivial zeros to the open strip, in orbits of the Klein four-group `s ↦ 1 − s`, `s ↦ s̄` (13 October 2026). -/ section strip open ComplexConjugate /-- A zero of `ζ` with real part at most zero is a trivial zero `−2(n+1)`: at `s' = 1 − s` the functional equation reads `ζ s = 2 (2π)^{−s'} Γ(s') cos(π s'/2) ζ(s')` with `Re s' ≥ 1`, where `ζ(s') ≠ 0` (the Euler product), so `cos(π s'/2) = 0`, `s'` an odd integer and `s` an even integer `≤ 0`; `s = 0` is excluded by `ζ 0 = −1/2`. -/ theorem zero_re_nonpos_trivial {s : ℂ} (h0 : riemannZeta s = 0) (hre : s.re ≤ 0) : ∃ n : ℕ, s = -2 * (n + 1) := by have hs0 : s ≠ 0 := fun h => by rw [h, riemannZeta_zero] at h0; norm_num at h0 set s' := 1 - s with hs' have hre' : 1 ≤ s'.re := by simp only [hs', Complex.sub_re, Complex.one_re]; linarith have hne : ∀ n : ℕ, s' ≠ -n := fun n h => by have := congrArg Complex.re h simp only [Complex.neg_re, Complex.natCast_re] at this have : (0 : ℝ) ≤ n := Nat.cast_nonneg n linarith have hne1 : s' ≠ 1 := fun h => hs0 (by rw [hs'] at h; linear_combination -h) have hfe := riemannZeta_one_sub hne hne1 have h1s : 1 - s' = s := by rw [hs']; ring rw [h1s, h0] at hfe have hz : riemannZeta s' ≠ 0 := riemannZeta_ne_zero_of_one_le_re hre' have hΓ : Complex.Gamma s' ≠ 0 := Complex.Gamma_ne_zero_of_re_pos (by linarith) have hpow : (2 * (Real.pi : ℂ)) ^ (-s') ≠ 0 := by rw [Complex.cpow_ne_zero_iff]; left exact mul_ne_zero two_ne_zero (Complex.ofReal_ne_zero.2 Real.pi_ne_zero) have hcos : Complex.cos ((Real.pi : ℂ) * s' / 2) = 0 := by have h := hfe.symm simp only [mul_eq_zero, two_ne_zero, false_or, hpow, hΓ, hz, or_false] at h exact h obtain ⟨k, hk⟩ := Complex.cos_eq_zero_iff.1 hcos have hπ : (Real.pi : ℂ) ≠ 0 := Complex.ofReal_ne_zero.2 Real.pi_ne_zero have hs'k : s' = 2 * k + 1 := by have : (Real.pi : ℂ) * s' = (Real.pi : ℂ) * (2 * k + 1) := by linear_combination 2 * hk exact mul_left_cancel₀ hπ this have hsk : s = -2 * k := by rw [← h1s, hs'k]; ring have hk0 : 0 ≤ k := by have := congrArg Complex.re hsk simp only [neg_mul, Complex.neg_re, Complex.mul_re, Complex.re_ofNat, Complex.im_ofNat, Complex.intCast_re, Complex.intCast_im, mul_zero, sub_zero] at this have : (0 : ℝ) ≤ k := by linarith exact_mod_cast this have hk1 : k ≠ 0 := fun h => hs0 (by rw [hsk, h]; simp) refine ⟨(k - 1).toNat, ?_⟩ have hk1' : 1 ≤ k := by omega have : ((k - 1).toNat : ℤ) = k - 1 := Int.toNat_of_nonneg (by omega) rw [hsk] have hcast : ((((k - 1).toNat : ℕ) : ℂ)) = (k : ℂ) - 1 := by rw [← Int.cast_natCast, this]; push_cast; ring rw [hcast]; ring /-- 20:D8, the strip: a nontrivial zero of `ζ` lies in the open strip `0 < Re s < 1`, and its Klein-four orbit under `s ↦ 1 − s` and `s ↦ s̄` consists of zeros: `Re s < 1` by the Euler product (`riemannZeta_ne_zero_of_one_le_re`), `0 < Re s` by the functional equation with the Euler product on the reflected side, `ζ(1 − s) = 0` by the functional equation (`riemannZeta_one_sub`) and `ζ(s̄) = 0` by `riemannZeta_conj`. -/ theorem zeros_in_strip {s : ℂ} (h0 : riemannZeta s = 0) (htriv : ¬∃ n : ℕ, s = -2 * (n + 1)) (h1 : s ≠ 1) : 0 < s.re ∧ s.re < 1 ∧ riemannZeta (1 - s) = 0 ∧ riemannZeta (conj s) = 0 := by have hlt : s.re < 1 := by by_contra h exact riemannZeta_ne_zero_of_one_le_re (not_lt.1 h) h0 have hpos : 0 < s.re := by by_contra h exact htriv (zero_re_nonpos_trivial h0 (not_lt.1 h)) refine ⟨hpos, hlt, ?_, ?_⟩ · have hne : ∀ n : ℕ, s ≠ -n := fun n h => by have := congrArg Complex.re h simp only [Complex.neg_re, Complex.natCast_re] at this have : (0 : ℝ) ≤ n := Nat.cast_nonneg n linarith rw [riemannZeta_one_sub hne h1, h0, mul_zero] · rw [riemannZeta_conj, h0, map_zero] end strip end FRC.Chart /-! inlined: FrcLedger/Theme/Strong.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Strong — the chart theme's strong field, crossover and series (10 October 2026) The readings of 21-gravity on the reals, moved from the paper module `FrcLedger/Gravity.lean` (which keeps every old name as an alias), every numeral re-anchored to the ledger's scale import (00:A7: `ln Ω = 283.5`, `Ω = 1.3 × 10¹²³`; `Theme/Chart.lean`'s `ln_omega_ledger`). The strong field: the operational cut `e^{2M/r_f} = Ω` with the ordering `r_* < r_f < M` exactly when `M > (ln Ω/2)²` (21:C12, P7); the photon sphere at `r = 2Gm` with `b_c = 2e·Gm` as the minimum of `r e^{2Gm/r}` (21:C12, P1); the shadow `+4.6 %` and ringdown `−4.4 %` bracketed from `e` and `√3` (21:P1); the innermost stable orbit at `r = 3 + √5` and the efficiency `5.48 %` against Schwarzschild's `5.72 %` (21:P1); the capacity ratio `1/ln²Ω = 1.24 × 10⁻⁵` at `283.5` (21:C13); the redshift's linear form (21:C4). The crossover: the registration root `η` of `wη² − 2η + w = 0` in `(0, 1)`, the crossover squeezed between its deep and Newtonian limits, the Tully–Fisher algebra (21:C19, P4, X2); the discriminant `0.051` at `g_N = 5a₀` against the simple interpolant (21:P4). The primordial fixed point `n_s = 1` (21:C18; the tilt at `283.5` is `Chart.tilt_ledger`). The dispersion symbol and the locked sum on `ℂ` (21:C15, C1). The series: the exponential reading composes and the isotropic Schwarzschild factor is `e^{−2 artanh(U/2)}` (21:C11); the post-Newtonian Taylor brackets (21:C8, P6); the preferred-frame scale `1/√Ω` at `1.3 × 10¹²³` (21:P2, C10); cardinality dilution (21:X8, C5). Classical (tier 2) on Mathlib's hierarchy; every bracket from `π` to six places, `e` to nine and the Taylor tail of `exp`. The finite content is proved with no axioms in the core (`FrcCore/Theme/Drift.lean`, `Theme/Lattice.lean`); the exact Mathlib variants are `Theme/Gravity.lean`'s. -/ namespace FRC.Strong open Real /-! ## Cardinality dilution (21:X8, C5) -/ section register /-- 21:X8, 21:C5 — the weakness of gravity as cardinality dilution: with the Planck mass the locality horizon, `m_P = √Ω`, the dimensionless coupling of two masses `m` is `(m/m_P)² = m²/Ω`, small because `Ω` is large. C5's frame covariance is not formal content. -/ theorem dilution (m Ω : ℝ) (hΩ : 0 < Ω) : (m / √Ω) ^ 2 = m ^ 2 / Ω := by rw [div_pow, sq_sqrt hΩ.le] end register /-! ## The strong field (21:C4, C12, C13, P1, P7) -/ section strongfield /-- 21:C12, 21:P7 — the operational cut and the slip core in the substrate coordinate (`G = 1`, `M` in Planck masses, `L = ln Ω`): `r_f = 2M/L` carries `e^{2M/r_f} = Ω` (the round-trip delay's factor); `r_* = √M < r_f` exactly when `M > (L/2)²`, and `r_f < M` exactly when `L > 2` (master E10). -/ theorem operational_cut (M L Ω : ℝ) (hM : 0 < M) (hL : 0 < L) (hΩ : L = log Ω) (hΩ0 : 0 < Ω) : exp (2 * M / (2 * M / L)) = Ω ∧ (√M < 2 * M / L ↔ (L / 2) ^ 2 < M) ∧ (2 * M / L < M ↔ 2 < L) := by refine ⟨?_, ?_, ?_⟩ · have : 2 * M / (2 * M / L) = L := by field_simp rw [this, hΩ, exp_log hΩ0] · rw [Real.sqrt_lt' (by positivity), div_pow, lt_div_iff₀ (by positivity)] constructor <;> intro h <;> nlinarith · rw [div_lt_iff₀ hL] constructor <;> intro h <;> nlinarith /-- 21:P1 — the photon sphere (`prop:shadow`, `rem:exponential`): the impact parameter `b(r) = r e^{2Gm/r}` of the exponential metric satisfies `b(r) ≥ 2e·Gm` for every `r > 0`, with equality exactly at `r = 2Gm` (from `x + 1 ≤ eˣ`, strict off `x = 0`): the photon sphere is at `r_ph = 2Gm`, the critical impact parameter `b_c = 2e·Gm`. -/ theorem photon_sphere (Gm r : ℝ) (hG : 0 < Gm) (hr : 0 < r) : 2 * exp 1 * Gm ≤ r * exp (2 * Gm / r) ∧ (r * exp (2 * Gm / r) = 2 * exp 1 * Gm ↔ r = 2 * Gm) := by have hsplit : exp (2 * Gm / r) = exp 1 * exp (2 * Gm / r - 1) := by rw [← exp_add]; ring_nf have hx := Real.add_one_le_exp (2 * Gm / r - 1) have hkey : 2 * exp 1 * Gm = r * exp 1 * (2 * Gm / r - 1 + 1) := by field_simp; ring have hpos : 0 < r * exp 1 := by positivity constructor · rw [hsplit, hkey] calc r * exp 1 * (2 * Gm / r - 1 + 1) ≤ r * exp 1 * exp (2 * Gm / r - 1) := mul_le_mul_of_nonneg_left hx hpos.le _ = r * (exp 1 * exp (2 * Gm / r - 1)) := by ring · constructor · intro h by_contra hne have hx' : 2 * Gm / r - 1 ≠ 0 := by intro h0 apply hne have : 2 * Gm / r = 1 := by linarith rw [div_eq_one_iff_eq hr.ne'] at this linarith have hlt := Real.add_one_lt_exp hx' have : r * exp 1 * (2 * Gm / r - 1 + 1) < r * exp 1 * exp (2 * Gm / r - 1) := mul_lt_mul_of_pos_left hlt hpos rw [hsplit, ← mul_assoc] at h linarith · rintro rfl have : 2 * Gm / (2 * Gm) = 1 := by field_simp rw [this]; ring /-- `√3` to seven places. -/ theorem sqrt_three_bounds : (1.7320508 : ℝ) < √3 ∧ √3 < 1.7320509 := ⟨(Real.lt_sqrt (by norm_num)).mpr (by norm_num), (Real.sqrt_lt' (by norm_num)).mpr (by norm_num)⟩ /-- 21:P1 — the shadow and the ringdown against general relativity, bracketed from `e` (nine places) and `√3`: the critical impact parameters `b_c = 2e·Gm` (this work) and `3√3·Gm` (Schwarzschild) have ratio `2e/(3√3)` between `1.0462` and `1.0463` (the shadow `+4.6 %`), and the eikonal ringdown frequency, `∝ 1/b_c`, ratio `3√3/(2e)` between `0.9557` and `0.9558` (`−4.4 %`); the Sgr A* excess `(4e − 6√3) θ_g` at the GRAVITY `θ_g = 5.12 µas` [data, A8] lies between `2.46` and `2.47 µas` (the `2.5 µas` of the text). -/ theorem shadow_bracket : (1.0462 : ℝ) < 2 * exp 1 / (3 * √3) ∧ 2 * exp 1 / (3 * √3) < 1.0463 ∧ (0.9557 : ℝ) < 3 * √3 / (2 * exp 1) ∧ 3 * √3 / (2 * exp 1) < 0.9558 ∧ (2.46 : ℝ) < (4 * exp 1 - 6 * √3) * 5.12 ∧ (4 * exp 1 - 6 * √3) * 5.12 < 2.47 := by have e1 := Real.exp_one_gt_d9 have e2 := Real.exp_one_lt_d9 obtain ⟨s1, s2⟩ := sqrt_three_bounds have hs : (0 : ℝ) < √3 := by positivity have he : (0 : ℝ) < exp 1 := exp_pos 1 refine ⟨?_, ?_, ?_, ?_, by nlinarith, by nlinarith⟩ · rw [lt_div_iff₀ (by positivity)]; nlinarith · rw [div_lt_iff₀ (by positivity)]; nlinarith · rw [lt_div_iff₀ (by positivity)]; nlinarith · rw [div_lt_iff₀ (by positivity)]; nlinarith /-- 21:P1 — the innermost stable circular orbit of the exponential metric (`G = m = 1`, isotropic radius), with the circular-orbit relations of the paper's `prop:isco` taken as given and not formalised (`L² = e^{2/r} r²/(r − 2)` and `E² = e^{−2/r}(r − 1)/(r − 2)` for a circular orbit at `r > 2`): what is proved is that `log L²` has derivative `(r² − 6r + 4)/(r²(r − 2))`, that `r_ISCO = 3 + √5` is the root of `r² − 6r + 4` above `2`, and that `(r − 1)/(r − 2) = r/4` there, so `E² = e^{−2/r} r/4` at the orbit. -/ theorem isco (r : ℝ) (hr : 2 < r) : HasDerivAt (fun r : ℝ => 2 / r + 2 * log r - 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 := by have h5 := Real.sq_sqrt (show (0 : ℝ) ≤ 5 by norm_num) have hs5 : (0 : ℝ) < √5 := by positivity refine ⟨?_, by linear_combination h5, by linarith, ?_⟩ · have hr0 : r ≠ 0 := by linarith have hr2 : r - 2 ≠ 0 := by linarith have d1 : HasDerivAt (fun r : ℝ => 2 / r) (-(2 / r ^ 2)) r := by have := (hasDerivAt_inv hr0).const_mul 2 convert this using 1 <;> [funext x; skip] <;> ring have d2 : HasDerivAt (fun r : ℝ => 2 * log r) (2 * r⁻¹) r := (Real.hasDerivAt_log hr0).const_mul 2 have d3 : HasDerivAt (fun r : ℝ => log (r - 2)) (1 / (r - 2)) r := ((hasDerivAt_id' r).sub_const 2).log hr2 convert (d1.add d2).sub d3 using 1 field_simp ring · rw [div_eq_div_iff (by linarith) (by norm_num)] linear_combination -h5 /-- A bracket of `e^{−x}` from `x₁ < x < x₂`, a lower bound of `e^{x₁}` and an upper bound of `e^{x₂}`. -/ theorem exp_neg_bracket {x x₁ x₂ lo hi : ℝ} (hx₁ : x₁ < x) (hx₂ : x < x₂) (hlo : 0 < lo) (h1 : lo < exp x₁) (h2 : exp x₂ < hi) : hi⁻¹ < exp (-x) ∧ exp (-x) < lo⁻¹ := by constructor · calc hi⁻¹ < (exp x₂)⁻¹ := inv_strictAnti₀ (exp_pos _) h2 _ = exp (-x₂) := (exp_neg _).symm _ < exp (-x) := exp_lt_exp.mpr (by linarith) · calc exp (-x) < exp (-x₁) := exp_lt_exp.mpr (by linarith) _ = (exp x₁)⁻¹ := exp_neg _ _ < lo⁻¹ := inv_strictAnti₀ hlo h1 /-- The Taylor brackets of `e^t` at the two ends of `t = 2/r_ISCO = (3 − √5)/2`. -/ theorem exp_isco_tail_bounds : (1.465161 : ℝ) < exp 0.381966 ∧ exp (0.3819661 : ℝ) < 1.465163 := by constructor · have h := abs_le.1 (Real.exp_bound (x := 0.381966) (by rw [abs_of_pos (by norm_num)]; norm_num) (n := 7) (by norm_num)) rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.381966)] at h have h1 := h.1 norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢ linarith · have h := Real.exp_bound' (x := 0.3819661) (by norm_num) (by norm_num) (n := 7) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢ linarith /-- `√5` to seven places. -/ theorem sqrt_five_bounds : (2.2360679 : ℝ) < √5 ∧ √5 < 2.2360680 := ⟨(Real.lt_sqrt (by norm_num)).mpr (by norm_num), (Real.sqrt_lt' (by norm_num)).mpr (by norm_num)⟩ /-- 21:P1 — the accretion efficiency bracketed: at `r_ISCO = 3 + √5` the orbital energy `E = √(e^{−2/r} r/4)` lies between `0.9452` and `0.9453`, so `1 − E` is between `5.47 %` and `5.48 %` (the text's `5.48 %`), against Schwarzschild's `1 − √(8/9)` between `5.71 %` and `5.72 %`. -/ theorem isco_efficiency : (0.0547 : ℝ) < 1 - √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) ∧ 1 - √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) < 0.0548 ∧ (0.0571 : ℝ) < 1 - √(8 / 9) ∧ 1 - √(8 / 9) < (0.0572 : ℝ) := by obtain ⟨s1, s2⟩ := sqrt_five_bounds obtain ⟨t1, t2⟩ := exp_isco_tail_bounds have hx : 2 / (3 + √5) = (3 - √5) / 2 := by have h5 := Real.sq_sqrt (show (0 : ℝ) ≤ 5 by norm_num) rw [div_eq_div_iff (by positivity) (by norm_num)] linear_combination h5 obtain ⟨hlo, hhi⟩ := exp_neg_bracket (x := 2 / (3 + √5)) (x₁ := 0.381966) (x₂ := 0.3819661) (by rw [hx]; linarith) (by rw [hx]; linarith) (by norm_num) t1 t2 norm_num at hlo hhi have hE := exp_pos (-(2 / (3 + √5))) have hv1 : (0.89341 : ℝ) < exp (-(2 / (3 + √5))) * (3 + √5) / 4 := by nlinarith have hv2 : exp (-(2 / (3 + √5))) * (3 + √5) / 4 < (0.89345 : ℝ) := by nlinarith have hq1 : (0.9452 : ℝ) < √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) := (Real.lt_sqrt (by norm_num)).mpr (by nlinarith) have hq2 : √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) < (0.9453 : ℝ) := (Real.sqrt_lt' (by norm_num)).mpr (by nlinarith) have hs1 : (0.9428 : ℝ) < √(8 / 9) := (Real.lt_sqrt (by norm_num)).mpr (by norm_num) have hs2 : √(8 / 9 : ℝ) < 0.9429 := (Real.sqrt_lt' (by norm_num)).mpr (by norm_num) refine ⟨by linarith, by linarith, by linarith, by linarith⟩ /-- The arithmetic behind 21:C13's capacity ratio: for `r_f = r_s/L` the square of `r_f/r_s` is `1/L²`, and at `L = ln Ω = 283.5` (the scale import) the ratio lies between `1.24 × 10⁻⁵` and `1.25 × 10⁻⁵` (the text's `1.24 × 10⁻⁵`); that the externally resolvable capacity scales as `(r_f/r_s)²` is the paper's count, not formal content. -/ theorem capacity_ratio (rs L : ℝ) (hrs : rs ≠ 0) (hL : L ≠ 0) : (rs / L / rs) ^ 2 = 1 / L ^ 2 := by field_simp theorem capacity_ratio_numeral : (1.24e-5 : ℝ) < 1 / 283.5 ^ 2 ∧ (1 / 283.5 ^ 2 : ℝ) < 1.25e-5 := by norm_num /-- 21:C4 — the redshift as clock rate: the bias field `e^{−u}` with `u = Gm/rc²` gives `Δf/f = 1 − e^{−u} = u + O(u²)`, `|1 − e^{−u} − u| ≤ u²` on `0 ≤ u ≤ 1`. -/ theorem redshift_linear (u : ℝ) (h0 : 0 ≤ u) (h1 : u ≤ 1) : |1 - exp (-u) - u| ≤ u ^ 2 := by have h := Real.exp_bound (x := -u) (by rw [abs_neg, abs_of_nonneg h0]; exact h1) (n := 2) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial, abs_neg, abs_of_nonneg h0] at h rw [abs_le] at h ⊢ constructor <;> nlinarith [sq_nonneg u] end strongfield /-! ## The floor and the crossover (21:C19, P4, X2) -/ section floor /-- 21:C19, 21:P4 — the registration root: for `0 < w < 1` the quadratic `wη² − 2η + w = 0` (rational in the paper's `w`, here over `ℝ`) has exactly the roots `(1 ∓ √(1 − w²))/w`; the smaller, `η = (1 − √(1 − w²))/w`, lies in `(0, 1)` and the larger exceeds `1`, so the in-`(0, 1)` root that fixes the resolved fraction `f = 1 − η^a` is unique. -/ theorem registration_root (w : ℝ) (hw0 : 0 < w) (hw1 : 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) := by have hw2 : 0 ≤ 1 - w ^ 2 := by nlinarith set s := √(1 - w ^ 2) with hs have hs2 : s ^ 2 = 1 - w ^ 2 := Real.sq_sqrt hw2 have hs0 : 0 ≤ s := Real.sqrt_nonneg _ have hs1 : s < 1 := by rw [hs, Real.sqrt_lt' (by norm_num)]; nlinarith have hsw : 1 - w < s := by nlinarith [mul_pos hw0 (sub_pos.mpr hw1)] have hab : (1 - s) / w + (1 + s) / w = 2 / w := by rw [← add_div]; ring_nf have hsum : w * (2 / w) = 2 := by field_simp have hprod : w * ((1 - s) / w * ((1 + s) / w)) = w := by rw [div_mul_div_comm, ← mul_div_assoc, div_eq_iff (by positivity)] linear_combination (-w) * hs2 have hquad : ∀ x : ℝ, w * x ^ 2 - 2 * x + w = w * (x - (1 - s) / w) * (x - (1 + s) / w) := by intro x have e : w * (x - (1 - s) / w) * (x - (1 + s) / w) = w * x ^ 2 - w * ((1 - s) / w + (1 + s) / w) * x + w * ((1 - s) / w * ((1 + s) / w)) := by ring rw [e, hab, hsum, hprod] refine ⟨?_, div_pos (by linarith) hw0, ?_, ?_, ?_⟩ · rw [hquad]; ring · rw [div_lt_one hw0]; linarith · rw [lt_div_iff₀ hw0]; linarith · intro x hx rw [hquad] at hx rcases mul_eq_zero.mp hx with h | h · rcases mul_eq_zero.mp h with h | h · exact absurd h hw0.ne' · left; linarith · right; linarith /-- 21:C19, 21:P4 — the crossover `g_obs = g_N/(1 − e^{−√x})`, `x = g_N/a₀`, squeezed: with `t = √x > 0`, `1 ≤ t/(1 − e^{−t})`, and `t/(1 − e^{−t}) ≤ 1/(1 − 3t/4)` for `t ≤ 1`; and the Tully–Fisher algebra is exact: `v² = g_obs r` with `g_obs = √(g_N a₀)`, `g_N = GM/r²`, gives `v⁴ = GMa₀`. -/ theorem crossover_limits (t : ℝ) (ht : 0 < t) : 0 < 1 - exp (-t) ∧ 1 ≤ t / (1 - exp (-t)) ∧ (t ≤ 1 → t / (1 - 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₀) := by have hpos : 0 < 1 - exp (-t) := by have : exp (-t) < exp 0 := exp_lt_exp.mpr (by linarith) rw [exp_zero] at this linarith refine ⟨hpos, ?_, ?_, ?_⟩ · rw [le_div_iff₀ hpos] have := Real.add_one_le_exp (-t) linarith · intro ht1 have h := Real.exp_bound (x := -t) (by rw [abs_neg, abs_of_pos ht]; exact ht1) (n := 2) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial, abs_neg, abs_of_pos ht] at h rw [abs_le] at h have h34 : 0 < 1 - 3 * t / 4 := by linarith rw [div_le_div_iff₀ hpos h34] nlinarith · intro G M r a₀ v hr hGM ha v2 have hnn : 0 ≤ G * M / r ^ 2 * a₀ := by positivity calc v ^ 4 = (v ^ 2) ^ 2 := by ring _ = (√(G * M / r ^ 2 * a₀)) ^ 2 * r ^ 2 := by rw [v2]; ring _ = G * M / r ^ 2 * a₀ * r ^ 2 := by rw [Real.sq_sqrt hnn] _ = G * M * a₀ := by field_simp /-- 21:C19, 21:P4, 21:X2 — the deep limit: `t/(1 − e^{−t}) → 1` as `t → 0⁺`, so `g_obs/√(g_N a₀) → 1` — the deep regime `g_obs = √(g_N a₀)`, the floor read as noise with no dark sector. -/ theorem crossover_deep_limit : Filter.Tendsto (fun t : ℝ => t / (1 - exp (-t))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) := by have hc : ContinuousAt (fun t : ℝ => 1 / (1 - 3 * t / 4)) 0 := by apply ContinuousAt.div continuousAt_const · fun_prop · norm_num have hup : Filter.Tendsto (fun t : ℝ => 1 / (1 - 3 * t / 4)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) := by have := hc.tendsto.mono_left (nhdsWithin_le_nhds : nhdsWithin (0 : ℝ) (Set.Ioi 0) ≤ nhds 0) simpa using this refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hup ?_ ?_ · filter_upwards [self_mem_nhdsWithin] with t ht exact (crossover_limits t ht).2.1 · filter_upwards [Ioo_mem_nhdsGT (show (0 : ℝ) < 1 by norm_num)] with t ht exact (crossover_limits t ht.1).2.2.1 ht.2.le /-- 21:C19, 21:P4 — the Newtonian limit: `1 − e^{−t} → 1` as `t → ∞`, so `g_obs/g_N → 1` for `x → ∞`. -/ theorem crossover_newton_limit : Filter.Tendsto (fun t : ℝ => 1 - exp (-t)) Filter.atTop (nhds 1) := by have := Real.tendsto_exp_neg_atTop_nhds_zero simpa using tendsto_const_nhds.sub this /-- The Taylor brackets of `e^t` at the two ends of `t = √5 − 2`. -/ theorem exp_root_five_tail_bounds : (1.2662602 : ℝ) < exp 0.2360679 ∧ exp (0.2360680 : ℝ) < 1.2662605 := by constructor · have h := abs_le.1 (Real.exp_bound (x := 0.2360679) (by rw [abs_of_pos (by norm_num)]; norm_num) (n := 7) (by norm_num)) rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.2360679)] at h have h1 := h.1 norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢ linarith · have h := Real.exp_bound' (x := 0.2360680) (by norm_num) (by norm_num) (n := 7) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢ linarith /-- 21:P4 — the discriminant against the simple interpolant at `g_N = 5a₀`: the crossover `ν(5) = 1/(1 − e^{−√5})` lies between `1.11966` and `1.11967`, the simple interpolant `ν_s(5) = 1/2 + √(1/4 + 1/5)` between `1.17082` and `1.17083`, so they part by between `0.0511` and `0.0512` in `g_obs/g_N` (the text's `0.05`). -/ theorem interpolant_discriminant : (1.11966 : ℝ) < 1 / (1 - exp (-√5)) ∧ 1 / (1 - exp (-√5)) < 1.11967 ∧ (1.17082 : ℝ) < 1 / 2 + √(1 / 4 + 1 / 5) ∧ 1 / 2 + √(1 / 4 + 1 / 5) < 1.17083 ∧ (0.0511 : ℝ) < (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) ∧ (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) < 0.0512 := by obtain ⟨s1, s2⟩ := sqrt_five_bounds obtain ⟨t1, t2⟩ := exp_root_five_tail_bounds have hm1 := Real.exp_neg_one_gt_d9 have hm2 := Real.exp_neg_one_lt_d9 have hsplit : exp (-√5) = exp (-1) * exp (-1) * exp (2 - √5) := by rw [← exp_add, ← exp_add]; ring_nf obtain ⟨hlo, hhi⟩ := exp_neg_bracket (x := √5 - 2) (x₁ := 0.2360679) (x₂ := 0.2360680) (by linarith) (by linarith) (by norm_num) t1 t2 norm_num at hlo hhi have hm : (0 : ℝ) < exp (-1) := exp_pos _ have hq1 : (0.106877 : ℝ) < exp (-√5) := by rw [hsplit]; nlinarith [mul_pos hm hm] have hq2 : exp (-√5) < (0.106878 : ℝ) := by rw [hsplit]; nlinarith [mul_pos hm hm] have hden : (0 : ℝ) < 1 - exp (-√5) := by linarith have hr1 : (1.11966 : ℝ) < 1 / (1 - exp (-√5)) := by rw [lt_div_iff₀ hden]; linarith have hr2 : 1 / (1 - exp (-√5)) < (1.11967 : ℝ) := by rw [div_lt_iff₀ hden]; linarith have hs1 : (0.67082 : ℝ) < √(1 / 4 + 1 / 5) := (Real.lt_sqrt (by norm_num)).mpr (by norm_num) have hs2 : √(1 / 4 + 1 / 5 : ℝ) < 0.67083 := (Real.sqrt_lt' (by norm_num)).mpr (by norm_num) refine ⟨hr1, hr2, by linarith, by linarith, by linarith, by linarith⟩ end floor /-! ## The primordial fixed point (21:C18) -/ section primordial /-- 21:C18 — the fixed point: for a power law `P(k) = k^n` the dimensionless `k³P(k)` is the same at every scale `k > 0` exactly when `n = −3`, i.e. `n_s − 1 = n + 3 = 0`, the Harrison–Zel'dovich `n_s = 1`, uniquely; that the drive's jitter spectrum is this fixed point is the paper's argument. -/ theorem scale_invariance_iff (n : ℝ) : (∀ k : ℝ, 0 < k → k ^ 3 * k ^ n = 1) ↔ n = -3 := by constructor · intro h have h2 := h 2 (by norm_num) have h3 : (2 : ℝ) ^ (n + 3) = 1 := by rw [rpow_add (by norm_num : (0 : ℝ) < 2), show (2 : ℝ) ^ (3 : ℝ) = 2 ^ (3 : ℕ) by exact_mod_cast rpow_natCast 2 3] linarith have hl := congrArg Real.log h3 rw [Real.log_rpow (by norm_num), Real.log_one] at hl rcases mul_eq_zero.mp hl with h | h · linarith · exact absurd h (Real.log_pos (by norm_num)).ne' · rintro rfl k hk rw [Real.rpow_neg hk.le, show (3 : ℝ) = (3 : ℕ) by norm_num, rpow_natCast] exact mul_inv_cancel₀ (pow_ne_zero 3 hk.ne') end primordial /-! ## The dispersion symbol and the locked sum (21:C1, C15) -/ section lattice /-- 21:C15 — the dispersion symbol: the central second difference acts on the plane wave `e^{ikx}` by `−(2 − 2 cos k) = −4 sin²(k/2)`; the wave equation, its two polarisations and the speed `c` are the package's. -/ theorem dispersion_symbol (k : ℝ) : 2 - 2 * cos k = 4 * sin (k / 2) ^ 2 := by have h := Real.cos_two_mul (k / 2) rw [show 2 * (k / 2) = k by ring] at h rw [h, Real.cos_sq']; ring /-- 21:C1 — the coherent coefficient: a locked cluster of `m` cells with one phase sums with coefficient exactly `m`, `‖Σ_{j linarith rw [show -(2 * (1 / 2 * log ((1 + U / 2) / (1 - U / 2)))) = -log ((1 + U / 2) / (1 - U / 2)) by ring, exp_neg, exp_log hpos, inv_div] /-- 21:C8, 21:P6, 21:C7 — the post-Newtonian inputs as Taylor brackets on `|U| ≤ 1/2`: the exponential metric's `A = e^{−2U}`, `B = e^{2U}` against the isotropic Schwarzschild `A_S = ((1 − U/2)/(1 + U/2))²`, `B_S = (1 + U/2)⁴` satisfy `|A − A_S − U³/6| ≤ 3U⁴` and `|B − B_S − U²/2| ≤ 3|U|³`: the single-potential inputs consumed by C23 coincide through first post-Newtonian order (`A` to `O(U²)`, `B` to `O(U)`) and part at 2PN with `δA = U³/6`, `δB = U²/2`; the two-body superposition of C23 is the package's. -/ theorem pn_series (U : ℝ) (hU : |U| ≤ 1 / 2) : |exp (-(2 * U)) - ((1 - U / 2) / (1 + U / 2)) ^ 2 - U ^ 3 / 6| ≤ 3 * U ^ 4 ∧ |exp (2 * U) - (1 + U / 2) ^ 4 - U ^ 2 / 2| ≤ 3 * |U| ^ 3 := by have hU' := abs_le.1 hU have hden : 1 + U / 2 ≠ 0 := by intro h; linarith [hU'.1] have hden2 : (9 / 16 : ℝ) ≤ (1 + U / 2) ^ 2 := by nlinarith [hU'.1] have hU4 : 0 ≤ U ^ 4 := by positivity have habs4 : |U| ^ 4 = U ^ 4 := by rw [← abs_pow, abs_of_nonneg hU4] have habs3 : |U| ^ 3 * |U| = U ^ 4 := by rw [← pow_succ, ← abs_pow, abs_of_nonneg (by positivity)] have hU3 : 0 ≤ |U| ^ 3 := by positivity constructor · have h := Real.exp_bound (x := -(2 * U)) (by rw [abs_neg, abs_mul, abs_two]; linarith) (n := 4) (by norm_num) rw [abs_neg, abs_mul, abs_two] at h norm_num [Finset.sum_range_succ, Nat.factorial] at h rw [abs_le] at h have hpow : (2 * |U|) ^ 4 = 16 * U ^ 4 := by rw [mul_pow, habs4]; norm_num rw [hpow] at h have hA : ((1 - U / 2) / (1 + U / 2)) ^ 2 - (1 - 2 * U + 2 * U ^ 2 - 3 / 2 * U ^ 3) = U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2 := by rw [div_pow, eq_div_iff (pow_ne_zero 2 hden), sub_mul, div_mul_cancel₀ _ (pow_ne_zero 2 hden)] ring have hrem : |U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2| ≤ 2.12 * U ^ 4 := by rw [abs_div, abs_mul, abs_of_nonneg hU4, abs_of_pos (by positivity : (0 : ℝ) < (1 + U / 2) ^ 2), div_le_iff₀ (by positivity)] have : |1 + 3 * U / 8| ≤ 1.1875 := by rw [abs_le]; constructor <;> linarith [hU'.1, hU'.2] nlinarith [abs_nonneg (1 + 3 * U / 8)] rw [abs_le] at hrem have hA' : ((1 - U / 2) / (1 + U / 2)) ^ 2 = 1 - 2 * U + 2 * U ^ 2 - 3 / 2 * U ^ 3 + U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2 := by linarith [hA] rw [hA', abs_le] constructor <;> nlinarith [hrem.1, hrem.2, h.1, h.2] · have h := Real.exp_bound (x := 2 * U) (by rw [abs_mul, abs_two]; linarith) (n := 3) (by norm_num) rw [abs_mul, abs_two] at h norm_num [Finset.sum_range_succ, Nat.factorial] at h rw [abs_le] at h ⊢ have hpow : (2 * |U|) ^ 3 = 8 * |U| ^ 3 := by rw [mul_pow]; norm_num rw [hpow] at h have hU4' : U ^ 4 ≤ |U| ^ 3 / 2 := by rw [← habs3]; nlinarith have hcube : U ^ 3 ≤ |U| ^ 3 ∧ -(|U| ^ 3) ≤ U ^ 3 := by constructor · calc U ^ 3 ≤ |U ^ 3| := le_abs_self _ _ = |U| ^ 3 := abs_pow U 3 · calc -(|U| ^ 3) = -|U ^ 3| := by rw [abs_pow] _ ≤ U ^ 3 := neg_abs_le _ constructor <;> nlinarith [h.1, h.2, hcube.1, hcube.2] /-- 21:P2, 21:C10 — the numeral behind the preferred-frame scale: the drive's signature is `O(1/√Ω)` (the paper's `α₁, α₂`), and at the scale import's `Ω = 1.3 × 10¹²³` (00:A7) this lies between `2.7` and `2.8 × 10⁻⁶²` (the row's `3 × 10⁻⁶²`). -/ theorem preferred_frame_scale : (2.7e-62 : ℝ) < 1 / √(1.3e123) ∧ 1 / √(1.3e123) < 2.8e-62 := by have hs : 0 < √(1.3e123 : ℝ) := Real.sqrt_pos.2 (by norm_num) constructor · rw [lt_one_div (by norm_num) hs, Real.sqrt_lt' (by norm_num)]; norm_num · rw [one_div_lt hs (by norm_num), Real.lt_sqrt (by norm_num)]; norm_num end series end FRC.Strong /-! inlined: FrcLedger/Theme/Gravity.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Gravity — the gravity theme on Mathlib: the exact faces of 21-gravity (10 October 2026) The exact Mathlib variants of 21-gravity's rows, moved from the paper module `FrcLedger/Gravity.lean` (which keeps every old name as an alias): the Carrier register on a field with `4S + 1 = 0` — the calibration congruence, the register value `G = 2S`, the action quantum as the quarter-turn pair (21:A1, C2, C5, C16); the count face of the area law and the merger law on `ℤ` (21:C13); the cover forcing and the PPN triangle over `ℚ` (21:A9, C7, C8, C25); the mass–energy channel as a gcd (21:A9); the central difference's anti-self-adjointness and the finite Fourier shift theorem on `ZMod N` (21:C9, C20). No reals here (gate G09): the chart readings are `Theme/Strong.lean`'s. The core proves the same faces with no axioms (`FrcCore/Theme/Gravity.lean`, `Theme/Drift.lean`, `Theme/Lattice.lean`, `Theme/Shift.lean`); these are their Mathlib counterparts on the classical hierarchy. -/ namespace FRC.GravML /-! ## The Carrier register (21:A1, C2, C5, C16) -/ section register variable {K : Type*} [Field K] /-- 21:C16, 21:A1 — the calibration congruence: on the Carrier chart `4S + 1 = 0` the full cycle `2π ↦ 4S` is `−1` and `(4S)² = 1`, one residue relation. -/ theorem calibration_congruence (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) : ((4 * S : ℕ) : K) = -1 ∧ ((4 * S : ℕ) : K) ^ 2 = 1 := by push_cast at hΩ ⊢ exact ⟨by linear_combination hΩ, by linear_combination (4 * (S : K) - 1) * hΩ⟩ /-- 21:C2, 21:C5, 21:C16 — the register value of the Newton constant, `G = 2S`, on the Carrier chart `4S + 1 = 0`: `2G = −1` (the half-cycle); `(−2) G = 1`, the face convention `4π ↦ −2` with `G = (−2)⁻¹`; the Gauss count `(2 · 4S) G = 1`; `c² = 2⁻¹ = 2S + 1` and `G = −c²` (the chart ratio `4π/2π = 2` is read as `(−2)/(−1)`). The uniqueness of the linear solution is `Dimensions.G_unique`. -/ theorem newton_register (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) : 2 * ((2 * S : ℕ) : K) = -1 ∧ (-2) * ((2 * S : ℕ) : K) = 1 ∧ (2 * ((4 * S : ℕ) : K)) * ((2 * S : ℕ) : K) = 1 ∧ 2 * ((2 * S + 1 : ℕ) : K) = 1 ∧ ((2 * S + 1 : ℕ) : K) = 2⁻¹ ∧ ((2 * S : ℕ) : K) = -((2 * S + 1 : ℕ) : K) := by push_cast at hΩ ⊢ refine ⟨by linear_combination hΩ, by linear_combination -hΩ, by linear_combination (4 * (S : K) - 1) * hΩ, by linear_combination hΩ, ?_, by linear_combination hΩ⟩ exact eq_inv_of_mul_eq_one_left (by linear_combination hΩ) /-- On the Carrier `𝔽_Ω`, `Ω = 4S + 1` prime, `2 ≠ 0` (`Ω` is odd). -/ theorem carrier_two_ne_zero (S : ℕ) [hp : Fact (Nat.Prime (4 * S + 1))] : (2 : ZMod (4 * S + 1)) ≠ 0 := by rw [show (2 : ZMod (4 * S + 1)) = ((2 : ℕ) : ZMod (4 * S + 1)) by norm_cast, Ne, ZMod.natCast_eq_zero_iff] intro hd have h1 : 4 * S + 1 ≤ 2 := Nat.le_of_dvd (by norm_num) hd have h2 : 2 ≤ 4 * S + 1 := hp.out.two_le omega /-- In any field with `4S + 1 = 0` and `2 ≠ 0`, a quarter-turn `i² = −1` gives a square root of `S`, `r = i/2`, with `(2r)² = −1`. -/ theorem hbar_of_quarter_turn {K : Type*} [Field K] (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) (h2 : (2 : K) ≠ 0) (i : K) (hi : i ^ 2 = -1) : ∃ r : K, r ^ 2 = (S : K) ∧ (2 * r) ^ 2 = -1 := by push_cast at hΩ have h4 : (2⁻¹ : K) ^ 2 * 4 = 1 := by field_simp; norm_num refine ⟨i * 2⁻¹, ?_, ?_⟩ · calc (i * 2⁻¹) ^ 2 = i ^ 2 * (2⁻¹) ^ 2 := by ring _ = -1 * (2⁻¹) ^ 2 := by rw [hi] _ = (S : K) := by linear_combination (-(2⁻¹ : K) ^ 2) * hΩ + (S : K) * h4 · have : 2 * (i * 2⁻¹) = i := by field_simp rw [this, hi] /-- 21:C5, 21:C16, 21:A1 — the action quantum as the quarter-turn pair: on every Carrier `Ω = 4S + 1` prime, `S` is a square (`S = (i/2)²` with `i² = −1`, since `4S = −1`), so `ħ = 2√S` has `ħ² = 4S = −1` — `ħ` is one of the quarter-turn pair `±i`. -/ theorem hbar_register (S : ℕ) [Fact (Nat.Prime (4 * S + 1))] : ∃ r : ZMod (4 * S + 1), r ^ 2 = (S : ZMod (4 * S + 1)) ∧ (2 * r) ^ 2 = -1 := by obtain ⟨i, hi⟩ : IsSquare (-1 : ZMod (4 * S + 1)) := ZMod.exists_sq_eq_neg_one_iff.mpr (by omega) exact hbar_of_quarter_turn S (ZMod.natCast_self _) (carrier_two_ne_zero S) i (by rw [sq]; exact hi.symm) end register /-! ## The count face and the cover forcing (21:A9, C7, C8, C13, C25) -/ section count /-- 21:C13 — the count face of the area law on a symmetry-complete shell `p = 4κ + 1`: with `S = (p² − 1)/4`, i.e. `4S + 1 = p²` for `S = κ(4κ + 2)`, and the coordinate area `A = p(p + 1)`, the ratio `S/A = κ/p` holds exactly (`Sp = κA`) and `S = (A/4)(1 − 1/p)` (`4Sp = A(p − 1)`) — the Bekenstein quarter as the `Q₄` quotient. -/ theorem count_face (κ : ℕ) : 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 * κ) := ⟨by ring, by ring, by ring⟩ /-- 21:C13 — the merger area law on the count face, `A = M(M + 1)`: `ΔA = 2M₁M₂` exactly under additive mass, the paper's instance `27 811 + 1 596 → 29 407` giving `ΔA = 88 772 712`; with a radiated `δ` the count gives `ΔA = 2M₁M₂ − (2(M₁ + M₂) + 1)δ + δ²`, at most the additive value for `0 ≤ δ ≤ 2(M₁ + M₂) + 1` — the area statement an inequality (the coefficient `−2(M₁ + M₂)δ` is the `A = M²` form; on the count face the linear term carries the extra `−δ`). -/ theorem merger_area_law (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 : ℤ) := by refine ⟨by ring, by ring, ?_, by norm_num⟩ intro h0 h1 nlinarith [mul_nonneg h0 (sub_nonneg.mpr h1)] /-- 21:A9, 21:C25, 21:C7, 21:C8 — the cover forcing: the apsidal coefficient `2 − β + 2γ` against the PPN-free deficit `3/2` equals the two-face ratio `2` exactly when `2γ − β = 1`, with deviation `(2/3)(2γ − β − 1)`; channel unity `γ = 1` makes the deflection factor `(1 + γ)/2` equal to `1` (the full `4Gm/c²b`) and, together with the forcing, gives `β = 1`, the perihelion factor `(2 + 2γ − β)/3` then `1`. -/ theorem cover_forcing (β γ : ℚ) : ((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)) := by refine ⟨?_, by ring, ?_⟩ · constructor <;> intro h <;> linarith · rintro rfl exact ⟨by norm_num, fun h => ⟨by linarith, by linarith⟩⟩ /-- 38:C8 — the face-ratio identity of the parametrised post-Newtonian family (Statement *The physical floors*, 38-s13): with the apsidal coefficient `2 − β + 2γ` and the `β, γ`-free clock-deficit coefficient `3/2`, the face ratio is `(2/3)(2 + 2γ − β)`, equal to `2` exactly when `2γ − β = 1`, with deviation `(2/3)(2γ − β − 1)`; the exponential metric `β = γ = 1` satisfies it; in Brans–Dicke theory (`β = 1`, `γ = (1 + ω)/(2 + ω)`) the combination is `2γ − β − 1 = −2/(2 + ω)`, nonzero at every finite coupling, deviation `−4/(3(2 + ω))`, and below every `ε` past `ω = 2/ε` (the general-relativistic limit, stated over `ℚ`). The coefficients themselves are the continuum chart's (the series of the isotropic metric, `o1_gr_chart.py`); the algebra is exact over `ℚ`. -/ theorem ppn_faces (β γ : ℚ) : (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 + ω)| < ε) := by refine ⟨by ring, ⟨fun h => by linarith, fun h => by linarith⟩, by ring, by norm_num, fun ω hω => ⟨?_, ?_, ?_⟩, ?_⟩ · field_simp; ring · field_simp; ring · exact div_ne_zero (by norm_num) hω · intro ε hε refine ⟨2 / ε, fun ω hω => ?_⟩ have h2 : 0 < 2 / ε := by positivity have hpos : 0 < 2 + ω := by linarith rw [abs_div, abs_neg, abs_of_pos hpos, abs_of_pos (by norm_num : (0 : ℚ) < 2), div_lt_iff₀ hpos] have : 2 / ε < ω := hω rw [div_lt_iff₀ hε] at this linarith /-- 38:C12, 38:C7 — the registration dictionary on a hosted pair: matching the temporal face `κ/(2S)` to the circular-orbit clock deficit `(3/2) r_g/p_sl` forces `p_sl = 3 (S/κ) r_g`, under which the angular face reads `3 r_g/p_sl = κ/S` automatically: one relation, homogeneous of degree `0`, fixing the ratio `p_sl/r_g = 3S/κ` — `58` at `(13, 233)` (`κ = 3`, `S = 58`: `p_sl = S r_g`), `174` at `(5, 233)`; the two faces `κ/S : κ/(2S) = 2`. -/ theorem registration_dictionary (κ S rg psl : ℚ) (hκ : κ ≠ 0) (hS : S ≠ 0) (hrg : rg ≠ 0) (hpsl : 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 := by refine ⟨⟨fun h => ?_, fun h => ?_⟩, fun h => ⟨?_, ?_⟩, ?_, by norm_num, by norm_num⟩ · field_simp at h ⊢; linarith · subst h; field_simp · subst h; field_simp · subst h; field_simp · field_simp /-- 21:A9 — the mass–energy channel `C_{p−1} ∩ C_{2(p+1)} = Q₄`: on every shell `p ≡ 1 (mod 4)`, `gcd(p − 1, 2(p + 1)) = 4`; the subgroup reading — in the cyclic unit group of `𝔽_{p²}` (order `(p − 1)(p + 1)`) the subgroups of orders `p − 1` and `2(p + 1)` meet in the subgroup of order `gcd` — is not formalised here. -/ theorem channel_q4 (p : ℕ) (hp : p % 4 = 1) : Nat.gcd (p - 1) (2 * (p + 1)) = 4 := by obtain ⟨κ, rfl⟩ : ∃ κ, p = 4 * κ + 1 := ⟨p / 4, by omega⟩ have h1 : 4 * κ + 1 - 1 = 4 * κ := by omega have h2 : 2 * (4 * κ + 1 + 1) = 4 * (1 + 2 * κ) := by ring rw [h1, h2, Nat.gcd_mul_left, Nat.gcd_add_mul_right_right, Nat.gcd_one_right] end count /-! ## The lattice on `ZMod N` (21:C9, C20) -/ section lattice variable {N : ℕ} [NeZero N] {R : Type*} [CommRing R] /-- 21:C9 — anti-self-adjointness of the central difference on the cycle `ℤ/N`: with `(Δf)(x) = f(x + 1) − f(x − 1)`, `Σ_x f(x)(Δg)(x) = −Σ_x (Δf)(x) g(x)` — `Δᵀ = −Δ`, the identity that carries the discrete Fierz–Pauli gauge invariance (the package proves the four-term functional's invariance as an exact integer identity; the paper's `½` in `D_μ = (T_μ − T_μ⁻¹)/2` scales both sides alike). The one-sided difference `(δf)(x) = f(x + 1) − f(x)` has adjoint the negative *backward* difference, `Σ_x f(x)(δg)(x) = −Σ_x (f(x) − f(x − 1)) g(x)` — the package's failing control is that this is not `−δ`. -/ theorem central_difference_adjoint (f g : ZMod N → R) : ∑ x, f x * (g (x + 1) - g (x - 1)) = -∑ x, (f (x + 1) - f (x - 1)) * g x ∧ ∑ x, f x * (g (x + 1) - g x) = -∑ x, (f x - f (x - 1)) * g x := by have h1 : ∑ x, f x * g (x + 1) = ∑ x, f (x - 1) * g x := by rw [← Equiv.sum_comp (Equiv.addRight (1 : ZMod N)) (fun x => f (x - 1) * g x)] simp have h2 : ∑ x, f x * g (x - 1) = ∑ x, f (x + 1) * g x := by rw [← Equiv.sum_comp (Equiv.subRight (1 : ZMod N)) (fun x => f (x + 1) * g x)] simp constructor · simp only [mul_sub, sub_mul, Finset.sum_sub_distrib, h1, h2]; ring · simp only [mul_sub, sub_mul, Finset.sum_sub_distrib, h1]; ring /-- The finite Fourier transform on the cycle, against a character `ζ` with `ζ^N = 1`: `(F f)(k) = Σ_x f(x) ζ^{xk}`. -/ def dft (ζ : R) (f : ZMod N → R) (k : ZMod N) : R := ∑ x, f x * ζ ^ (x.val * k.val) omit [NeZero N] in /-- A root of unity is insensitive to the reduction of its exponent modulo `N`. -/ theorem pow_val_mod (ζ : R) (hζ : ζ ^ N = 1) (m k : ℕ) : ζ ^ ((m % N) * k) = ζ ^ (m * k) := by conv_rhs => rw [← Nat.mod_add_div m N] rw [add_mul, pow_add, mul_assoc, pow_mul, pow_mul, hζ, one_pow, mul_one] omit [NeZero N] in /-- A root of unity is insensitive to the reduction of a factor of its exponent modulo `N`. -/ theorem pow_mul_val_mod (ζ : R) (hζ : ζ ^ N = 1) (k m : ℕ) : ζ ^ (k * (m % N)) = ζ ^ (k * m) := by rw [mul_comm, pow_val_mod ζ hζ, mul_comm] /-- 21:C20 — the finite Fourier shift theorem in both forms, the kick of the two-shift law: the kick, a character `ζ^{ax}` multiplying `f` in position, shifts the transform, `F(ζ^{a·} f)(k) = (F f)(k + a)`; dually, shifting `f` by `a` multiplies its transform by the character, `F(f(· − a))(k) = ζ^{ak} (F f)(k)`. -/ theorem shift_theorem (ζ : R) (hζ : ζ ^ N = 1) (f : ZMod N → R) (a k : ZMod N) : dft ζ (fun x => ζ ^ (a.val * x.val) * f x) k = dft ζ f (k + a) ∧ dft ζ (fun x => f (x - a)) k = ζ ^ (a.val * k.val) * dft ζ f k := by constructor · unfold dft apply Finset.sum_congr rfl intro x _ dsimp only rw [ZMod.val_add, pow_mul_val_mod ζ hζ, mul_add, pow_add, mul_comm a.val x.val] ring · unfold dft rw [Finset.mul_sum, ← Equiv.sum_comp (Equiv.addRight a)] apply Finset.sum_congr rfl intro x _ simp only [Equiv.coe_addRight, add_sub_cancel_right] rw [ZMod.val_add, pow_val_mod ζ hζ, add_mul, pow_add] ring end lattice end FRC.GravML /-! inlined: FrcLedger/Theme/Horizon.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Horizon — the horizon theme on Mathlib: the shell arithmetic of 20-rh (ledger migration, task LM36) The exact arithmetic of the shell theorem and its neighbours, proved for every shell: an arbitrary finite field `F` with `4κ + 1` elements and a primitive root `g`, or `ZMod p` where the prime is needed, and over any integral domain for the Ramanujan sum. The zero-slot and slot complementarity (20:B4, B5); the Ramanujan sum `c_p(n) = −1` off the origin (20:B7); the constants of the Subject register (20:B10); the quadratic extension `F(η)`, `η² = ν` a nonsquare, as Mathlib's `QuadraticAlgebra F ν 0`: the phase circle of order `p + 1`, Frobenius as conjugation and as inversion on the circle, the quarter-turn off the circle (20:B6); the critical line `Tr z = 1 ⟺ Re z = 2⁻¹` with `p` points and energy `¼ − νb²` (20:B8); the Klein four-group of Frobenius and the half-turn with its fixed loci (20:B9); the scale-shift on the power characters and its trace (20:E1, E12 (iii)), the power characters never orthonormal (20:E13); frame coincidence below the horizon (20:B2) and the laboratory pair `(13, 233)` (20:B1). The theorems moved here from 20-rh's `FrcLedger/Rh.lean` (7 October 2026), under the same names in the namespace `FRC.HorizonML`; that module keeps the old names as aliases. The complex characters of the cycle and the von Mangoldt weight use the reals and live in the chart theme (`Theme/Chart.lean`). Classical (tier 2) on Mathlib's hierarchy, with no reals: the exact Mathlib theme of gate G09. -/ namespace FRC.HorizonML open Finset /-! ## The shell: the zero-slot, slot complementarity and the Ramanujan sum (rows B4, B5, B7) -/ section shell variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] /-- 20:B4 — zero-slot, every shell: `Σ_{x ∈ F^×} x^k = 0` on every nonterminal exponent `1 ≤ k ≤ p − 2`, and `= −1` on the full cycle `k = p − 1`. -/ theorem zero_slot : (∀ k, 1 ≤ k → k ≤ Fintype.card F - 2 → ∑ x : Fˣ, ((x : F) ^ k) = 0) ∧ ∑ x : Fˣ, ((x : F) ^ (Fintype.card F - 1)) = -1 := by refine ⟨fun k hk1 hk2 => ?_, ?_⟩ · rw [FiniteField.sum_pow_units, ite_eq_right] intro hdvd have := Nat.le_of_dvd (by omega) hdvd omega · rw [FiniteField.sum_pow_units, ite_eq_left dvd_rfl] omit [DecidableEq F] in /-- 20:B5 — slot complementarity, every shell: `Φ(k) = −g^k` is injective on the nontrivial spectral slots `1 ≤ k ≤ p − 2` and maps them onto the nonterminal additive slots `F^× ∖ {−1}`. -/ theorem slot_complementarity (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) : Set.InjOn (fun k : ℕ => -(g ^ k)) (Set.Icc 1 (Fintype.card F - 2)) ∧ (fun k : ℕ => -(g ^ k)) '' Set.Icc 1 (Fintype.card F - 2) = {y : F | y ≠ 0 ∧ y ≠ -1} := by have h1 : 1 < Fintype.card F := Fintype.one_lt_card have : NeZero (Fintype.card F - 1) := ⟨by omega⟩ have hg0 : g ≠ 0 := by rintro rfl have := hg.pow_eq_one rw [zero_pow (by omega)] at this exact zero_ne_one this refine ⟨fun a ha b hb hab => ?_, ?_⟩ · simp only [Set.mem_Icc] at ha hb exact hg.pow_inj (by omega) (by omega) (neg_injective hab) · ext y simp only [Set.mem_image, Set.mem_Icc, Set.mem_ofPred_eq] constructor · rintro ⟨k, ⟨hk1, hk2⟩, rfl⟩ refine ⟨neg_ne_zero.2 (pow_ne_zero _ hg0), fun h => ?_⟩ have := neg_injective h exact hg.pow_ne_one_of_pos_of_lt (by omega) (by omega) this · rintro ⟨hy0, hy1⟩ have hpow : (-y) ^ (Fintype.card F - 1) = 1 := FiniteField.pow_card_sub_one_eq_one (-y) (neg_ne_zero.2 hy0) obtain ⟨i, hi, hiy⟩ := hg.eq_pow_of_pow_eq_one hpow have hi0 : i ≠ 0 := by rintro rfl rw [pow_zero] at hiy exact hy1 (by rw [← neg_neg y, ← hiy]) exact ⟨i, ⟨by omega, by omega⟩, by rw [hiy, neg_neg]⟩ end shell section ramanujan variable {R : Type*} [CommRing R] [IsDomain R] /-- 20:B7 — the flat ground state, in any integral domain with a primitive `p`-th root of unity `ω` (the cyclotomic ledger, `𝔽_q` with `q ≡ 1 (mod p)`, or `ℂ`): the full-modulus Ramanujan sum `c_p(n) = Σ_{a=1}^{p−1} ω^{an}` equals `−1` for every `n ≢ 0 (mod p)`, and `p − 1` at the origin; the mode at the spectral origin carries no prime information. -/ theorem ramanujan_sum {p : ℕ} (hp : 0 < p) {ω : R} (hω : IsPrimitiveRoot ω p) (n : ℕ) : (¬ p ∣ n → ∑ a ∈ Ico 1 p, ω ^ (a * n) = -1) ∧ (p ∣ n → ∑ a ∈ Ico 1 p, ω ^ (a * n) = ((p - 1 : ℕ) : R)) := by have hsplit : ∑ a ∈ range p, ω ^ (a * n) = 1 + ∑ a ∈ Ico 1 p, ω ^ (a * n) := by obtain ⟨m, rfl⟩ : ∃ m, p = m + 1 := ⟨p - 1, by omega⟩ rw [sum_range_succ', sum_Ico_eq_sum_range, Nat.add_sub_cancel, zero_mul, pow_zero, add_comm] congr 1 refine sum_congr rfl fun a _ => ?_ rw [add_comm 1 a] constructor · intro hn have hx1 : ω ^ n ≠ 1 := fun h => hn ((hω.pow_eq_one_iff_dvd n).1 h) have hxp : (ω ^ n) ^ p = 1 := by rw [← pow_mul, mul_comm, pow_mul, hω.pow_eq_one, one_pow] have hsum : ∑ a ∈ range p, ω ^ (a * n) = 0 := by have h := geom_sum_mul (ω ^ n) p rw [hxp, sub_self] at h have h' : ∑ a ∈ range p, ω ^ (a * n) = ∑ a ∈ range p, (ω ^ n) ^ a := sum_congr rfl fun a _ => by rw [← pow_mul, mul_comm] rw [h'] exact (mul_eq_zero.1 h).resolve_right (sub_ne_zero.2 hx1) rw [hsum] at hsplit exact (neg_eq_of_add_eq_zero_right hsplit.symm).symm · intro hn have hone : ∀ a, ω ^ (a * n) = 1 := fun a => by obtain ⟨c, rfl⟩ := hn rw [← mul_assoc, mul_comm a, mul_assoc, pow_mul, hω.pow_eq_one, one_pow] simp only [hone, sum_const, Nat.card_Ico, nsmul_eq_mul, mul_one] end ramanujan /-! ## The Subject register on the shell (rows B10, B8's arithmetic) -/ section constants variable {F : Type*} [Field F] [Fintype F] /-- `2 ≠ 0` on a shell of `4κ + 1` elements. -/ lemma two_ne_zero_of_card (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) : (2 : F) ≠ 0 := by intro h2 have hc : ((4 * κ + 1 : ℕ) : F) = 0 := by rw [← hκ]; exact FiniteField.cast_card_eq_zero F have : ((4 * κ + 1 : ℕ) : F) = 2 * (2 * κ) + 1 := by push_cast; ring rw [this, h2, zero_mul, zero_add] at hc exact one_ne_zero hc /-- 20:B8, 20:B10 — the half-turn arithmetic on every shell of `4κ + 1` elements: `2π ≡ −1` with `π = 2κ`, and `2⁻¹ = 2κ + 1 = −π`. -/ theorem half_turn (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) : (2 : F) * ((2 * κ : ℕ) : F) = -1 ∧ (2 : F) * ((2 * κ + 1 : ℕ) : F) = 1 ∧ ((2 * κ + 1 : ℕ) : F) = -((2 * κ : ℕ) : F) ∧ (2 : F)⁻¹ = ((2 * κ + 1 : ℕ) : F) := by have hc : ((4 * κ + 1 : ℕ) : F) = 0 := by rw [← hκ]; exact FiniteField.cast_card_eq_zero F have h2 : (2 : F) ≠ 0 := two_ne_zero_of_card κ hκ have e1 : (2 : F) * ((2 * κ : ℕ) : F) = -1 := by have : ((4 * κ + 1 : ℕ) : F) = 2 * ((2 * κ : ℕ) : F) + 1 := by push_cast; ring rw [this] at hc exact eq_neg_of_add_eq_zero_left hc have e2 : (2 : F) * ((2 * κ + 1 : ℕ) : F) = 1 := by push_cast at e1 ⊢ linear_combination e1 refine ⟨e1, e2, ?_, ?_⟩ · push_cast at e1 e2 ⊢ have : (2 : F) * (2 * (κ : F) + 1 + 2 * (κ : F)) = 0 := by linear_combination e2 + e1 have := (mul_eq_zero.1 this).resolve_left h2 exact eq_neg_of_add_eq_zero_left this · exact (eq_inv_of_mul_eq_one_right e2).symm /-- The half-period `g^{2κ} = −1` for a primitive root of a shell with `4κ + 1` elements. -/ lemma half_period (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) : g ^ (2 * κ) = -1 := by have hκ' : Fintype.card F - 1 = 4 * κ := by omega have hκpos : κ ≠ 0 := by intro h; subst h; have := Fintype.one_lt_card (α := F); omega have h2 : IsPrimitiveRoot (g ^ (2 * κ)) 2 := by rw [hκ'] at hg exact hg.pow (by omega) (show 4 * κ = 2 * κ * 2 by ring) exact h2.eq_neg_one_of_two_right /-- 20:B10 — the Subject constants on every shell: `π = 2κ` with `2π = −1`; the quarter-turn `i = g^{−κ}` (read as `g^{3κ}`, since `g^{4κ} = 1`) equals `−g^κ` and squares to `−1`; `g^π = −1`; and the Euler identity `e^{iπ} = (g^m)^{m·π} = −1` for every odd `m` — the convention "`e = g^m` on the odd representative `m` of `i`" fixes the parity of the exponent, and the identity uses nothing else about `m`. -/ theorem subject_constants (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) : (2 : F) * ((2 * κ : ℕ) : F) = -1 ∧ g ^ (3 * κ) = -(g ^ κ) ∧ (g ^ (3 * κ)) ^ 2 = -1 ∧ g ^ (2 * κ) = -1 ∧ ∀ m : ℕ, m % 2 = 1 → (g ^ m) ^ (m * (2 * κ)) = -1 := by have hhp := half_period κ hκ g hg have hi : g ^ (3 * κ) = -(g ^ κ) := by rw [show 3 * κ = κ + 2 * κ by ring, pow_add, hhp, mul_neg, mul_one] refine ⟨(half_turn κ hκ).1, hi, ?_, hhp, fun m hm => ?_⟩ · rw [hi, neg_sq, ← pow_mul, show κ * 2 = 2 * κ by ring, hhp] · rw [← pow_mul, show m * (m * (2 * κ)) = 2 * κ * (m * m) by ring, pow_mul, hhp] have hodd : Odd (m * m) := by have := Nat.odd_iff.2 hm exact this.mul this exact hodd.neg_one_pow /-- 20:B10 [value] — on `𝔽₁₃(τ; 0, 1, 2)`: `κ = 3`, `π = 6`, `2π = −1`, `i = 2^{−3} = 2^9 = 5`, `i² = −1`, `e = 2^5 = 6` on the odd representative `5`, `2^π = −1`, `e^{iπ} = 6^{30} = −1`. -/ theorem constants13 : (2 : ZMod 13) * 6 = -1 ∧ (2 : ZMod 13) ^ 9 = 5 ∧ (5 : ZMod 13) ^ 2 = -1 ∧ (2 : ZMod 13) ^ 5 = 6 ∧ (2 : ZMod 13) ^ 6 = -1 ∧ (6 : ZMod 13) ^ (5 * 6) = -1 := by decide end constants /-! ## The quadratic extension: the phase circle, the critical line, the two loci of agreement (rows B6, B8, B9) -/ section extension variable {F : Type*} [Field F] (ν : F) local notation "K" => QuadraticAlgebra F ν 0 /-- The trace of `a + bη` is `2a`. -/ lemma trace_eq (z : K) : QuadraticAlgebra.trace z = 2 * z.re := by rw [QuadraticAlgebra.trace_def, zero_mul, add_zero] /-- The norm of `a + bη` is `a² − νb²`. -/ lemma norm_eq (z : K) : QuadraticAlgebra.norm z = z.re * z.re - ν * z.im * z.im := by rw [QuadraticAlgebra.norm_def, zero_mul, zero_mul, add_zero] /-- The conjugate of `a + bη` is `a − bη`. -/ lemma star_eq (z : K) : star z = ⟨z.re, -z.im⟩ := by ext <;> simp [QuadraticAlgebra.re_star, QuadraticAlgebra.im_star] /-- 20:B9 — Frobenius `φ = star` and the functional-equation half-turn `ρ : z ↦ 1 − z` generate a Klein four-group: both are involutions and they commute. -/ theorem klein_four (z : K) : star (star z) = z ∧ (1 - (1 - z)) = z ∧ star (1 - z) = 1 - star z := by refine ⟨star_star z, sub_sub_cancel 1 z, ?_⟩ rw [star_sub, star_one] /-- 20:B9 — the fixed locus of Frobenius is the prime meridian `F` (the elements with `b = 0`). -/ theorem fixed_frobenius (h2 : (2 : F) ≠ 0) (z : K) : star z = z ↔ z.im = 0 := by rw [star_eq] constructor · intro h have := congrArg QuadraticAlgebra.im h simp only at this have h' : (2 : F) * z.im = 0 := by linear_combination -this exact (mul_eq_zero.1 h').resolve_left h2 · intro h ext <;> simp [h] /-- 20:B8, 20:B9 — the finite critical line: `Tr z = 1` exactly when `Re z = 2⁻¹`; this locus is the fixed locus of `σ = ρ ∘ φ : z ↦ 1 − z̄`. -/ theorem trace_eq_one_iff (h2 : (2 : F) ≠ 0) (z : K) : (QuadraticAlgebra.trace z = 1 ↔ z.re = 2⁻¹) ∧ (1 - star z = z ↔ z.re = 2⁻¹) := by have key : (2 : F) * z.re = 1 ↔ z.re = 2⁻¹ := by constructor · intro h; exact eq_inv_of_mul_eq_one_right h · intro h; rw [h, mul_inv_cancel₀ h2] refine ⟨by rw [trace_eq]; exact key, ?_⟩ rw [star_eq] constructor · intro h have := congrArg QuadraticAlgebra.re h simp only [QuadraticAlgebra.re_sub, QuadraticAlgebra.re_one] at this exact key.1 (by linear_combination -this) · intro h ext · simp only [QuadraticAlgebra.re_sub, QuadraticAlgebra.re_one] have := key.2 h linear_combination -this · simp only [QuadraticAlgebra.im_sub, QuadraticAlgebra.im_one, zero_sub, neg_neg] /-- 20:B9 — the fixed locus of the half-turn `ρ` is the single point `2⁻¹`, the meeting of the prime meridian and the critical line. -/ theorem fixed_half_turn (h2 : (2 : F) ≠ 0) (z : K) : (1 - z = z ↔ z = ⟨2⁻¹, 0⟩) ∧ (z.im = 0 ∧ z.re = 2⁻¹ ↔ z = ⟨2⁻¹, 0⟩) := by have hinv : (2 : F) * 2⁻¹ = 1 := mul_inv_cancel₀ h2 constructor · constructor · intro h have hre := congrArg QuadraticAlgebra.re h have him := congrArg QuadraticAlgebra.im h simp only [QuadraticAlgebra.re_sub, QuadraticAlgebra.re_one, QuadraticAlgebra.im_sub, QuadraticAlgebra.im_one, zero_sub] at hre him have h2re : (2 : F) * z.re = 1 := by linear_combination -hre have h2im : (2 : F) * z.im = 0 := by linear_combination -him ext · exact eq_inv_of_mul_eq_one_right h2re · exact (mul_eq_zero.1 h2im).resolve_left h2 · rintro rfl ext · simp only [QuadraticAlgebra.re_sub, QuadraticAlgebra.re_one] linear_combination -hinv · simp only [QuadraticAlgebra.im_sub, QuadraticAlgebra.im_one, sub_zero] · constructor · rintro ⟨him, hre⟩; ext · exact hre · exact him · rintro rfl; exact ⟨rfl, rfl⟩ /-- 20:B8 — on the critical line the energy is `N(z) = ¼ − νb²`. -/ theorem norm_on_line (z : K) (hz : z.re = 2⁻¹) : QuadraticAlgebra.norm z = (4 : F)⁻¹ - ν * z.im ^ 2 := by rw [norm_eq, hz, sq, mul_assoc] congr 1 rw [show (4 : F) = 2 * 2 by norm_num, mul_inv] /-- 20:E12, 20:B8 — the spectral readout: the mode index `θ ∈ F` is read at the point `z(θ) = 2⁻¹ + θη` of the quadratic extension. -/ def readout (θ : F) : K := ⟨2⁻¹, θ⟩ /-- 20:E12, 20:B8 — clause (ii) of the shell theorem: every readout `z(θ) = 2⁻¹ + θη` lies on the trace-one line, its real part is the half-turn `2⁻¹`, and `θ ↦ z(θ)` is injective (with `card_critical_line`, a bijection of `F` onto the line). -/ theorem readout_on_line (h2 : (2 : F) ≠ 0) (θ : F) : QuadraticAlgebra.trace (readout ν θ) = 1 ∧ (readout ν θ).re = 2⁻¹ ∧ Function.Injective (readout ν) := by refine ⟨?_, rfl, fun a b h => by simpa [readout] using congrArg QuadraticAlgebra.im h⟩ rw [trace_eq] exact mul_inv_cancel₀ h2 variable [Fintype F] [DecidableEq F] /-- The extension as a finite type, through its coordinates. -/ noncomputable instance instFintypeK : Fintype K := Fintype.ofEquiv (F × F) (QuadraticAlgebra.equivProd ν 0).symm /-- 20:B8 — the critical line carries exactly `p` points: `z = 2⁻¹ + bη`, one for each `b ∈ F`. -/ theorem card_critical_line (h2 : (2 : F) ≠ 0) : (univ.filter (fun z : K => QuadraticAlgebra.trace z = 1)).card = Fintype.card F := by have hline : univ.filter (fun z : K => QuadraticAlgebra.trace z = 1) = univ.image (fun b : F => (⟨2⁻¹, b⟩ : K)) := by ext z simp only [mem_filter, mem_univ, true_and, mem_image] rw [(trace_eq_one_iff ν h2 z).1] constructor · intro h; exact ⟨z.im, by ext <;> simp [h]⟩ · rintro ⟨b, rfl⟩; rfl rw [hline, card_image_of_injective _ (fun a b h => by simpa using congrArg QuadraticAlgebra.im h), card_univ] omit [DecidableEq F] in /-- 20:E12 — the slot index of a nontrivial slot: for `1 ≤ k ≤ p − 2` the index `θ = Φ(k) = −g^k` at which slot `k` is read is neither `0` (the centre `2⁻¹`) nor `−1` (the full-cycle exponent). -/ theorem readout_slot_index (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (k : ℕ) (hk1 : 1 ≤ k) (hk2 : k ≤ Fintype.card F - 2) : -(g ^ k) ≠ 0 ∧ -(g ^ k) ≠ -1 := by have hcard : 1 < Fintype.card F := Fintype.one_lt_card have hg0 : g ≠ 0 := hg.ne_zero (by omega) refine ⟨fun h => pow_ne_zero k hg0 (neg_eq_zero.1 h), fun h => ?_⟩ have h1 : g ^ k = 1 := neg_inj.1 h have hdvd := (hg.pow_eq_one_iff_dvd k).1 h1 have := Nat.le_of_dvd (by omega) hdvd omega end extension section frobenius variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] {p : ℕ} [hp : Fact p.Prime] [CharP F p] (hcard : Fintype.card F = p) (ν : F) [hν : Fact (¬ IsSquare ν)] local notation "K" => QuadraticAlgebra F ν 0 omit [DecidableEq F] in include hcard hν in /-- On a shell carrying a nonsquare, `2 ≠ 0` (every element of `𝔽₂` is a square). -/ lemma two_ne_zero_of_nonsquare : (2 : F) ≠ 0 := by intro h2 have hp2 : p = 2 := (Nat.prime_dvd_prime_iff_eq hp.out Nat.prime_two).1 ((CharP.cast_eq_zero_iff F p 2).1 (by exact_mod_cast h2)) -- every element of a two-element field is a square: `x^2 = x` apply hν.out refine ⟨ν, ?_⟩ have := FiniteField.pow_card ν rw [hcard, hp2, sq] at this exact this.symm omit [DecidableEq F] in include hcard hν in /-- Euler's criterion for the nonsquare `ν`: `ν^{(p−1)/2} = −1`. -/ lemma nonsquare_pow : ν ^ (p / 2) = -1 := by have h2 : (2 : F) ≠ 0 := two_ne_zero_of_nonsquare hcard ν have hp2 : p ≠ 2 := by intro h; apply h2 have := (CharP.cast_eq_zero_iff F p p).2 dvd_rfl rw [h] at this; exact_mod_cast this have hchar : ringChar F ≠ 2 := by rw [ringChar.eq F p]; exact hp2 have hν0 : ν ≠ 0 := by rintro rfl; exact hν.out ⟨0, by simp⟩ rcases FiniteField.pow_dichotomy hchar hν0 with h | h · exact absurd ((FiniteField.isSquare_iff hchar hν0).2 h) hν.out · rwa [hcard] at h omit [DecidableEq F] in include hcard in /-- 20:B6 — Frobenius on the extension is conjugation: `z^p = z̄` for every `z ∈ F(η)`. -/ theorem frobenius_eq_star (z : K) : z ^ p = star z := by have : CharP K p := charP_of_injective_algebraMap (algebraMap F K).injective p have hodd : p = 2 * (p / 2) + 1 := by have := hp.out.eq_two_or_odd' rcases this with h | h · exfalso have h2 : (2 : F) ≠ 0 := two_ne_zero_of_nonsquare hcard ν apply h2 have := (CharP.cast_eq_zero_iff F p p).2 dvd_rfl rw [h] at this; exact_mod_cast this · exact (Nat.two_mul_div_two_add_one_of_odd h).symm have hω : (QuadraticAlgebra.omega : K) ^ p = -QuadraticAlgebra.omega := by rw [hodd, pow_succ, pow_mul, QuadraticAlgebra.omega_pow_two_eq_add] simp only [zero_smul, add_zero] rw [← Algebra.algebraMap_eq_smul_one, ← map_pow, nonsquare_pow hcard ν, map_neg, map_one, neg_one_mul] have hz : z = algebraMap F K z.re + z.im • QuadraticAlgebra.omega := by rw [Algebra.algebraMap_eq_smul_one]; exact (QuadraticAlgebra.re_smul_add_im_smul z).symm have hre : z.re ^ p = z.re := by rw [← hcard]; exact FiniteField.pow_card z.re have him : z.im ^ p = z.im := by rw [← hcard]; exact FiniteField.pow_card z.im conv_lhs => rw [hz] rw [add_pow_char, ← map_pow, hre, smul_pow, him, hω, star_eq] ext · simp [QuadraticAlgebra.algebraMap_eq, QuadraticAlgebra.re_omega] · simp [QuadraticAlgebra.algebraMap_eq, QuadraticAlgebra.im_omega] omit [DecidableEq F] in include hcard in /-- 20:B6 — the norm is the `(p+1)`-st power: `z^{p+1} = z z̄ = N(z)` in the extension. -/ theorem norm_eq_pow (z : K) : algebraMap F K (QuadraticAlgebra.norm z) = z ^ (p + 1) := by rw [pow_succ, frobenius_eq_star hcard ν z, QuadraticAlgebra.algebraMap_norm_eq_mul_star, mul_comm] include hcard in /-- 20:B6 — the phase circle `U_{p+1} = {z : N(z) = 1}` has exactly `p + 1` elements, and Frobenius is inversion on it: `z̄ = z⁻¹` for `N(z) = 1`. -/ theorem phase_circle : (univ.filter (fun z : K => QuadraticAlgebra.norm z = 1)).card = p + 1 ∧ ∀ z : K, QuadraticAlgebra.norm z = 1 → star z = z⁻¹ := by constructor · -- the circle is the set of `(p+1)`-st roots of unity, counted by a primitive root have hcardK : Fintype.card K = p ^ 2 := by rw [Fintype.card_congr (QuadraticAlgebra.equivProd ν 0), Fintype.card_prod, hcard, sq] have hset : univ.filter (fun z : K => QuadraticAlgebra.norm z = 1) = Polynomial.nthRootsFinset (p + 1) (1 : K) := by ext z rw [mem_filter, Polynomial.mem_nthRootsFinset (by omega), ← norm_eq_pow hcard ν] constructor · rintro ⟨-, h⟩; rw [h, map_one] · intro h; exact ⟨mem_univ _, QuadraticAlgebra.algebraMap_injective (by rw [h, map_one])⟩ rw [hset] -- a primitive `(p+1)`-st root of unity in `K` obtain ⟨ζ, hζ⟩ := IsCyclic.exists_generator (α := Kˣ) have hord : orderOf ζ = p ^ 2 - 1 := by rw [orderOf_eq_card_of_forall_mem_zpowers hζ, Nat.card_eq_fintype_card, Fintype.card_units, hcardK] have hprim : IsPrimitiveRoot ζ (p ^ 2 - 1) := hord ▸ IsPrimitiveRoot.orderOf ζ have hp1 : p ^ 2 - 1 = (p - 1) * (p + 1) := by obtain ⟨q, hq⟩ : ∃ q, p = q + 1 := ⟨p - 1, by have := hp.out.one_lt; omega⟩ rw [hq, Nat.add_sub_cancel] apply Nat.sub_eq_of_eq_add ring have hpos : 0 < p ^ 2 - 1 := by have := hp.out.one_lt; rw [hp1]; exact Nat.mul_pos (by omega) (by omega) have hprim' : IsPrimitiveRoot ((ζ : K) ^ (p - 1)) (p + 1) := by rw [← Units.val_pow_eq_pow_val, IsPrimitiveRoot.coe_units_iff] exact hprim.pow hpos hp1 exact hprim'.card_nthRootsFinset · intro z hz have h := QuadraticAlgebra.algebraMap_norm_eq_mul_star z rw [hz, map_one] at h exact eq_inv_of_mul_eq_one_right h.symm omit [DecidableEq F] in include hcard in /-- 20:B6 — the quarter-turn `i ∈ F` (`i² = −1`) is Frobenius-fixed and off the circle: `N(i) = −1 ≠ 1`. -/ theorem quarter_turn_off_circle (i : F) (hi : i ^ 2 = -1) : star (algebraMap F K i) = algebraMap F K i ∧ QuadraticAlgebra.norm (algebraMap F K i) = -1 ∧ QuadraticAlgebra.norm (algebraMap F K i) ≠ 1 := by have h2 : (2 : F) ≠ 0 := two_ne_zero_of_nonsquare hcard ν have hn : QuadraticAlgebra.norm (algebraMap F K i) = -1 := by rw [QuadraticAlgebra.norm_algebraMap, hi] refine ⟨?_, hn, ?_⟩ · rw [star_eq, QuadraticAlgebra.algebraMap_eq]; simp · rw [hn]; intro h apply h2 linear_combination -h end frobenius /-! ## The scale-shift on the shell: the `𝔽_p` reading (rows E1, E12(iii), E13) -/ section spectrum variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] /-- 20:E1, 20:E12 — the scale-shift `S : x ↦ g^r x` is a permutation of `F^×` (a bijection, so its matrix on `ℓ²(F^×)` is a permutation matrix, hence unitary) with the power characters `x ↦ x^k` as eigenvectors in the `𝔽_p` reading, `S x^k = g^{rk} x^k`, and its fixed-point count — the trace of its permutation matrix — is `(p − 1)·[(p − 1) ∣ r]`, which carries no prime data. -/ theorem scale_shift (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (r : ℕ) : Function.Bijective (fun x : Fˣ => (Units.mk0 g (hg.ne_zero (by have := Fintype.one_lt_card (α := F); omega))) ^ r * x) ∧ (∀ (k : ℕ) (x : F), (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k) ∧ (univ.filter (fun x : Fˣ => g ^ r * (x : F) = x)).card = if (Fintype.card F - 1) ∣ r then Fintype.card F - 1 else 0 := by refine ⟨(Group.mulLeft_bijective _), fun k x => mul_pow _ _ _, ?_⟩ split_ifs with hdvd · have h1 : g ^ r = 1 := (hg.pow_eq_one_iff_dvd r).2 hdvd have : univ.filter (fun x : Fˣ => g ^ r * (x : F) = x) = univ := by ext x; simp [h1] rw [this, card_univ, Fintype.card_units] · have h1 : g ^ r ≠ 1 := fun h => hdvd ((hg.pow_eq_one_iff_dvd r).1 h) have : univ.filter (fun x : Fˣ => g ^ r * (x : F) = x) = ∅ := by rw [Finset.filter_eq_empty_iff] intro x _ h apply h1 have hx : (x : F) ≠ 0 := x.ne_zero calc g ^ r = g ^ r * (x : F) * (x : F)⁻¹ := by rw [mul_assoc, mul_inv_cancel₀ hx, mul_one] _ = 1 := by rw [h, mul_inv_cancel₀ hx] rw [this, card_empty] /-- 20:E12, 20:E13 — the `𝔽_p`-valued power characters are never orthonormal: the self-pairing `Σ_{x ∈ F^×} x^j · x^j` is `0` or `−1`, never `1`, on every odd shell. -/ theorem power_characters_not_orthonormal (h2 : (2 : F) ≠ 0) (j : ℕ) : ∑ x : Fˣ, ((x : F) ^ j * (x : F) ^ j) ≠ 1 := by have : ∑ x : Fˣ, ((x : F) ^ j * (x : F) ^ j) = ∑ x : Fˣ, ((x : F) ^ (2 * j)) := sum_congr rfl fun x _ => by rw [← pow_add, two_mul] rw [this, FiniteField.sum_pow_units] split_ifs · intro h; apply h2; linear_combination -h · exact zero_ne_one end spectrum /-! ## Frame coincidence below the horizon (row B2) -/ section coincidence /-- 20:B2 — below the horizon the reading is frame-exact: on any shell `ZMod q` with `H² < q`, residues `n ≤ H` are the integers themselves and window products read back exactly, so the Subject `𝔽_p` and the Carrier `𝔽_Ω` agree on the window. -/ theorem window_readback {q : ℕ} [NeZero q] {H : ℕ} (hH : H * H < q) : (∀ m, m ≤ H → ((m : ZMod q)).val = m) ∧ ∀ a b, a ≤ H → b ≤ H → ((a : ZMod q) * b).val = a * b := by have hle : ∀ m, m ≤ H → m < q := fun m hm => by rcases Nat.eq_zero_or_pos H with h | h · subst h; have := Nat.pos_of_ne_zero (NeZero.ne q); omega · exact lt_of_le_of_lt (le_trans hm (Nat.le_mul_self H)) hH refine ⟨fun m hm => ZMod.val_natCast_of_lt (hle m hm), fun a b ha hb => ?_⟩ rw [← Nat.cast_mul, ZMod.val_natCast_of_lt] exact lt_of_le_of_lt (Nat.mul_le_mul ha hb) hH /-- 20:B2 — primality equals irreducibility in the window: for `2 ≤ m ≤ H` and any shell with `H² < q`, `m` is prime iff it admits no factorisation `a · b = m` with `2 ≤ a, b ≤ H` read on the shell. -/ theorem prime_iff_window_irreducible {q : ℕ} [NeZero q] {H : ℕ} (hH : H * H < q) (m : ℕ) (hm2 : 2 ≤ m) (hmH : m ≤ H) : Nat.Prime m ↔ ¬ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (a : ZMod q) * b = m := by have hrb := window_readback (q := q) hH constructor · rintro hp ⟨a, b, ha2, hb2, haH, hbH, hab⟩ have hval := congrArg ZMod.val hab rw [hrb.2 a b haH hbH, hrb.1 m hmH] at hval have hdvd : a ∣ m := ⟨b, hval.symm⟩ rcases (Nat.dvd_prime hp).1 hdvd with h | h · omega · rw [h] at hval have hb1 : b = 1 := Nat.eq_of_mul_eq_mul_left (show 0 < m by omega) (show m * b = m * 1 by rw [Nat.mul_one]; exact hval) omega · intro h rw [Nat.prime_def] refine ⟨hm2, fun a ham => ?_⟩ by_contra hane push Not at hane obtain ⟨b, hb⟩ := ham have hb0 : b ≠ 0 := by rintro rfl; rw [Nat.mul_zero] at hb; omega have hb1 : b ≠ 1 := by rintro rfl; rw [Nat.mul_one] at hb; exact hane.2 hb.symm have ha0 : a ≠ 0 := by rintro rfl; rw [Nat.zero_mul] at hb; omega apply h refine ⟨a, b, by omega, by omega, le_trans (Nat.le_of_dvd (by omega) ⟨b, hb⟩) hmH, le_trans (Nat.le_of_dvd (by omega) ⟨a, by rw [mul_comm]; exact hb⟩) hmH, ?_⟩ rw [← Nat.cast_mul, ← hb] /-- 20:B2 — `⌊√p⌋² < p` for a prime `p`: the horizon window `H = ⌊√p⌋` is wrap-free. -/ lemma sqrt_sq_lt_prime {p : ℕ} (hp : p.Prime) : Nat.sqrt p * Nat.sqrt p < p := by rcases lt_or_eq_of_le (Nat.sqrt_le p) with h | h · exact h · exfalso have hdvd : Nat.sqrt p ∣ p := ⟨Nat.sqrt p, h.symm⟩ rcases (Nat.dvd_prime hp).1 hdvd with h1 | h1 · rw [h1] at h; have := hp.one_lt; omega · rw [h1] at h have := hp.one_lt nlinarith end coincidence /-! ## The laboratory pair (13, 233) (row B1) -/ section lab /-- 20:B1 [value] — the laboratory pair `(13, 233)`: nested, `13² < 233`; the two cycles share the quarter-turn core `Q₄` and nothing else, `gcd(12, 232) = 4`, with `5² = −1` on `𝔽₁₃` and `89² = −1` on `𝔽₂₃₃`; and `12 ∤ 232`. -/ theorem lab_pair : 13 * 13 < 233 ∧ Nat.gcd 12 232 = 4 ∧ (5 : ZMod 13) ^ 2 = -1 ∧ (89 : ZMod 233) ^ 2 = -1 ∧ ¬ 12 ∣ 232 := by decide /-- 20:B1 — no projection of the Carrier's cycle onto the Subject's: there is no surjective homomorphism `C_{232} → C_{12}`, since `12 ∤ 232`. -/ theorem no_cycle_projection : ¬ ∃ f : Multiplicative (ZMod 232) →* Multiplicative (ZMod 12), Function.Surjective f := by rintro ⟨f, hf⟩ have := Subgroup.card_dvd_of_surjective f hf rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card] at this simp only [Fintype.card_multiplicative, ZMod.card] at this exact absurd this (by decide) end lab end FRC.HorizonML /-! inlined: FrcLedger/Keys/Chart.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Keys.Chart — the keyed theorems of the chart theme (ledger migration, task LM19) One declaration per key, `FRC.LedgerML.p`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration `FRC..p` as an alias. Every declaration has the axioms of Mathlib's hierarchy at most (`check_axioms.py`). -/ namespace FRC.LedgerML -- Keys of the chart theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file) /-- 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. -/ theorem 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 := @FRC.Chart.scale_import /-- 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. -/ theorem 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 : ℝ) := @FRC.Chart.running_floor /-- 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$. -/ theorem 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 Ω := And.intro @FRC.Chart.tilt_ledger (@FRC.Chart.efold_count) /-- 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. -/ theorem 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 := And.intro @FRC.Chart.floor_value (@FRC.Chart.floor_fine) /-- 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. -/ theorem 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 := 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))))))) /-- 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$). -/ theorem 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 := And.intro @FRC.Chart.age_rate_locus (@FRC.Chart.locus_bracket) /-- p20020 — 20:C2. Resonance and the von Mangoldt weight: $R_L\to\frac{\varphi(n)}{n}\Lambda(n)$ (Hardy, A6); $\Lambda=\mu\ast\log$ exactly on the divisor lattice; the intertwiner $\Lambda=\frac{n}{\varphi(n)}R$; support the prime powers in every form. -/ theorem p20020 : ∀ (m : ℕ), ArithmeticFunction.vonMangoldt m = ∑ d ∈ m.divisors, ↑(ArithmeticFunction.moebius d) * Real.log (↑m / ↑d) ∧ (ArithmeticFunction.vonMangoldt m ≠ (0 : ℝ) ↔ IsPrimePow m) := @FRC.Chart.vonMangoldt_moebius /-- p20023 — 20:C5. Mean-square flatness: with $r_j$ the normalised correlation of the mean-removed prime indicator with the nonconstant chart mode $\chi_j$, $\sum_{j\ne0}r_j^{2}=1$ exactly (Parseval), so the root-mean-square correlation is $1/\sqrt{\p-2}$. -/ theorem p20023 : (∀ {n : ℕ} [NeZero n] (v : ZMod n → ℂ), ∑ j, Complex.normSq (FRC.Chart.coef v j) = ↑n * ∑ m, Complex.normSq (v m)) ∧ ∀ {n : ℕ} [NeZero n] (u : ZMod n → ℂ), ∑ m, u m = (0 : ℂ) → u ≠ (0 : ZMod n → ℂ) → ∑ j ∈ Finset.univ.erase (0 : ZMod n), Complex.normSq (FRC.Chart.coef u j) / (↑n * ∑ m, Complex.normSq (u m)) = (1 : ℝ) ∧ (∑ j ∈ Finset.univ.erase (0 : ZMod n), Complex.normSq (FRC.Chart.coef u j) / (↑n * ∑ m, Complex.normSq (u m))) / (↑n - (1 : ℝ)) = (1 : ℝ) / (↑n - (1 : ℝ)) := And.intro @FRC.Chart.chi_parseval (@FRC.Chart.flatness) set_option linter.defProp false in /-- 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. -/ def p20032 := And.intro @FRC.HorizonML.scale_shift (And.intro @FRC.Chart.character_eigen (@FRC.Chart.chi_shift)) set_option linter.defProp false in /-- 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. -/ def 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)))) set_option linter.defProp false in /-- 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. -/ def 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))) set_option linter.defProp false in /-- 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. -/ def p20080 := @FRC.Chart.zeros_in_strip set_option linter.defProp false in /-- 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$. -/ def p21016 := @FRC.Strong.locked_sum /-- 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. -/ theorem p21019 : ∀ (u : ℝ), (0 : ℝ) ≤ u → u ≤ (1 : ℝ) → |(1 : ℝ) - Real.exp (-u) - u| ≤ u ^ (2 : ℕ) := @FRC.Strong.redshift_linear /-- p21020 — 21:C5. The magnitude $G=\hbar c/m_P^2$, frame-covariant (a relativity principle for scale); gravity's weakness is cardinality dilution. -/ theorem 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 : ℕ) / Ω := And.intro @FRC.GravML.hbar_register (@FRC.Strong.dilution) /-- p21022 — 21:C7. Channel unity forces the spatial bias to equal the temporal one, $\gamma=1$, restoring the full light deflection $4Gm/c^2b$. -/ theorem 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 : ℕ) := And.intro @FRC.GravML.cover_forcing (@FRC.Strong.pn_series) /-- p21023 — 21:C8. The exponential isotropic metric by multiplicative composition, with $\beta=\gamma=1$: deflection, Shapiro delay, and perihelion at their observed values. -/ theorem 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 : ℕ) := And.intro @FRC.GravML.cover_forcing (@FRC.Strong.pn_series) /-- 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. -/ theorem 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 : ℕ) := @FRC.Strong.exponential_reading /-- 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_*(\ln\Omega/2)^{2}$ Planck masses (master E10). -/ theorem 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) := @FRC.Strong.operational_cut /-- 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. -/ theorem p21030 : ∀ (k : ℝ), (2 : ℝ) - (2 : ℝ) * Real.cos k = (4 : ℝ) * Real.sin (k / (2 : ℝ)) ^ (2 : ℕ) := @FRC.Strong.dispersion_symbol /-- 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. -/ theorem 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 := And.intro @FRC.Strong.scale_invariance_iff (@FRC.Chart.tilt_ledger) /-- 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$. -/ theorem p21042 : Filter.Tendsto (fun t => t / ((1 : ℝ) - Real.exp (-t))) (nhdsWithin (0 : ℝ) (Set.Ioi (0 : ℝ))) (nhds (1 : ℝ)) := @FRC.Strong.crossover_deep_limit /-- p21048 — 21:X8. \textbf{The weakness of gravity} is cardinality dilution, not a hierarchy to be tuned. -/ theorem p21048 : ∀ (m Ω : ℝ), (0 : ℝ) < Ω → (m / √Ω) ^ (2 : ℕ) = m ^ (2 : ℕ) / Ω := @FRC.Strong.dilution /-- p21049 — 21:P1. Strong-field signatures at or outside the photon sphere: shadow $+4.6\%$, ringdown $-4.4\%$, 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. -/ theorem 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 := And.intro @FRC.Strong.photon_sphere (And.intro @FRC.Strong.shadow_bracket (And.intro @FRC.Strong.isco (@FRC.Strong.isco_efficiency))) /-- 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. -/ theorem 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) := @FRC.Strong.operational_cut /-- 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. -/ theorem p21051 : 27e-63 < (1 : ℝ) / √13e122 ∧ (1 : ℝ) / √13e122 < 28e-63 := @FRC.Strong.preferred_frame_scale /-- 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. -/ theorem 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 := @FRC.Chart.floor_value /-- 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$. -/ theorem 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 := And.intro @FRC.Strong.crossover_limits (And.intro @FRC.Strong.crossover_newton_limit (And.intro @FRC.Strong.registration_root (@FRC.Strong.interpolant_discriminant))) /-- 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. -/ theorem 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 : ℝ) := @FRC.Chart.running_floor /-- 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. -/ theorem 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 : ℕ) := @FRC.Strong.pn_series /-- 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$. -/ theorem 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 := @FRC.Chart.tilt_ledger /-- 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. -/ theorem 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 := And.intro @FRC.GravML.count_face (And.intro @FRC.GravML.merger_area_law (And.intro @FRC.Strong.capacity_ratio (@FRC.Strong.capacity_ratio_numeral))) /-- 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}. -/ theorem 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 : ℝ)) := And.intro @FRC.Strong.registration_root (And.intro @FRC.Strong.crossover_limits (@FRC.Strong.crossover_deep_limit)) /-- p38010 — 38:B2. The radial ladder: shells at $R\sin(2a\pi/13)$ [chart]; capacity $4a<\p\Leftrightarrow a\le\kap$. -/ theorem 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 := @FRC.Chart.ladder_monotone /-- 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)$. -/ theorem 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 := @FRC.Chart.floor_value /-- 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). -/ theorem 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 : ℝ) := And.intro @FRC.Chart.floor_value (@FRC.Chart.running_floor) -- end keys end FRC.LedgerML /-! inlined: FrcLedger/Keys/Gravity.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Keys.Gravity — the keyed theorems of the gravity theme (ledger migration, task LM19) One declaration per key, `FRC.LedgerML.p`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration `FRC..p` as an alias. Every declaration has the axioms of Mathlib's hierarchy at most (`check_axioms.py`). -/ namespace FRC.LedgerML -- Keys of the gravity theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file) /-- 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$. -/ 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 : ℕ))) := And.intro @FRC.GravML.calibration_congruence (@FRC.GravML.hbar_register) /-- 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$. -/ theorem 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 : ℕ) := And.intro @FRC.GravML.cover_forcing (@FRC.GravML.channel_q4) set_option linter.defProp false in /-- 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. -/ def p21017 := @FRC.GravML.newton_register /-- 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). -/ theorem 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 := @FRC.GravML.central_difference_adjoint set_option linter.defProp false in /-- 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). -/ def p21031 := And.intro @FRC.GravML.calibration_congruence (@FRC.GravML.newton_register) /-- 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. -/ theorem 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 := @FRC.GravML.shift_theorem /-- 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. -/ theorem 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 : ℚ))) := @FRC.GravML.cover_forcing /-- 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. -/ theorem 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 : ℚ) := @FRC.GravML.registration_dictionary /-- 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. -/ theorem 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 : ℚ) + ω)| < ε := @FRC.GravML.ppn_faces -- end keys end FRC.LedgerML /-! FrcLedger/Gravity.lean -/ /-! # 21-gravity — the paper module on Mathlib: every row's declaration under the paper's name (10 October 2026) Rows of the predicate ledger of *Gravitation as Phase Synchronisation over Finite Holographic Substrate* (tree `21-gravity-20260623`). Since 10 October 2026 (the paper's migration to the framework, `reports/blueprint-20261010.md`) the theorems live in the themes and every name here is an alias: the exact faces in `FrcLedger/Theme/Gravity.lean` (`FRC.GravML`: the Carrier register, the count face and the merger law, the cover forcing over `ℚ`, the channel, the central difference and the shift theorem on `ZMod N`), the chart readings in `FrcLedger/Theme/Strong.lean` (`FRC.Strong`: the operational cut, the photon sphere, the shadow and the ringdown, the ISCO and its efficiency, the capacity ratio and the preferred-frame scale re-anchored to the scale import `ln Ω = 283.5`, `Ω = 1.3 × 10¹²³`, the redshift, the registration root and the crossover, the discriminant, the fixed point, the dispersion symbol, the locked sum, the exponential reading, the post-Newtonian brackets, dilution), and the floor and the tilt in `FrcLedger/Theme/Chart.lean` (`FRC.Chart.floor_value`, `FRC.Chart.tilt_ledger`; the tilt was bracketed at `281` here before 10 October 2026). Classical (tier 2) on Mathlib's hierarchy; the finite content — the register on every frame, the channel, the defect's recurrence, the pair tally, the Gauss law, the post-Newtonian coefficients, the central difference and the shift theorem — is proved with no axioms in the core (`FrcCore/Theme/Gravity.lean`, `Theme/Drift.lean`, `Theme/Lattice.lean`, `Theme/Shift.lean`; the aliases `FrcCore/Gravity.lean`). `make_predicates.py` writes the typed predicates `FRC.Gravity.p21NNN` below this module's declarations. -/ namespace FRC.Gravity open Real /-! ## Old names (10 October 2026): every declaration of this module is an alias of a theme's, under the paper's name — `FRC.GravML` (`Theme/Gravity.lean`), `FRC.Strong` (`Theme/Strong.lean`), `FRC.Chart` (`Theme/Chart.lean`) -/ section register variable {K : Type*} [Field K] /-- 21:C16, 21:A1 — the calibration congruence: on the Carrier chart `4S + 1 = 0` the full cycle `2π ↦ 4S` is `−1` and `(4S)² = 1`, one residue relation. (`FRC.GravML.calibration_congruence`, `Theme/Gravity.lean`). -/ theorem calibration_congruence (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) : ((4 * S : ℕ) : K) = -1 ∧ ((4 * S : ℕ) : K) ^ 2 = 1 := FRC.GravML.calibration_congruence S hΩ /-- 21:C2, 21:C5, 21:C16 — the register value of the Newton constant, `G = 2S`, on the Carrier chart `4S + 1 = 0`: `2G = −1` (the half-cycle); `(−2) G = 1`, the face convention `4π ↦ −2` with `G = (−2)⁻¹`; the Gauss count `(2 · 4S) G = 1`; `c² = 2⁻¹ = 2S + 1` and `G = −c²` (the chart ratio `4π/2π = 2` is read as `(−2)/(−1)`). The uniqueness of the linear solution is `Dimensions.G_unique`. (`FRC.GravML.newton_register`, `Theme/Gravity.lean`). -/ theorem newton_register (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) : 2 * ((2 * S : ℕ) : K) = -1 ∧ (-2) * ((2 * S : ℕ) : K) = 1 ∧ (2 * ((4 * S : ℕ) : K)) * ((2 * S : ℕ) : K) = 1 ∧ 2 * ((2 * S + 1 : ℕ) : K) = 1 ∧ ((2 * S + 1 : ℕ) : K) = 2⁻¹ ∧ ((2 * S : ℕ) : K) = -((2 * S + 1 : ℕ) : K) := FRC.GravML.newton_register S hΩ /-- 21:C5, 21:C16, 21:A1 — the action quantum as the quarter-turn pair: on every Carrier `Ω = 4S + 1` prime, `S` is a square (`S = (i/2)²` with `i² = −1`, since `4S = −1`), so `ħ = 2√S` has `ħ² = 4S = −1` — `ħ` is one of the quarter-turn pair `±i`. (`FRC.GravML.hbar_register`, `Theme/Gravity.lean`). -/ theorem hbar_register (S : ℕ) [Fact (Nat.Prime (4 * S + 1))] : ∃ r : ZMod (4 * S + 1), r ^ 2 = (S : ZMod (4 * S + 1)) ∧ (2 * r) ^ 2 = -1 := FRC.GravML.hbar_register S /-- 21:X8, 21:C5 — the weakness of gravity as cardinality dilution: with the Planck mass the locality horizon, `m_P = √Ω`, the dimensionless coupling of two masses `m` is `(m/m_P)² = m²/Ω`, small because `Ω` is large. C5's frame covariance is not formal content. (`FRC.Strong.dilution`, `Theme/Strong.lean`). -/ theorem dilution (m Ω : ℝ) (hΩ : 0 < Ω) : (m / √Ω) ^ 2 = m ^ 2 / Ω := FRC.Strong.dilution m Ω hΩ end register /-- 21:C13 — the count face of the area law on a symmetry-complete shell `p = 4κ + 1`: with `S = (p² − 1)/4`, i.e. `4S + 1 = p²` for `S = κ(4κ + 2)`, and the coordinate area `A = p(p + 1)`, the ratio `S/A = κ/p` holds exactly (`Sp = κA`) and `S = (A/4)(1 − 1/p)` (`4Sp = A(p − 1)`) — the Bekenstein quarter as the `Q₄` quotient. (`FRC.GravML.count_face`, `Theme/Gravity.lean`). -/ theorem count_face (κ : ℕ) : 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 * κ) := FRC.GravML.count_face κ /-- 21:C13 — the merger area law on the count face, `A = M(M + 1)`: `ΔA = 2M₁M₂` exactly under additive mass, the paper's instance `27 811 + 1 596 → 29 407` giving `ΔA = 88 772 712`; with a radiated `δ` the count gives `ΔA = 2M₁M₂ − (2(M₁ + M₂) + 1)δ + δ²`, at most the additive value for `0 ≤ δ ≤ 2(M₁ + M₂) + 1` — the area statement an inequality (the coefficient `−2(M₁ + M₂)δ` is the `A = M²` form; on the count face the linear term carries the extra `−δ`). (`FRC.GravML.merger_area_law`, `Theme/Gravity.lean`). -/ theorem merger_area_law (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 : ℤ) := FRC.GravML.merger_area_law M₁ M₂ δ /-- 21:A9, 21:C25, 21:C7, 21:C8 — the cover forcing: the apsidal coefficient `2 − β + 2γ` against the PPN-free deficit `3/2` equals the two-face ratio `2` exactly when `2γ − β = 1`, with deviation `(2/3)(2γ − β − 1)`; channel unity `γ = 1` makes the deflection factor `(1 + γ)/2` equal to `1` (the full `4Gm/c²b`) and, together with the forcing, gives `β = 1`, the perihelion factor `(2 + 2γ − β)/3` then `1`. That channel unity forces the spatial bias to equal the temporal one is Lem. isopair's argument, with `γ = 1` the exponential metric's coefficient (`pn_series` carries `B = e^{2U}` against `(1 + U/2)⁴` through `O(U)`). (`FRC.GravML.cover_forcing`, `Theme/Gravity.lean`). -/ theorem cover_forcing (β γ : ℚ) : ((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)) := FRC.GravML.cover_forcing β γ /-- 21:A9 — the mass–energy channel `C_{p−1} ∩ C_{2(p+1)} = Q₄`: on every shell `p ≡ 1 (mod 4)`, `gcd(p − 1, 2(p + 1)) = 4`; the subgroup reading — in the cyclic unit group of `𝔽_{p²}` (order `(p − 1)(p + 1)`) the subgroups of orders `p − 1` and `2(p + 1)` meet in the subgroup of order `gcd` — is not formalised here. (`FRC.GravML.channel_q4`, `Theme/Gravity.lean`). -/ theorem channel_q4 (p : ℕ) (hp : p % 4 = 1) : Nat.gcd (p - 1) (2 * (p + 1)) = 4 := FRC.GravML.channel_q4 p hp /-- 21:C12, 21:P7 — the operational cut and the slip core in the substrate coordinate (`G = 1`, `M` in Planck masses, `L = ln Ω`): `r_f = 2M/L` carries `e^{2M/r_f} = Ω` (the round-trip delay's factor); `r_* = √M < r_f` exactly when `M > (L/2)²`, and `r_f < M` exactly when `L > 2` (master E10). (`FRC.Strong.operational_cut`, `Theme/Strong.lean`). -/ theorem operational_cut (M L Ω : ℝ) (hM : 0 < M) (hL : 0 < L) (hΩ : L = log Ω) (hΩ0 : 0 < Ω) : exp (2 * M / (2 * M / L)) = Ω ∧ (√M < 2 * M / L ↔ (L / 2) ^ 2 < M) ∧ (2 * M / L < M ↔ 2 < L) := FRC.Strong.operational_cut M L Ω hM hL hΩ hΩ0 /-- 21:P1 — the photon sphere (`prop:shadow`, `rem:exponential`): the impact parameter `b(r) = r e^{2Gm/r}` of the exponential metric satisfies `b(r) ≥ 2e·Gm` for every `r > 0`, with equality exactly at `r = 2Gm` (from `x + 1 ≤ eˣ`, strict off `x = 0`): the photon sphere is at `r_ph = 2Gm`, the critical impact parameter `b_c = 2e·Gm`. (`FRC.Strong.photon_sphere`, `Theme/Strong.lean`). -/ theorem photon_sphere (Gm r : ℝ) (hG : 0 < Gm) (hr : 0 < r) : 2 * exp 1 * Gm ≤ r * exp (2 * Gm / r) ∧ (r * exp (2 * Gm / r) = 2 * exp 1 * Gm ↔ r = 2 * Gm) := FRC.Strong.photon_sphere Gm r hG hr /-- 21:P1 — the shadow and the ringdown against general relativity, bracketed from `e` (nine places) and `√3`: the critical impact parameters `b_c = 2e·Gm` (this work) and `3√3·Gm` (Schwarzschild) have ratio `2e/(3√3)` between `1.0462` and `1.0463` (the shadow `+4.6 %`), and the eikonal ringdown frequency, `∝ 1/b_c`, ratio `3√3/(2e)` between `0.9557` and `0.9558` (`−4.4 %`); the Sgr A* excess `(4e − 6√3) θ_g` at the GRAVITY `θ_g = 5.12 µas` [data, A8] lies between `2.46` and `2.47 µas` (the `2.5 µas` of the text). (`FRC.Strong.shadow_bracket`, `Theme/Strong.lean`). -/ theorem shadow_bracket : (1.0462 : ℝ) < 2 * exp 1 / (3 * √3) ∧ 2 * exp 1 / (3 * √3) < 1.0463 ∧ (0.9557 : ℝ) < 3 * √3 / (2 * exp 1) ∧ 3 * √3 / (2 * exp 1) < 0.9558 ∧ (2.46 : ℝ) < (4 * exp 1 - 6 * √3) * 5.12 ∧ (4 * exp 1 - 6 * √3) * 5.12 < 2.47 := FRC.Strong.shadow_bracket /-- 21:P1 — the innermost stable circular orbit of the exponential metric (`G = m = 1`, isotropic radius), with the circular-orbit relations of the paper's `prop:isco` taken as given and not formalised (`L² = e^{2/r} r²/(r − 2)` and `E² = e^{−2/r}(r − 1)/(r − 2)` for a circular orbit at `r > 2`): what is proved is that `log L²` has derivative `(r² − 6r + 4)/(r²(r − 2))`, that `r_ISCO = 3 + √5` is the root of `r² − 6r + 4` above `2`, and that `(r − 1)/(r − 2) = r/4` there, so `E² = e^{−2/r} r/4` at the orbit. (`FRC.Strong.isco`, `Theme/Strong.lean`). -/ theorem isco (r : ℝ) (hr : 2 < r) : HasDerivAt (fun r : ℝ => 2 / r + 2 * log r - 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 := FRC.Strong.isco r hr /-- 21:P1 — the accretion efficiency bracketed: at `r_ISCO = 3 + √5` the orbital energy `E = √(e^{−2/r} r/4)` lies between `0.9452` and `0.9453`, so `1 − E` is between `5.47 %` and `5.48 %` (the text's `5.48 %`), against Schwarzschild's `1 − √(8/9)` between `5.71 %` and `5.72 %`. (`FRC.Strong.isco_efficiency`, `Theme/Strong.lean`). -/ theorem isco_efficiency : (0.0547 : ℝ) < 1 - √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) ∧ 1 - √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) < 0.0548 ∧ (0.0571 : ℝ) < 1 - √(8 / 9) ∧ 1 - √(8 / 9) < (0.0572 : ℝ) := FRC.Strong.isco_efficiency /-- 21:C13 — the arithmetic behind the capacity ratio: for `r_f = r_s/L` the square of `r_f/r_s` is `1/L²`, and at `L = ln Ω = 283.5` (the scale import) the ratio lies between `1.24 × 10⁻⁵` and `1.25 × 10⁻⁵` (the text's `1.24 × 10⁻⁵`); that the externally resolvable capacity scales as `(r_f/r_s)²` is the paper's count, not formal content. (`FRC.Strong.capacity_ratio`, `Theme/Strong.lean`). -/ theorem capacity_ratio (rs L : ℝ) (hrs : rs ≠ 0) (hL : L ≠ 0) : (rs / L / rs) ^ 2 = 1 / L ^ 2 := FRC.Strong.capacity_ratio rs L hrs hL /-- 21:P7, 21:C13 — the capacity ratio's numeral at the scale import's `ln Ω = 283.5`: `1/283.5²` lies between `1.24 × 10⁻⁵` and `1.25 × 10⁻⁵`, the text's `S/S_BH = 1.24 × 10⁻⁵`. (`FRC.Strong.capacity_ratio_numeral`, `Theme/Strong.lean`). -/ theorem capacity_ratio_numeral : (1.24e-5 : ℝ) < 1 / 283.5 ^ 2 ∧ (1 / 283.5 ^ 2 : ℝ) < 1.25e-5 := FRC.Strong.capacity_ratio_numeral /-- 21:C4 — the redshift as clock rate: the bias field `e^{−u}` with `u = Gm/rc²` gives `Δf/f = 1 − e^{−u} = u + O(u²)`, `|1 − e^{−u} − u| ≤ u²` on `0 ≤ u ≤ 1`. (`FRC.Strong.redshift_linear`, `Theme/Strong.lean`). -/ theorem redshift_linear (u : ℝ) (h0 : 0 ≤ u) (h1 : u ≤ 1) : |1 - exp (-u) - u| ≤ u ^ 2 := FRC.Strong.redshift_linear u h0 h1 /-- 21:C19, 21:P4 — the registration root: for `0 < w < 1` the quadratic `wη² − 2η + w = 0` (rational in the paper's `w`, here over `ℝ`) has exactly the roots `(1 ∓ √(1 − w²))/w`; the smaller, `η = (1 − √(1 − w²))/w`, lies in `(0, 1)` and the larger exceeds `1`, so the in-`(0, 1)` root that fixes the resolved fraction `f = 1 − η^a` is unique. (`FRC.Strong.registration_root`, `Theme/Strong.lean`). -/ theorem registration_root (w : ℝ) (hw0 : 0 < w) (hw1 : 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) := FRC.Strong.registration_root w hw0 hw1 /-- 21:C19, 21:P4 — the crossover `g_obs = g_N/(1 − e^{−√x})`, `x = g_N/a₀`, squeezed: with `t = √x > 0`, `1 ≤ t/(1 − e^{−t})`, and `t/(1 − e^{−t}) ≤ 1/(1 − 3t/4)` for `t ≤ 1`; and the Tully–Fisher algebra is exact: `v² = g_obs r` with `g_obs = √(g_N a₀)`, `g_N = GM/r²`, gives `v⁴ = GMa₀`. (`FRC.Strong.crossover_limits`, `Theme/Strong.lean`). -/ theorem crossover_limits (t : ℝ) (ht : 0 < t) : 0 < 1 - exp (-t) ∧ 1 ≤ t / (1 - exp (-t)) ∧ (t ≤ 1 → t / (1 - 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₀) := FRC.Strong.crossover_limits t ht /-- 21:C19, 21:P4, 21:X2 — the deep limit: `t/(1 − e^{−t}) → 1` as `t → 0⁺`, so `g_obs/√(g_N a₀) → 1` — the deep regime `g_obs = √(g_N a₀)`, the floor read as noise with no dark sector. (`FRC.Strong.crossover_deep_limit`, `Theme/Strong.lean`). -/ theorem crossover_deep_limit : Filter.Tendsto (fun t : ℝ => t / (1 - exp (-t))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) := FRC.Strong.crossover_deep_limit /-- 21:C19, 21:P4 — the Newtonian limit: `1 − e^{−t} → 1` as `t → ∞`, so `g_obs/g_N → 1` for `x → ∞`. (`FRC.Strong.crossover_newton_limit`, `Theme/Strong.lean`). -/ theorem crossover_newton_limit : Filter.Tendsto (fun t : ℝ => 1 - exp (-t)) Filter.atTop (nhds 1) := FRC.Strong.crossover_newton_limit /-- 21:P4 — the discriminant against the simple interpolant at `g_N = 5a₀`: the crossover `ν(5) = 1/(1 − e^{−√5})` lies between `1.11966` and `1.11967`, the simple interpolant `ν_s(5) = 1/2 + √(1/4 + 1/5)` between `1.17082` and `1.17083`, so they part by between `0.0511` and `0.0512` in `g_obs/g_N` (the text's `0.05`). (`FRC.Strong.interpolant_discriminant`, `Theme/Strong.lean`). -/ theorem interpolant_discriminant : (1.11966 : ℝ) < 1 / (1 - exp (-√5)) ∧ 1 / (1 - exp (-√5)) < 1.11967 ∧ (1.17082 : ℝ) < 1 / 2 + √(1 / 4 + 1 / 5) ∧ 1 / 2 + √(1 / 4 + 1 / 5) < 1.17083 ∧ (0.0511 : ℝ) < (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) ∧ (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) < 0.0512 := FRC.Strong.interpolant_discriminant /-- 21:C18 — the fixed point: for a power law `P(k) = k^n` the dimensionless `k³P(k)` is the same at every scale `k > 0` exactly when `n = −3`, i.e. `n_s − 1 = n + 3 = 0`, the Harrison–Zel'dovich `n_s = 1`, uniquely; that the drive's jitter spectrum is this fixed point is the paper's argument. (`FRC.Strong.scale_invariance_iff`, `Theme/Strong.lean`). -/ theorem scale_invariance_iff (n : ℝ) : (∀ k : ℝ, 0 < k → k ^ 3 * k ^ n = 1) ↔ n = -3 := FRC.Strong.scale_invariance_iff n /-- 21:C15 — the dispersion symbol: the central second difference acts on the plane wave `e^{ikx}` by `−(2 − 2 cos k) = −4 sin²(k/2)`; the wave equation, its two polarisations and the speed `c` are the package's. (`FRC.Strong.dispersion_symbol`, `Theme/Strong.lean`). -/ theorem dispersion_symbol (k : ℝ) : 2 - 2 * cos k = 4 * sin (k / 2) ^ 2 := FRC.Strong.dispersion_symbol k /-- 21:C1 — the coherent coefficient: a locked cluster of `m` cells with one phase sums with coefficient exactly `m`, `‖Σ_{j ζ ^ (a.val * x.val) * f x) k = dft ζ f (k + a) ∧ dft ζ (fun x => f (x - a)) k = ζ ^ (a.val * k.val) * dft ζ f k := FRC.GravML.shift_theorem ζ hζ f a k end lattice /-- 21:C18, 21:P8 — the tilt's numerals at the ledger's `ln Ω = 283.5` (`FRC.Chart.tilt_ledger`, the scale import 00:A7; before 10 October 2026 this name bracketed the tilt at `281`): `−π²/283.5` between `−0.03482` and `−0.03481` (the row's `−0.0348`), `+0.07σ` from Planck 2018's `−0.0351 ± 0.0042` [data], and `½ ln Ω` excluded at `8.2σ`. -/ theorem tilt_bracket : (0.03481 : ℝ) < π ^ 2 / 283.5 ∧ π ^ 2 / 283.5 < 0.03482 ∧ (0.068 * 0.0042 : ℝ) < 0.0351 - π ^ 2 / 283.5 ∧ 0.0351 - π ^ 2 / 283.5 < 0.069 * 0.0042 ∧ (8.2 * 0.0042 : ℝ) < π ^ 2 / (283.5 / 2) - 0.0351 ∧ π ^ 2 / (283.5 / 2) - 0.0351 < 8.25 * 0.0042 := FRC.Chart.tilt_ledger /-- 21:P3 — the floor `a₀ = cH₀/2π` at the entailed `H₀ = 67.4`: between `1.04` and `1.05 × 10⁻¹⁰ m s⁻²`, `13 %` low and `0.7σ` against the fitted `1.20 ± 0.24 × 10⁻¹⁰`. -/ theorem floor_value (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) : (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.05e-10 ∧ (0.868 : ℝ) < c * H0 / (2 * π) / 1.2e-10 ∧ c * H0 / (2 * π) / 1.2e-10 < 0.870 ∧ (0.65 : ℝ) < (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 ∧ (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 < 0.67 := FRC.Chart.floor_value c H0 hc hH /-- 21:P5 — the running floor: if the floor is read at every redshift on the registered rate, `a₀(z) = cH(z)/2π`, and the deep regime's `v⁴ = GMa₀` holds at fixed baryonic mass `M`, then `a₀(z)/a₀(0) = H(z)/H(0) = E(z)` and the Tully–Fisher zero-point evolves as `v(z)/v(0) = E(z)^{1/4}`; that the floor tracks the registered rate is the row's realisation clause (00:D5), not formal content. (`FRC.Chart.running_floor`, `Theme/Chart.lean`, the master's 00:P1). -/ theorem running_floor (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ) (hc : 0 < c) (hG : 0 < G) (hM : 0 < M) (h0 : 0 < H 0) (hz : 0 < H z) (ha : ∀ z, a z = c * H z / (2 * π)) (hv0 : 0 < v 0) (hvz : 0 < v z) (htf : ∀ 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 : ℝ) := FRC.Chart.running_floor c G M H a v z hc hG hM h0 hz ha hv0 hvz htf -- Ledger predicates of 21-gravity (generated by make_predicates.py from docs/21-gravity/21-gravity-ledger.json; edit the ledger, not this section) /-- 21:A1 (p21001) — 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$. -/ 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 : ℕ))) := @FRC.LedgerML.p21001 /-- 21:A9 (p21009) — 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$. -/ theorem 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 : ℕ) := @FRC.LedgerML.p21009 set_option linter.defProp false in /-- 21:C1 (p21016) — 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$. -/ def p21016 := @FRC.LedgerML.p21016 set_option linter.defProp false in /-- 21:C2 (p21017) — 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. -/ def p21017 := @FRC.LedgerML.p21017 /-- 21:C4 (p21019) — 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. -/ theorem p21019 : ∀ (u : ℝ), (0 : ℝ) ≤ u → u ≤ (1 : ℝ) → |(1 : ℝ) - Real.exp (-u) - u| ≤ u ^ (2 : ℕ) := @FRC.LedgerML.p21019 /-- 21:C5 (p21020) — The magnitude $G=\hbar c/m_P^2$, frame-covariant (a relativity principle for scale); gravity's weakness is cardinality dilution. -/ theorem 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 : ℕ) / Ω := @FRC.LedgerML.p21020 /-- 21:C7 (p21022) — Channel unity forces the spatial bias to equal the temporal one, $\gamma=1$, restoring the full light deflection $4Gm/c^2b$. -/ theorem 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 : ℕ) := @FRC.LedgerML.p21022 /-- 21:C8 (p21023) — The exponential isotropic metric by multiplicative composition, with $\beta=\gamma=1$: deflection, Shapiro delay, and perihelion at their observed values. -/ theorem 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 : ℕ) := @FRC.LedgerML.p21023 /-- 21:C9 (p21024) — The discrete Fierz--Pauli functional, exactly gauge-invariant and the unique adjacency-local stiffness on the shell (the spin-one case is unique-Maxwell). -/ theorem 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 := @FRC.LedgerML.p21024 /-- 21:C11 (p21026) — 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. -/ theorem 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 : ℕ) := @FRC.LedgerML.p21026 /-- 21:C12 (p21027) — 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_*(\ln\Omega/2)^{2}$ Planck masses (master E10). -/ theorem 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) := @FRC.LedgerML.p21027 /-- 21:C13 (p21062) — 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. -/ theorem 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 := @FRC.LedgerML.p21062 /-- 21:C15 (p21030) — 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. -/ theorem p21030 : ∀ (k : ℝ), (2 : ℝ) - (2 : ℝ) * Real.cos k = (4 : ℝ) * Real.sin (k / (2 : ℝ)) ^ (2 : ℕ) := @FRC.LedgerML.p21030 set_option linter.defProp false in /-- 21:C16 (p21031) — 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). -/ def p21031 := @FRC.LedgerML.p21031 /-- 21:C18 (p21033) — 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. -/ theorem 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 := @FRC.LedgerML.p21033 /-- 21:C19 (p21064) — 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}. -/ theorem 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 : ℝ)) := @FRC.LedgerML.p21064 /-- 21:C20 (p21035) — 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. -/ theorem 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 := @FRC.LedgerML.p21035 /-- 21:C25 (p21040) — 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. -/ theorem 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 : ℚ))) := @FRC.LedgerML.p21040 /-- 21:X2 (p21042) — \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$. -/ theorem p21042 : Filter.Tendsto (fun t => t / ((1 : ℝ) - Real.exp (-t))) (nhdsWithin (0 : ℝ) (Set.Ioi (0 : ℝ))) (nhds (1 : ℝ)) := @FRC.LedgerML.p21042 /-- 21:X8 (p21048) — \textbf{The weakness of gravity} is cardinality dilution, not a hierarchy to be tuned. -/ theorem p21048 : ∀ (m Ω : ℝ), (0 : ℝ) < Ω → (m / √Ω) ^ (2 : ℕ) = m ^ (2 : ℕ) / Ω := @FRC.LedgerML.p21048 /-- 21:P1 (p21049) — Strong-field signatures at or outside the photon sphere: shadow $+4.6\%$, ringdown $-4.4\%$, 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. -/ theorem 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 := @FRC.LedgerML.p21049 /-- 21:P7 (p21050) — 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. -/ theorem 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) := @FRC.LedgerML.p21050 /-- 21:P8 (p21060) — 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$. -/ theorem 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 := @FRC.LedgerML.p21060 /-- 21:P2 (p21051) — 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. -/ theorem p21051 : 27e-63 < (1 : ℝ) / √13e122 ∧ (1 : ℝ) / √13e122 < 28e-63 := @FRC.LedgerML.p21051 /-- 21:P3 (p21052) — 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. -/ theorem 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 := @FRC.LedgerML.p21052 /-- 21:P4 (p21053) — 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$. -/ theorem 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 := @FRC.LedgerML.p21053 /-- 21:P5 (p21054) — The floor tracks the expansion, $a_0(z)\propto H(z)$ (BTFR zero-point $\propto E(z)^{1/4}$); high-$z$ rotation curves decisive. -/ theorem 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 : ℝ) := @FRC.LedgerML.p21054 /-- 21:P6 (p21055) — 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. -/ theorem 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 : ℕ) := @FRC.LedgerML.p21055 -- end ledger predicates end FRC.Gravity -- Ledger predicates: axioms (each predicate's, computed here) #print axioms FRC.Gravity.p21001 #print axioms FRC.Gravity.p21009 #print axioms FRC.Gravity.p21016 #print axioms FRC.Gravity.p21017 #print axioms FRC.Gravity.p21019 #print axioms FRC.Gravity.p21020 #print axioms FRC.Gravity.p21022 #print axioms FRC.Gravity.p21023 #print axioms FRC.Gravity.p21024 #print axioms FRC.Gravity.p21026 #print axioms FRC.Gravity.p21027 #print axioms FRC.Gravity.p21062 #print axioms FRC.Gravity.p21030 #print axioms FRC.Gravity.p21031 #print axioms FRC.Gravity.p21033 #print axioms FRC.Gravity.p21064 #print axioms FRC.Gravity.p21035 #print axioms FRC.Gravity.p21040 #print axioms FRC.Gravity.p21042 #print axioms FRC.Gravity.p21048 #print axioms FRC.Gravity.p21049 #print axioms FRC.Gravity.p21050 #print axioms FRC.Gravity.p21060 #print axioms FRC.Gravity.p21051 #print axioms FRC.Gravity.p21052 #print axioms FRC.Gravity.p21053 #print axioms FRC.Gravity.p21054 #print axioms FRC.Gravity.p21055