Theme/Strong.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Chart34/-!5# FrcLedger.Theme.Strong — the chart theme's strong field, crossover and series (10 October 2026)67The readings of 21-gravity on the reals, moved from the paper module `FrcLedger/Gravity.lean` (which keeps every old8name as an alias), every numeral re-anchored to the ledger's scale import (00:A7: `ln Ω = 283.5`, `Ω = 1.3 × 10¹²³`;9`Theme/Chart.lean`'s `ln_omega_ledger`). The strong field: the operational cut `e^{2M/r_f} = Ω` with the ordering10`r_* < r_f < M` exactly when `M > (ln Ω/2)²` (21:C12, P7); the photon sphere at `r = 2Gm` with `b_c = 2e·Gm` as the11minimum of `r e^{2Gm/r}` (21:C12, P1); the shadow `+4.6 %` and ringdown `−4.4 %` bracketed from `e` and `√3` (21:P1); the eikonal pair12`Ω_c = λ = 1/(2eM)` from the derivatives of `r² e^{4M/r}` at `2M` (00:E14, 16 October 2026);13the innermost stable orbit at `r = 3 + √5` and the efficiency `5.48 %` against Schwarzschild's `5.72 %` (21:P1); the14capacity ratio `1/ln²Ω = 1.24 × 10⁻⁵` at `283.5` (21:C13); the redshift's linear form (21:C4). The crossover: the15registration root `η` of `wη² − 2η + w = 0` in `(0, 1)`, the crossover squeezed between its deep and Newtonian16limits, the Tully–Fisher algebra (21:C19, P4, X2); the discriminant `0.051` at `g_N = 5a₀` against the simple17interpolant (21:P4). The primordial fixed point `n_s = 1` (21:C18; the tilt at `283.5` is `Chart.tilt_ledger`).18The dispersion symbol and the locked sum on `ℂ` (21:C15, C1). The series: the exponential reading composes and the19isotropic Schwarzschild factor is `e^{−2 artanh(U/2)}` (21:C11); the post-Newtonian Taylor brackets (21:C8, P6); the20preferred-frame scale `1/√Ω` at `1.3 × 10¹²³` (21:P2, C10); cardinality dilution (21:X8, C5). Classical (tier 2) on21Mathlib's hierarchy; every bracket from `π` to six places, `e` to nine and the Taylor tail of `exp`. The finite22content is proved with no axioms in the core (`FrcCore/Theme/Drift.lean`, `Theme/Lattice.lean`); the exact Mathlib23variants are `Theme/Gravity.lean`'s.24-/2526namespace FRC.Strong2728open Real2930/-! ## Cardinality dilution (21:X8, C5) -/31section register3233/-- 21:X8, 21:C5 — the weakness of gravity as cardinality dilution: with the Planck mass the34locality horizon, `m_P = √Ω`, the dimensionless coupling of two masses `m` is `(m/m_P)² = m²/Ω`, small because35`Ω` is large. C5's frame covariance is not formal content. -/36theorem dilution (m Ω : ℝ) (hΩ : 0 < Ω) : (m / √Ω) ^ 2 = m ^ 2 / Ω := by37  rw [div_pow, sq_sqrt hΩ.le]3839end register4041/-! ## The strong field (21:C4, C12, C13, P1, P7) -/42section strongfield4344/-- 21:C12, 21:P7 — the operational cut and the slip core in the substrate coordinate (`G = 1`, `M` in Planck45masses, `L = ln Ω`): `r_f = 2M/L` carries `e^{2M/r_f} = Ω` (the round-trip delay's factor); `r_* = √M < r_f`46exactly when `M > (L/2)²`, and `r_f < M` exactly when `L > 2` (master E10). -/47theorem operational_cut (M L Ω : ℝ) (hM : 0 < M) (hL : 0 < L) (hΩ : L = log Ω) (hΩ0 : 0 < Ω) :48    exp (2 * M / (2 * M / L)) = Ω ∧49    (√M < 2 * M / L ↔ (L / 2) ^ 2 < M) ∧ (2 * M / L < M ↔ 2 < L) := by50  refine ⟨?_, ?_, ?_⟩51  · have : 2 * M / (2 * M / L) = L := by field_simp52    rw [this, hΩ, exp_log hΩ0]53  · rw [Real.sqrt_lt' (by positivity), div_pow, lt_div_iff₀ (by positivity)]54    constructor <;> intro h <;> nlinarith55  · rw [div_lt_iff₀ hL]56    constructor <;> intro h <;> nlinarith5758/-- 21:P1 — the photon sphere (`prop:shadow`, `rem:exponential`): the impact parameter `b(r) = r e^{2Gm/r}` of the exponential metric59satisfies `b(r) ≥ 2e·Gm` for every `r > 0`, with equality exactly at `r = 2Gm` (from `x + 1 ≤ eˣ`, strict off60`x = 0`): the photon sphere is at `r_ph = 2Gm`, the critical impact parameter `b_c = 2e·Gm`. -/61theorem photon_sphere (Gm r : ℝ) (hG : 0 < Gm) (hr : 0 < r) :62    2 * exp 1 * Gm ≤ r * exp (2 * Gm / r) ∧ (r * exp (2 * Gm / r) = 2 * exp 1 * Gm ↔ r = 2 * Gm) := by63  have hsplit : exp (2 * Gm / r) = exp 1 * exp (2 * Gm / r - 1) := by64    rw [← exp_add]; ring_nf65  have hx := Real.add_one_le_exp (2 * Gm / r - 1)66  have hkey : 2 * exp 1 * Gm = r * exp 1 * (2 * Gm / r - 1 + 1) := by field_simp; ring67  have hpos : 0 < r * exp 1 := by positivity68  constructor69  · rw [hsplit, hkey]70    calc r * exp 1 * (2 * Gm / r - 1 + 1) ≤ r * exp 1 * exp (2 * Gm / r - 1) :=71          mul_le_mul_of_nonneg_left hx hpos.le72      _ = r * (exp 1 * exp (2 * Gm / r - 1)) := by ring73  · constructor74    · intro h75      by_contra hne76      have hx' : 2 * Gm / r - 1 ≠ 0 := by77        intro h078        apply hne79        have : 2 * Gm / r = 1 := by linarith80        rw [div_eq_one_iff_eq hr.ne'] at this81        linarith82      have hlt := Real.add_one_lt_exp hx'83      have : r * exp 1 * (2 * Gm / r - 1 + 1) < r * exp 1 * exp (2 * Gm / r - 1) :=84        mul_lt_mul_of_pos_left hlt hpos85      rw [hsplit, ← mul_assoc] at h86      linarith87    · rintro rfl88      have : 2 * Gm / (2 * Gm) = 1 := by field_simp89      rw [this]; ring9091/-- `√3` to seven places. -/92theorem sqrt_three_bounds : (1.7320508 : ℝ) < √3 ∧ √3 < 1.7320509 :=93  ⟨(Real.lt_sqrt (by norm_num)).mpr (by norm_num), (Real.sqrt_lt' (by norm_num)).mpr (by norm_num)⟩9495/-- 21:P1 — the shadow and the ringdown against general relativity, bracketed from `e` (nine places) and `√3`:96the critical impact parameters `b_c = 2e·Gm` (this work) and `3√3·Gm` (Schwarzschild) have ratio97`2e/(3√3)` between `1.0462` and `1.0463` (the shadow `+4.6 %`), and the eikonal ringdown frequency, `∝ 1/b_c`,98ratio `3√3/(2e)` between `0.9557` and `0.9558` (`−4.4 %`); the Sgr A* excess `(4e − 6√3) θ_g` at the99GRAVITY `θ_g = 5.12 µas` [data, A8] lies between `2.46` and `2.47 µas` (the `2.5 µas` of the text). -/100theorem shadow_bracket :101    (1.0462 : ℝ) < 2 * exp 1 / (3 * √3) ∧ 2 * exp 1 / (3 * √3) < 1.0463 ∧102    (0.9557 : ℝ) < 3 * √3 / (2 * exp 1) ∧ 3 * √3 / (2 * exp 1) < 0.9558 ∧103    (2.46 : ℝ) < (4 * exp 1 - 6 * √3) * 5.12 ∧ (4 * exp 1 - 6 * √3) * 5.12 < 2.47 := by104  have e1 := Real.exp_one_gt_d9105  have e2 := Real.exp_one_lt_d9106  obtain ⟨s1, s2⟩ := sqrt_three_bounds107  have hs : (0 : ℝ) < √3 := by positivity108  have he : (0 : ℝ) < exp 1 := exp_pos 1109  refine ⟨?_, ?_, ?_, ?_, by nlinarith, by nlinarith⟩110  · rw [lt_div_iff₀ (by positivity)]; nlinarith111  · rw [div_lt_iff₀ (by positivity)]; nlinarith112  · rw [lt_div_iff₀ (by positivity)]; nlinarith113  · rw [div_lt_iff₀ (by positivity)]; nlinarith114115/-- 00:E14 — the eikonal pair of the exponential reading (`G = 1`, `M` the mass): with `h(r) = r² e^{4M/r} = b(r)²` the116square of the impact function, `h′(r) = e^{4M/r}(2r − 4M)` for `r ≠ 0`, zero exactly at `r_c = 2M` (the photon sphere of117`photon_sphere`), and `h″(2M) = 2e²`; the orbital rate squared `Ω_c² = 1/h(2M) = 1/(2eM)²` and the Lyapunov rate squared118`λ² = e^{−4u} h″/(2h)` at `2M` coincide, and the pair is `3√3/(2e)` of Schwarzschild's `1/(3√3 M)` (`shadow_bracket`119brackets that ratio). -/120theorem eikonal_pair (M : ℝ) (hM : 0 < M) :121    (∀ r : ℝ, r ≠ 0 →122      HasDerivAt (fun r : ℝ => r ^ 2 * exp (4 * M / r)) (exp (4 * M / r) * (2 * r - 4 * M)) r) ∧123    (∀ r : ℝ, exp (4 * M / r) * (2 * r - 4 * M) = 0 ↔ r = 2 * M) ∧124    (∀ r : ℝ, r ≠ 0 →125      HasDerivAt (fun r : ℝ => exp (4 * M / r) * (2 * r - 4 * M))126        (exp (4 * M / r) * (2 - 4 * M * (2 * r - 4 * M) / r ^ 2)) r) ∧127    exp (4 * M / (2 * M)) * (2 - 4 * M * (2 * (2 * M) - 4 * M) / (2 * M) ^ 2) = 2 * exp 2 ∧128    (2 * M) ^ 2 * exp (4 * M / (2 * M)) = (2 * exp 1 * M) ^ 2 ∧129    exp (-(4 * M / (2 * M))) * (2 * exp 2) / (2 * ((2 * M) ^ 2 * exp (4 * M / (2 * M)))) =130      (1 / (2 * exp 1 * M)) ^ 2 ∧131    (1 / (2 * exp 1 * M)) / (1 / (3 * √3 * M)) = 3 * √3 / (2 * exp 1) := by132  have hM0 : M ≠ 0 := hM.ne'133  have h42 : 4 * M / (2 * M) = 2 := by field_simp; ring134  have he2 : exp 2 = exp 1 ^ 2 := by135    calc exp 2 = exp (1 + 1) := by norm_num136      _ = exp 1 * exp 1 := Real.exp_add 1 1137      _ = exp 1 ^ 2 := by ring138  have hs3 : (0 : ℝ) < √3 := Real.sqrt_pos.mpr (by norm_num)139  -- the derivative of the exponent 4M/r140  have hinner : ∀ r : ℝ, r ≠ 0 → HasDerivAt (fun r : ℝ => 4 * M / r) (-(4 * M) / r ^ 2) r := by141    intro r hr142    have := (hasDerivAt_inv hr).const_mul (4 * M)143    refine this.congr_deriv ?_ |>.congr_of_eventuallyEq (Filter.Eventually.of_forall fun y => ?_)144    · field_simp145    · simp [div_eq_mul_inv]146  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩147  · intro r hr148    have hexp := (hinner r hr).exp149    have := (hasDerivAt_pow 2 r).mul hexp150    refine this.congr_deriv ?_151    field_simp152    ring153  · intro r154    constructor155    · intro h156      rcases mul_eq_zero.mp h with h | h157      · exact absurd h (Real.exp_pos _).ne'158      · linarith159    · intro h; subst h; ring160  · intro r hr161    have hexp := (hinner r hr).exp162    have hlin : HasDerivAt (fun r : ℝ => 2 * r - 4 * M) 2 r := by163      simpa using ((hasDerivAt_id r).const_mul (2 : ℝ)).sub_const (4 * M)164    have := hexp.mul hlin165    refine this.congr_deriv ?_166    field_simp167    ring168  · rw [h42]; field_simp; ring169  · rw [h42, he2]; ring170  · have h1 : exp 1 ≠ 0 := (Real.exp_pos 1).ne'171    rw [h42, Real.exp_neg, he2]172    field_simp173  · have h1 : exp 1 ≠ 0 := (Real.exp_pos 1).ne'174    field_simp175176/-- 21:P1 — the innermost stable circular orbit of the exponential metric (`G = m = 1`, isotropic radius),177with the circular-orbit relations of the paper's `prop:isco` taken as given and not formalised178(`L² = e^{2/r} r²/(r − 2)` and `E² = e^{−2/r}(r − 1)/(r − 2)` for a circular orbit at `r > 2`): what is179proved is that `log L²` has derivative `(r² − 6r + 4)/(r²(r − 2))`, that `r_ISCO = 3 + √5` is the root of180`r² − 6r + 4` above `2`, and that `(r − 1)/(r − 2) = r/4` there, so `E² = e^{−2/r} r/4` at the orbit. -/181theorem isco (r : ℝ) (hr : 2 < r) :182    HasDerivAt (fun r : ℝ => 2 / r + 2 * log r - log (r - 2))183      ((r ^ 2 - 6 * r + 4) / (r ^ 2 * (r - 2))) r ∧184    (3 + √5) ^ 2 - 6 * (3 + √5) + 4 = 0 ∧ 2 < 3 + √5 ∧185    (3 + √5 - 1) / (3 + √5 - 2) = (3 + √5) / 4 := by186  have h5 := Real.sq_sqrt (show (0 : ℝ) ≤ 5 by norm_num)187  have hs5 : (0 : ℝ) < √5 := by positivity188  refine ⟨?_, by linear_combination h5, by linarith, ?_⟩189  · have hr0 : r ≠ 0 := by linarith190    have hr2 : r - 2 ≠ 0 := by linarith191    have d1 : HasDerivAt (fun r : ℝ => 2 / r) (-(2 / r ^ 2)) r := by192      have := (hasDerivAt_inv hr0).const_mul 2193      convert this using 1 <;> [funext x; skip] <;> ring194    have d2 : HasDerivAt (fun r : ℝ => 2 * log r) (2 * r⁻¹) r :=195      (Real.hasDerivAt_log hr0).const_mul 2196    have d3 : HasDerivAt (fun r : ℝ => log (r - 2)) (1 / (r - 2)) r :=197      ((hasDerivAt_id' r).sub_const 2).log hr2198    convert (d1.add d2).sub d3 using 1199    field_simp200    ring201  · rw [div_eq_div_iff (by linarith) (by norm_num)]202    linear_combination -h5203204/-- A bracket of `e^{−x}` from `x₁ < x < x₂`, a lower bound of `e^{x₁}` and an upper bound of `e^{x₂}`. -/205theorem exp_neg_bracket {x x₁ x₂ lo hi : ℝ} (hx₁ : x₁ < x) (hx₂ : x < x₂) (hlo : 0 < lo)206    (h1 : lo < exp x₁) (h2 : exp x₂ < hi) : hi⁻¹ < exp (-x) ∧ exp (-x) < lo⁻¹ := by207  constructor208  · calc hi⁻¹ < (exp x₂)⁻¹ := inv_strictAnti₀ (exp_pos _) h2209      _ = exp (-x₂) := (exp_neg _).symm210      _ < exp (-x) := exp_lt_exp.mpr (by linarith)211  · calc exp (-x) < exp (-x₁) := exp_lt_exp.mpr (by linarith)212      _ = (exp x₁)⁻¹ := exp_neg _213      _ < lo⁻¹ := inv_strictAnti₀ hlo h1214215/-- The Taylor brackets of `e^t` at the two ends of `t = 2/r_ISCO = (3 − √5)/2`. -/216theorem exp_isco_tail_bounds :217    (1.465161 : ℝ) < exp 0.381966 ∧ exp (0.3819661 : ℝ) < 1.465163 := by218  constructor219  · have h := abs_le.1 (Real.exp_bound (x := 0.381966) (by rw [abs_of_pos (by norm_num)]; norm_num)220      (n := 7) (by norm_num))221    rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.381966)] at h222    have h1 := h.1223    norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢224    linarith225  · have h := Real.exp_bound' (x := 0.3819661) (by norm_num) (by norm_num) (n := 7) (by norm_num)226    norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢227    linarith228229/-- `√5` to seven places. -/230theorem sqrt_five_bounds : (2.2360679 : ℝ) < √5 ∧ √5 < 2.2360680 :=231  ⟨(Real.lt_sqrt (by norm_num)).mpr (by norm_num), (Real.sqrt_lt' (by norm_num)).mpr (by norm_num)⟩232233/-- 21:P1 — the accretion efficiency bracketed: at `r_ISCO = 3 + √5` the orbital energy `E = √(e^{−2/r} r/4)`234lies between `0.9452` and `0.9453`, so `1 − E` is between `5.47 %` and `5.48 %` (the text's `5.48 %`),235against Schwarzschild's `1 − √(8/9)` between `5.71 %` and `5.72 %`. -/236theorem isco_efficiency :237    (0.0547 : ℝ) < 1 - √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) ∧238    1 - √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) < 0.0548 ∧239    (0.0571 : ℝ) < 1 - √(8 / 9) ∧ 1 - √(8 / 9) < (0.0572 : ℝ) := by240  obtain ⟨s1, s2⟩ := sqrt_five_bounds241  obtain ⟨t1, t2⟩ := exp_isco_tail_bounds242  have hx : 2 / (3 + √5) = (3 - √5) / 2 := by243    have h5 := Real.sq_sqrt (show (0 : ℝ) ≤ 5 by norm_num)244    rw [div_eq_div_iff (by positivity) (by norm_num)]245    linear_combination h5246  obtain ⟨hlo, hhi⟩ := exp_neg_bracket (x := 2 / (3 + √5)) (x₁ := 0.381966) (x₂ := 0.3819661)247    (by rw [hx]; linarith) (by rw [hx]; linarith) (by norm_num) t1 t2248  norm_num at hlo hhi249  have hE := exp_pos (-(2 / (3 + √5)))250  have hv1 : (0.89341 : ℝ) < exp (-(2 / (3 + √5))) * (3 + √5) / 4 := by nlinarith251  have hv2 : exp (-(2 / (3 + √5))) * (3 + √5) / 4 < (0.89345 : ℝ) := by nlinarith252  have hq1 : (0.9452 : ℝ) < √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) :=253    (Real.lt_sqrt (by norm_num)).mpr (by nlinarith)254  have hq2 : √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) < (0.9453 : ℝ) :=255    (Real.sqrt_lt' (by norm_num)).mpr (by nlinarith)256  have hs1 : (0.9428 : ℝ) < √(8 / 9) := (Real.lt_sqrt (by norm_num)).mpr (by norm_num)257  have hs2 : √(8 / 9 : ℝ) < 0.9429 := (Real.sqrt_lt' (by norm_num)).mpr (by norm_num)258  refine ⟨by linarith, by linarith, by linarith, by linarith⟩259260/-- 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 at261`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 the262externally resolvable capacity scales as `(r_f/r_s)²` is the paper's count, not formal content. -/263theorem capacity_ratio (rs L : ℝ) (hrs : rs ≠ 0) (hL : L ≠ 0) : (rs / L / rs) ^ 2 = 1 / L ^ 2 := by264  field_simp265266theorem capacity_ratio_numeral : (1.24e-5 : ℝ) < 1 / 283.5 ^ 2 ∧ (1 / 283.5 ^ 2 : ℝ) < 1.25e-5 := by267  norm_num268269/-- 21:C4 — the redshift as clock rate: the bias field `e^{−u}` with `u = Gm/rc²` gives270`Δf/f = 1 − e^{−u} = u + O(u²)`, `|1 − e^{−u} − u| ≤ u²` on `0 ≤ u ≤ 1`. -/271theorem redshift_linear (u : ℝ) (h0 : 0 ≤ u) (h1 : u ≤ 1) : |1 - exp (-u) - u| ≤ u ^ 2 := by272  have h := Real.exp_bound (x := -u) (by rw [abs_neg, abs_of_nonneg h0]; exact h1) (n := 2) (by norm_num)273  norm_num [Finset.sum_range_succ, Nat.factorial, abs_neg, abs_of_nonneg h0] at h274  rw [abs_le] at h ⊢275  constructor <;> nlinarith [sq_nonneg u]276277end strongfield278279/-! ## The floor and the crossover (21:C19, P4, X2) -/280section floor281282/-- 21:C19, 21:P4 — the registration root: for `0 < w < 1` the quadratic `wη² − 2η + w = 0` (rational in the283paper's `w`, here over `ℝ`) has284exactly the roots `(1 ∓ √(1 − w²))/w`; the smaller, `η = (1 − √(1 − w²))/w`, lies in `(0, 1)` and the larger285exceeds `1`, so the in-`(0, 1)` root that fixes the resolved fraction `f = 1 − η^a` is unique. -/286theorem registration_root (w : ℝ) (hw0 : 0 < w) (hw1 : w < 1) :287    w * ((1 - √(1 - w ^ 2)) / w) ^ 2 - 2 * ((1 - √(1 - w ^ 2)) / w) + w = 0 ∧288    0 < (1 - √(1 - w ^ 2)) / w ∧ (1 - √(1 - w ^ 2)) / w < 1 ∧289    1 < (1 + √(1 - w ^ 2)) / w ∧290    (∀ x : ℝ, w * x ^ 2 - 2 * x + w = 0 →291      x = (1 - √(1 - w ^ 2)) / w ∨ x = (1 + √(1 - w ^ 2)) / w) := by292  have hw2 : 0 ≤ 1 - w ^ 2 := by nlinarith293  set s := √(1 - w ^ 2) with hs294  have hs2 : s ^ 2 = 1 - w ^ 2 := Real.sq_sqrt hw2295  have hs0 : 0 ≤ s := Real.sqrt_nonneg _296  have hs1 : s < 1 := by297    rw [hs, Real.sqrt_lt' (by norm_num)]; nlinarith298  have hsw : 1 - w < s := by nlinarith [mul_pos hw0 (sub_pos.mpr hw1)]299  have hab : (1 - s) / w + (1 + s) / w = 2 / w := by rw [← add_div]; ring_nf300  have hsum : w * (2 / w) = 2 := by field_simp301  have hprod : w * ((1 - s) / w * ((1 + s) / w)) = w := by302    rw [div_mul_div_comm, ← mul_div_assoc, div_eq_iff (by positivity)]303    linear_combination (-w) * hs2304  have hquad : ∀ x : ℝ, w * x ^ 2 - 2 * x + w = w * (x - (1 - s) / w) * (x - (1 + s) / w) := by305    intro x306    have e : w * (x - (1 - s) / w) * (x - (1 + s) / w)307        = w * x ^ 2 - w * ((1 - s) / w + (1 + s) / w) * x + w * ((1 - s) / w * ((1 + s) / w)) := by ring308    rw [e, hab, hsum, hprod]309  refine ⟨?_, div_pos (by linarith) hw0, ?_, ?_, ?_⟩310  · rw [hquad]; ring311  · rw [div_lt_one hw0]; linarith312  · rw [lt_div_iff₀ hw0]; linarith313  · intro x hx314    rw [hquad] at hx315    rcases mul_eq_zero.mp hx with h | h316    · rcases mul_eq_zero.mp h with h | h317      · exact absurd h hw0.ne'318      · left; linarith319    · right; linarith320321/-- 21:C19, 21:P4 — the crossover `g_obs = g_N/(1 − e^{−√x})`, `x = g_N/a₀`, squeezed: with `t = √x > 0`,322`1 ≤ t/(1 − e^{−t})`, and `t/(1 − e^{−t}) ≤ 1/(1 − 3t/4)` for `t ≤ 1`; and the Tully–Fisher algebra is323exact: `v² = g_obs r` with `g_obs = √(g_N a₀)`, `g_N = GM/r²`, gives `v⁴ = GMa₀`. -/324theorem crossover_limits (t : ℝ) (ht : 0 < t) :325    0 < 1 - exp (-t) ∧ 1 ≤ t / (1 - exp (-t)) ∧326    (t ≤ 1 → t / (1 - exp (-t)) ≤ 1 / (1 - 3 * t / 4)) ∧327    (∀ G M r a₀ v : ℝ, 0 < r → 0 ≤ G * M → 0 ≤ a₀ →328      v ^ 2 = √(G * M / r ^ 2 * a₀) * r → v ^ 4 = G * M * a₀) := by329  have hpos : 0 < 1 - exp (-t) := by330    have : exp (-t) < exp 0 := exp_lt_exp.mpr (by linarith)331    rw [exp_zero] at this332    linarith333  refine ⟨hpos, ?_, ?_, ?_⟩334  · rw [le_div_iff₀ hpos]335    have := Real.add_one_le_exp (-t)336    linarith337  · intro ht1338    have h := Real.exp_bound (x := -t) (by rw [abs_neg, abs_of_pos ht]; exact ht1) (n := 2) (by norm_num)339    norm_num [Finset.sum_range_succ, Nat.factorial, abs_neg, abs_of_pos ht] at h340    rw [abs_le] at h341    have h34 : 0 < 1 - 3 * t / 4 := by linarith342    rw [div_le_div_iff₀ hpos h34]343    nlinarith344  · intro G M r a₀ v hr hGM ha v2345    have hnn : 0 ≤ G * M / r ^ 2 * a₀ := by positivity346    calc v ^ 4 = (v ^ 2) ^ 2 := by ring347      _ = (√(G * M / r ^ 2 * a₀)) ^ 2 * r ^ 2 := by rw [v2]; ring348      _ = G * M / r ^ 2 * a₀ * r ^ 2 := by rw [Real.sq_sqrt hnn]349      _ = G * M * a₀ := by field_simp350351/-- 21:C19, 21:P4, 21:X2 — the deep limit: `t/(1 − e^{−t}) → 1` as `t → 0⁺`, so `g_obs/√(g_N a₀) → 1` — the352deep regime `g_obs = √(g_N a₀)`, the floor read as noise with no dark sector. -/353theorem crossover_deep_limit :354    Filter.Tendsto (fun t : ℝ => t / (1 - exp (-t))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) := by355  have hc : ContinuousAt (fun t : ℝ => 1 / (1 - 3 * t / 4)) 0 := by356    apply ContinuousAt.div continuousAt_const357    · fun_prop358    · norm_num359  have hup : Filter.Tendsto (fun t : ℝ => 1 / (1 - 3 * t / 4)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) := by360    have := hc.tendsto.mono_left (nhdsWithin_le_nhds : nhdsWithin (0 : ℝ) (Set.Ioi 0) ≤ nhds 0)361    simpa using this362  refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hup ?_ ?_363  · filter_upwards [self_mem_nhdsWithin] with t ht364    exact (crossover_limits t ht).2.1365  · filter_upwards [Ioo_mem_nhdsGT (show (0 : ℝ) < 1 by norm_num)] with t ht366    exact (crossover_limits t ht.1).2.2.1 ht.2.le367368/-- 21:C19, 21:P4 — the Newtonian limit: `1 − e^{−t} → 1` as `t → ∞`, so `g_obs/g_N → 1` for `x → ∞`. -/369theorem crossover_newton_limit :370    Filter.Tendsto (fun t : ℝ => 1 - exp (-t)) Filter.atTop (nhds 1) := by371  have := Real.tendsto_exp_neg_atTop_nhds_zero372  simpa using tendsto_const_nhds.sub this373374/-- The Taylor brackets of `e^t` at the two ends of `t = √5 − 2`. -/375theorem exp_root_five_tail_bounds :376    (1.2662602 : ℝ) < exp 0.2360679 ∧ exp (0.2360680 : ℝ) < 1.2662605 := by377  constructor378  · have h := abs_le.1 (Real.exp_bound (x := 0.2360679) (by rw [abs_of_pos (by norm_num)]; norm_num)379      (n := 7) (by norm_num))380    rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.2360679)] at h381    have h1 := h.1382    norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢383    linarith384  · have h := Real.exp_bound' (x := 0.2360680) (by norm_num) (by norm_num) (n := 7) (by norm_num)385    norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢386    linarith387388/-- 21:P4 — the discriminant against the simple interpolant at `g_N = 5a₀`: the crossover389`ν(5) = 1/(1 − e^{−√5})` lies between `1.11966` and `1.11967`, the simple interpolant390`ν_s(5) = 1/2 + √(1/4 + 1/5)` between `1.17082` and `1.17083`, so they part by between `0.0511` and `0.0512` in391`g_obs/g_N` (the text's `0.05`). -/392theorem interpolant_discriminant :393    (1.11966 : ℝ) < 1 / (1 - exp (-√5)) ∧ 1 / (1 - exp (-√5)) < 1.11967 ∧394    (1.17082 : ℝ) < 1 / 2 + √(1 / 4 + 1 / 5) ∧ 1 / 2 + √(1 / 4 + 1 / 5) < 1.17083 ∧395    (0.0511 : ℝ) < (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) ∧396    (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) < 0.0512 := by397  obtain ⟨s1, s2⟩ := sqrt_five_bounds398  obtain ⟨t1, t2⟩ := exp_root_five_tail_bounds399  have hm1 := Real.exp_neg_one_gt_d9400  have hm2 := Real.exp_neg_one_lt_d9401  have hsplit : exp (-√5) = exp (-1) * exp (-1) * exp (2 - √5) := by402    rw [← exp_add, ← exp_add]; ring_nf403  obtain ⟨hlo, hhi⟩ := exp_neg_bracket (x := √5 - 2) (x₁ := 0.2360679) (x₂ := 0.2360680)404    (by linarith) (by linarith) (by norm_num) t1 t2405  norm_num at hlo hhi406  have hm : (0 : ℝ) < exp (-1) := exp_pos _407  have hq1 : (0.106877 : ℝ) < exp (-√5) := by rw [hsplit]; nlinarith [mul_pos hm hm]408  have hq2 : exp (-√5) < (0.106878 : ℝ) := by rw [hsplit]; nlinarith [mul_pos hm hm]409  have hden : (0 : ℝ) < 1 - exp (-√5) := by linarith410  have hr1 : (1.11966 : ℝ) < 1 / (1 - exp (-√5)) := by rw [lt_div_iff₀ hden]; linarith411  have hr2 : 1 / (1 - exp (-√5)) < (1.11967 : ℝ) := by rw [div_lt_iff₀ hden]; linarith412  have hs1 : (0.67082 : ℝ) < √(1 / 4 + 1 / 5) := (Real.lt_sqrt (by norm_num)).mpr (by norm_num)413  have hs2 : √(1 / 4 + 1 / 5 : ℝ) < 0.67083 := (Real.sqrt_lt' (by norm_num)).mpr (by norm_num)414  refine ⟨hr1, hr2, by linarith, by linarith, by linarith, by linarith⟩415416end floor417418/-! ## The primordial fixed point (21:C18) -/419section primordial420421/-- 21:C18 — the fixed point: for a power law `P(k) = k^n` the dimensionless `k³P(k)` is the422same at every scale `k > 0` exactly when `n = −3`, i.e. `n_s − 1 = n + 3 = 0`, the Harrison–Zel'dovich423`n_s = 1`, uniquely; that the drive's jitter spectrum is this fixed point is the paper's argument. -/424theorem scale_invariance_iff (n : ℝ) :425    (∀ k : ℝ, 0 < k → k ^ 3 * k ^ n = 1) ↔ n = -3 := by426  constructor427  · intro h428    have h2 := h 2 (by norm_num)429    have h3 : (2 : ℝ) ^ (n + 3) = 1 := by430      rw [rpow_add (by norm_num : (0 : ℝ) < 2), show (2 : ℝ) ^ (3 : ℝ) = 2 ^ (3 : ℕ) by431        exact_mod_cast rpow_natCast 2 3]432      linarith433    have hl := congrArg Real.log h3434    rw [Real.log_rpow (by norm_num), Real.log_one] at hl435    rcases mul_eq_zero.mp hl with h | h436    · linarith437    · exact absurd h (Real.log_pos (by norm_num)).ne'438  · rintro rfl k hk439    rw [Real.rpow_neg hk.le, show (3 : ℝ) = (3 : ℕ) by norm_num, rpow_natCast]440    exact mul_inv_cancel₀ (pow_ne_zero 3 hk.ne')441442end primordial443444/-! ## The dispersion symbol and the locked sum (21:C1, C15) -/445section lattice446447/-- 21:C15 — the dispersion symbol: the central second difference acts on the plane wave448`e^{ikx}` by `−(2 − 2 cos k) = −4 sin²(k/2)`; the wave equation, its two polarisations and the speed `c` are449the package's. -/450theorem dispersion_symbol (k : ℝ) : 2 - 2 * cos k = 4 * sin (k / 2) ^ 2 := by451  have h := Real.cos_two_mul (k / 2)452  rw [show 2 * (k / 2) = k by ring] at h453  rw [h, Real.cos_sq']; ring454455/-- 21:C1 — the coherent coefficient: a locked cluster of `m` cells with one phase sums with456coefficient exactly `m`, `‖Σ_{j<m} z‖ = m ‖z‖`; the incoherent `O(√m)` and the gradient flow are not formal457content. -/458theorem locked_sum (m : ℕ) (z : ℂ) : ‖∑ _j : Fin m, z‖ = m * ‖z‖ := by459  simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin]460461end lattice462463/-! ## The series (21:C8, C10, C11, P2, P6) -/464section series465466/-- 21:C11 — the exponential reading is the multiplicative one, `e^{−(a+b)} = e^{−a} e^{−b}`; the isotropic467Schwarzschild factor `R(U) = (1 − U/2)/(1 + U/2)` is `e^{−2 artanh(U/2)}`, the exponential reading of the468self-sourced `ψ = 2 artanh(U/2)`, and it violates the composition law: `R(1) = 1/3 ≠ 9/25 = R(1/2)²`. -/469theorem exponential_reading (a b : ℝ) :470    exp (-(a + b)) = exp (-a) * exp (-b) ∧471    (∀ U : ℝ, -2 < U → U < 2 → exp (-(2 * artanh (U / 2))) = (1 - U / 2) / (1 + U / 2)) ∧472    (1 - (1 : ℝ) / 2) / (1 + 1 / 2) ≠ ((1 - (1 / 2 : ℝ) / 2) / (1 + (1 / 2) / 2)) ^ 2 := by473  refine ⟨by rw [← exp_add]; ring_nf, ?_, by norm_num⟩474  intro U h1 h2475  have hx : U / 2 ∈ Set.Icc (-1 : ℝ) 1 := ⟨by linarith, by linarith⟩476  rw [Real.artanh_eq_half_log hx]477  have hpos : 0 < (1 + U / 2) / (1 - U / 2) := by apply div_pos <;> linarith478  rw [show -(2 * (1 / 2 * log ((1 + U / 2) / (1 - U / 2)))) = -log ((1 + U / 2) / (1 - U / 2)) by ring,479    exp_neg, exp_log hpos, inv_div]480481/-- 21:C8, 21:P6, 21:C7 — the post-Newtonian inputs as Taylor brackets on `|U| ≤ 1/2`: the exponential metric's482`A = e^{−2U}`, `B = e^{2U}` against the isotropic Schwarzschild `A_S = ((1 − U/2)/(1 + U/2))²`,483`B_S = (1 + U/2)⁴` satisfy `|A − A_S − U³/6| ≤ 3U⁴` and `|B − B_S − U²/2| ≤ 3|U|³`: the single-potential484inputs consumed by C23 coincide through first post-Newtonian order (`A` to `O(U²)`, `B` to `O(U)`) and part at4852PN with `δA = U³/6`, `δB = U²/2`; the two-body superposition of C23 is the package's. -/486theorem pn_series (U : ℝ) (hU : |U| ≤ 1 / 2) :487    |exp (-(2 * U)) - ((1 - U / 2) / (1 + U / 2)) ^ 2 - U ^ 3 / 6| ≤ 3 * U ^ 4 ∧488    |exp (2 * U) - (1 + U / 2) ^ 4 - U ^ 2 / 2| ≤ 3 * |U| ^ 3 := by489  have hU' := abs_le.1 hU490  have hden : 1 + U / 2 ≠ 0 := by intro h; linarith [hU'.1]491  have hden2 : (9 / 16 : ℝ) ≤ (1 + U / 2) ^ 2 := by nlinarith [hU'.1]492  have hU4 : 0 ≤ U ^ 4 := by positivity493  have habs4 : |U| ^ 4 = U ^ 4 := by rw [← abs_pow, abs_of_nonneg hU4]494  have habs3 : |U| ^ 3 * |U| = U ^ 4 := by495    rw [← pow_succ, ← abs_pow, abs_of_nonneg (by positivity)]496  have hU3 : 0 ≤ |U| ^ 3 := by positivity497  constructor498  · have h := Real.exp_bound (x := -(2 * U)) (by rw [abs_neg, abs_mul, abs_two]; linarith) (n := 4)499      (by norm_num)500    rw [abs_neg, abs_mul, abs_two] at h501    norm_num [Finset.sum_range_succ, Nat.factorial] at h502    rw [abs_le] at h503    have hpow : (2 * |U|) ^ 4 = 16 * U ^ 4 := by rw [mul_pow, habs4]; norm_num504    rw [hpow] at h505    have hA : ((1 - U / 2) / (1 + U / 2)) ^ 2 - (1 - 2 * U + 2 * U ^ 2 - 3 / 2 * U ^ 3)506        = U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2 := by507      rw [div_pow, eq_div_iff (pow_ne_zero 2 hden), sub_mul, div_mul_cancel₀ _ (pow_ne_zero 2 hden)]508      ring509    have hrem : |U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2| ≤ 2.12 * U ^ 4 := by510      rw [abs_div, abs_mul, abs_of_nonneg hU4, abs_of_pos (by positivity : (0 : ℝ) < (1 + U / 2) ^ 2),511        div_le_iff₀ (by positivity)]512      have : |1 + 3 * U / 8| ≤ 1.1875 := by rw [abs_le]; constructor <;> linarith [hU'.1, hU'.2]513      nlinarith [abs_nonneg (1 + 3 * U / 8)]514    rw [abs_le] at hrem515    have hA' : ((1 - U / 2) / (1 + U / 2)) ^ 2516        = 1 - 2 * U + 2 * U ^ 2 - 3 / 2 * U ^ 3 + U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2 := by517      linarith [hA]518    rw [hA', abs_le]519    constructor <;> nlinarith [hrem.1, hrem.2, h.1, h.2]520  · have h := Real.exp_bound (x := 2 * U) (by rw [abs_mul, abs_two]; linarith) (n := 3) (by norm_num)521    rw [abs_mul, abs_two] at h522    norm_num [Finset.sum_range_succ, Nat.factorial] at h523    rw [abs_le] at h ⊢524    have hpow : (2 * |U|) ^ 3 = 8 * |U| ^ 3 := by rw [mul_pow]; norm_num525    rw [hpow] at h526    have hU4' : U ^ 4 ≤ |U| ^ 3 / 2 := by rw [← habs3]; nlinarith527    have hcube : U ^ 3 ≤ |U| ^ 3 ∧ -(|U| ^ 3) ≤ U ^ 3 := by528      constructor529      · calc U ^ 3 ≤ |U ^ 3| := le_abs_self _530          _ = |U| ^ 3 := abs_pow U 3531      · calc -(|U| ^ 3) = -|U ^ 3| := by rw [abs_pow]532          _ ≤ U ^ 3 := neg_abs_le _533    constructor <;> nlinarith [h.1, h.2, hcube.1, hcube.2]534535/-- 21:P2, 21:C10 — the numeral behind the preferred-frame scale: the drive's signature is `O(1/√Ω)` (the paper's536`α₁, α₂`), and at the scale import's `Ω = 1.3 × 10¹²³` (00:A7) this lies between `2.7` and `2.8 × 10⁻⁶²` (the row's537`3 × 10⁻⁶²`). -/538theorem preferred_frame_scale : (2.7e-62 : ℝ) < 1 / √(1.3e123) ∧ 1 / √(1.3e123) < 2.8e-62 := by539  have hs : 0 < √(1.3e123 : ℝ) := Real.sqrt_pos.2 (by norm_num)540  constructor541  · rw [lt_one_div (by norm_num) hs, Real.sqrt_lt' (by norm_num)]; norm_num542  · rw [one_div_lt hs (by norm_num), Real.lt_sqrt (by norm_num)]; norm_num543544end series545546end FRC.Strong547