import Mathlib /-! Generated by `lean/make_web.py` from `FrcLedger/Gravity.lean` — one self-contained file for the Lean web editor. Edit the modules, not this file. -/ /-! FrcLedger/Gravity.lean -/ /-! # 21-gravity — the Carrier register, the count face, the strong field and the floor: the ledger predicates in Lean (2026-09-20) Rows of the predicate ledger of *Gravitation as Phase Synchronisation over Finite Holographic Substrate* (tree `21-gravity-20260623`). The Carrier register: the calibration congruence `2π ↦ 4S ≡ −1`, `(4S)² ≡ 1`, and the register value of the Newton constant `G = 2S` — `2G = −1`, `G = (−2)⁻¹` (the face convention `4π ↦ −2`), the Gauss count `(2 · 4S)⁻¹ = 2S`, `G = −c²` with `c² = 2⁻¹ = 2S + 1`, the chart ratio `4π/2π = 2` as `(−2)/(−1)` — and the action quantum as one of the quarter-turn pair `±i`, `ħ = 2√S` with `ħ² = 4S = −1` on every Carrier (C2, C5, C16; the laboratory Carrier's residues are `Dimensions.carrierLab`). The count face of the area law on a symmetry-complete shell, `S/A = κ/p` and `S = (A/4)(1 − 1/p)` exactly, the merger law `ΔA = 2M₁M₂` with its radiating form and the paper's instance (C13); the cover forcing `2γ − β = 1` with its deviation and the triangle `γ = 1 ∧ 2γ − β = 1 ⇒ β = 1` with the perihelion factor (A9, C7, C8, C25); the mass–energy channel `gcd(p − 1, 2(p + 1)) = 4` on every `p ≡ 1 (mod 4)` (A9). The strong field: the operational cut `e^{2M/r_f} = Ω` with the ordering `r_* < r_f < M` exactly when `M > (ln Ω/2)²` and `ln Ω > 2` (C12); the photon sphere at `r = 2Gm` with `b_c = 2e·Gm` as the minimum of `r e^{2Gm/r}` (C12, P1); the shadow `+4.6 %` and ringdown `−4.4 %` bracketed from `e` and `√3`, the Sgr A* excess (P1); the innermost stable orbit — with the circular-orbit `L²` of the paper taken as given, the stationarity root `r = 3 + √5` and `E² = e^{−2/r} r/4` there — and the efficiency `5.48 %` against Schwarzschild's `5.72 %` bracketed (P1); the capacity ratio `ln⁻²Ω` (C13); the redshift's linear form (C4). The floor `a₀ = cH₀/2π` at the entailed `H₀` against the SPARC scale, `13 %` low and `0.7σ` (P3); the registration root `η` of `wη² − 2η + w = 0` in `(0, 1)`, the crossover squeezed between its deep and Newtonian limits — both as limits — with the Tully–Fisher algebra (C19, P4); the discriminant `0.05` at `g_N = 5a₀` against the simple interpolant (P4). The primordial spectrum: scale invariance of `k³P(k)` exactly at `n_s = 1`, the tilt `−π²/ln Ω = −0.0351` at `ln Ω = 281` (`122 ln 10 = 280.9`), the `8.4σ` exclusion of `½ ln Ω`, the `0.25 %` per factor two (C18, P8). The lattice: the central difference is anti-self-adjoint on the cycle (`Δᵀ = −Δ`, the identity carrying the Fierz–Pauli gauge invariance) while the adjoint of the one-sided difference is the negative backward difference (C9); the finite Fourier shift theorem in both forms — the kick as a character in position, the position shift as a character on the transform (C20); the arithmetic behind C15's dispersion symbol and C1's coherent coefficient. The series: the exponential reading is multiplicative and the isotropic Schwarzschild factor is `e^{−2 artanh(U/2)}`, violating the composition law (C11); the post-Newtonian Taylor brackets — `A − A_S = U³/6 + O(U⁴)`, `B − B_S = U²/2 + O(U³)` — the single-potential inputs shared through 1PN and parting at 2PN (C8, P6); the numeral behind P2's preferred-frame scale, `1/√Ω = 10⁻⁶¹`. Classical (tier 2) on Mathlib's hierarchy; the finite content — the register on every frame, the count face, the merger instance, the laboratory Carrier decided by the kernel — is proved with no axioms in `FrcCore/Gravity.lean`. Outside both modules: the realisations of block B, the synchronisation dynamics (the Kuramoto relaxation, C1's gradient flow, C21, C22), the four-term Fierz–Pauli functional itself (the package's exact integer identity), the orbit equations behind the ISCO, the two-body sector of C23, the rotating solution and the wave equation beyond their symbols, and every comparison with measured data, which enters below only as declared numerals [data]. -/ namespace FRC.Gravity open Real /-! ## The Carrier register (21:C2, C5, C16, X8) -/ 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) /-- The arithmetic behind 21:X8 — 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 count face and the cover forcing (21:A9, B2, 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` together with the forcing gives `β = 1`, and the perihelion factor `(2 + 2γ − β)/3` is then `1` (the deflection factor `(1 + γ)/2` is `1` at `γ = 1`). -/ theorem cover_forcing (β γ : ℝ) : ((2 - β + 2 * γ) / (3 / 2) = 2 ↔ 2 * γ - β = 1) ∧ (2 - β + 2 * γ) / (3 / 2) - 2 = 2 / 3 * (2 * γ - β - 1) ∧ (γ = 1 → 2 * γ - β = 1 → β = 1 ∧ (2 + 2 * γ - β) / 3 = 1) := by refine ⟨?_, by ring, ?_⟩ · constructor <;> intro h <;> linarith · rintro rfl h exact ⟨by linarith, by linarith⟩ /-- 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 strong field (21:C4, C12, C13, P1, P7, X3) -/ 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 Ω = 281` the ratio lies between `1.26 × 10⁻⁵` and `1.27 × 10⁻⁵` (the text's `1.3 × 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.26e-5 : ℝ) < 1 / 281 ^ 2 ∧ (1 / 281 ^ 2 : ℝ) < 1.27e-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 registration crossover (21:C19, P3, P4, X2) -/ section floor /-- 21:P3 — the weak-acceleration floor `a₀ = cH₀/2π` at the entailed `H₀ = 67.4 km s⁻¹ Mpc⁻¹` (the `H₀` of `\cite{entropy}`, the speed of light and the megaparsec all 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 /-- 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 spectrum (21:C18, P8, X6) -/ section primordial /-- The arithmetic behind 21:C18's 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') /-- The Taylor brackets of `e^t` at `t = 0.30259` (below) and `t = 0.30258` (above), the two sides of `ln 10 − 2`. -/ theorem exp_log_ten_tail_bounds : (1.353359 : ℝ) < exp 0.30259 ∧ exp (0.30258 : ℝ) < 1.353346 := by constructor · have h := abs_le.1 (Real.exp_bound (x := 0.30259) (by rw [abs_of_pos (by norm_num)]; norm_num) (n := 7) (by norm_num)) rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.30259)] at h have h1 := h.1 norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢ linarith · have h := Real.exp_bound' (x := 0.30258) (by norm_num) (by norm_num) (n := 8) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢ linarith /-- 21:P8 — `ln 10` bracketed: `2.30258 < ln 10 < 2.30259`, from `e` to nine places and the Taylor tail. -/ theorem log_ten_bounds : (2.30258 : ℝ) < log 10 ∧ log 10 < 2.30259 := by have e1 := Real.exp_one_gt_d9 have e2 := Real.exp_one_lt_d9 obtain ⟨t1, t2⟩ := exp_log_ten_tail_bounds have he : (0 : ℝ) < exp 1 := exp_pos 1 constructor · rw [Real.lt_log_iff_exp_lt (by norm_num)] have : exp (2.30258 : ℝ) = exp 1 * exp 1 * exp 0.30258 := by rw [← exp_add, ← exp_add]; norm_num rw [this]; nlinarith [mul_pos he he, exp_pos (0.30258 : ℝ)] · rw [Real.log_lt_iff_lt_exp (by norm_num)] have : exp (2.30259 : ℝ) = exp 1 * exp 1 * exp 0.30259 := by rw [← exp_add, ← exp_add]; norm_num rw [this]; nlinarith [mul_pos he he, exp_pos (0.30259 : ℝ)] /-- 21:C18, 21:P8 — the tilt's numerals bracketed: the e-fold count `ln Ω` at `Ω = 10¹²²` is `122 ln 10`, between `280.91` and `280.92` (the anchored `281`); the committed tilt `−π²/281` lies between `−0.035124` and `−0.035123` (the text's `−0.0351`, against Planck's `−0.0351 ± 0.0042` [data]); the neighbouring count `½ ln Ω` gives `−π²/140.5`, parted from the committed value by more than `8.36σ` and less than `8.37σ` at `σ = 0.0042` (the text's `8.4σ`); and a factor two in `S` moves the tilt by the fraction `ln 2/281`, between `0.246 %` and `0.247 %` (the text's `0.25 %`). -/ theorem tilt_bracket : (280.91 : ℝ) < 122 * log 10 ∧ 122 * log 10 < 280.92 ∧ (-0.035124 : ℝ) < -(π ^ 2 / 281) ∧ -(π ^ 2 / 281) < -0.035123 ∧ (8.36 : ℝ) * 0.0042 < π ^ 2 / 140.5 - π ^ 2 / 281 ∧ π ^ 2 / 140.5 - π ^ 2 / 281 < 8.37 * 0.0042 ∧ (0.00246 : ℝ) < log 2 / 281 ∧ log 2 / 281 < 0.00247 := by obtain ⟨l1, l2⟩ := log_ten_bounds have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hp2 : (9.8696002 : ℝ) < π ^ 2 := by nlinarith have hp2' : π ^ 2 < (9.8696066 : ℝ) := by nlinarith have h2a := Real.log_two_gt_d9 have h2b := Real.log_two_lt_d9 have hσ : π ^ 2 / 140.5 - π ^ 2 / 281 = π ^ 2 / 281 := by ring rw [hσ] refine ⟨by linarith, by linarith, by linarith, by linarith, ?_, ?_, by linarith, by linarith⟩ · norm_num; linarith · norm_num; linarith end primordial /-! ## The lattice (21:C1, C9, C15, 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 /-- The arithmetic behind 21:C15's 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 /-- The arithmetic behind 21:C1's 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 — 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] /-- The numeral behind 21:P2: the drive's signature is `O(1/√Ω)` (the paper's `α₁, α₂`), and at `Ω = 10¹²²` this is `10⁻⁶¹`. -/ theorem preferred_frame_scale : 1 / √((10 : ℝ) ^ 122) = 10 ^ (-61 : ℤ) := by rw [show (10 : ℝ) ^ 122 = (10 ^ 61) ^ 2 by norm_num, Real.sqrt_sq (by positivity)] norm_num end series end FRC.Gravity