The Lean module lean/FrcLedger/Entropy.lean of the paper 14-entr (on Mathlib): 82 theorems (2 definitions): 0 with no axioms, 8 at tier 1 (propext, Quot.sound), 74 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (violet, Mathlib; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import Mathlib2import FrcLedger.Theme.Chart3import FrcLedger.Keys.Chart45/-!6# 14-entropy — the de Sitter import, the octant and the age–rate locus: the ledger predicates in Lean (2026-09-19)78Rows of the predicate ledger of *De Sitter Entropy Estimates over Finite Holographic Substrate* (tree9`14-entropy-20260722`). The import and its congruences: `Ω = 4S + 1` fixes `S = (Ω − 1)/4` and `4 ∣ Ω − 1`10(A1); on every Carrier the quarter-turn `i² = −1` exists — the generative four of the quarter identity11`4S = Ω − 1`, the area law's chart face `4π n_A = 4S` (B9); the triality centre `3 ∣ Ω + 1` with no element of12order three on the Carrier, the c-square `2` a square exactly when `S` is even, and the laboratory Carrier13`2 408 561` decided (A2). The angle–count dictionary `2π ↔ 4S`, `π/4 ↔ S/2`, the octant's chart conversion14`(S/2)/(4S) · 2π r_H/c = (π/4) r_H/c` and Milgrom's rebooking `cH/2π = cHħ/h` (B2, C5, X2); the octant sector:15`8 ∣ 4S ⟺ S` even, the closure budget `2x ≤ S ⟺ x ≤ S/2`, the character of order eight with `ζ⁴ = −1` and the16Tsirelson square `(2(ζ + ζ⁻¹))² = 8`, the sector realised on every Carrier exactly when `S` is even, and the17c-square congruence as the sector's second face (C5, C6, X4); the horizon-quarter closure (C2). The rival18chart's age identity `t₀H_Λ = (2/3) artanh √Ω_Λ` taken as the import it is, verified against the chart's own19Friedmann equation (the standard closed form `(Ω_m/Ω_Λ)^{1/3} sinh^{2/3}(3H_Λ t/2)` solves20`(ȧ/a)² = H₀²(Ω_m a⁻³ + Ω_Λ)` with `a(0) = 0`, expanding, and in the flat case `Ω_m + Ω_Λ = 1` reaches `1`21exactly at `t H_Λ = (2/3) artanh √Ω_Λ`, with rate `H₀` there; that it is the unique such solution is not22formalised), its numeral at the fitted `0.685` bracketed, and its inversion: `π/4` is reached at23`Ω_Λ = tanh²(3π/8)` and, on `[0, 1)`, only there (A8, C3, C7, X3); the age–rate locus24`t H₀ = (π/4)/tanh(3π/8)`, the channel-1 consistency and the two-cluster chart identity (P3, C8, C4); the25effective-fluid reading `w = −1` (B8, P4); the count face and its chart dress `√(S/π)` (C9); the capacity axis —26`κ = 2` has no shell, hydrogen at `κ = 3`, the `3N` shell exactly when `12N + 1` is prime and none at `N = 2`,27the nesting bound `q⁴ < Ω` with `N ≤ 3` on the laboratory Carrier (C10, B10). Classical (tier 2) on Mathlib's28hierarchy; the finite content — the congruences, the octant on every framed shell, the Carrier and the nesting29decided by the kernel — is proved with no axioms in `FrcCore/Entropy.lean`. Since the ledger migration (task LM30) the30octant's chart theorems — the conversion, the brackets of `tanh(3π/8)`, the landing and the locus — live in the31chart theme, `FrcLedger/Theme/Chart.lean`, as `FRC.Chart.*`; the old names below are aliases. What is outside both modules: the32realisation premises of the octant lemma (A4 reciprocity, A5 the equatorial horizon, B6 the closure budget, B733the depth rule) — the modules decide the lemma's arithmetic, clause (iv) and the closure count, not its34realisation content; and the chart identities marked [chart] or [ΛCDM] below are identities of the continuum35reading, with no finite content of their own.36-/3738namespace FRC.Entropy3940open Real4142/-! ## The import and its congruences (14:A1, A2, B9) -/43section carrier4445/-- 14:A1, 14:B9 — the arithmetic behind the import: `Ω = 4S + 1` gives `S = (Ω − 1)/4`, `4 ∣ Ω − 1` and46`Ω ≡ 1 (mod 4)`; the quarter identity `4S = Ω − 1` is exact, the finite face of B9's area law `A = 4S`. -/47
theorem cardinality {Ω S : ℕ} (h : Ω = 4 * S + 1) :48 S = (Ω - 1) / 4 ∧ 4 ∣ Ω - 1 ∧ Ω % 4 = 1 ∧ 4 * S = Ω - 1 := by49 subst h; refine ⟨by omega, ⟨S, by omega⟩, by omega, by omega⟩5051/-- In any field of characteristic `≠ 2`, a root of `i² = −1` has `i⁴ = 1` and is neither `1` nor `−1`. -/52theorem quarter_turn_of_sq {K : Type*} [Field K] (i : K) (h2 : (2 : K) ≠ 0) (hi : i ^ 2 = -1) :53 i ^ 4 = 1 ∧ i ≠ 1 ∧ i ≠ -1 := by54 refine ⟨?_, ?_, ?_⟩55 · calc i ^ 4 = (i ^ 2) ^ 2 := by ring56 _ = 1 := by rw [hi]; ring57 · rintro rfl; apply h2; linear_combination hi58 · rintro rfl; apply h2; linear_combination hi5960/-- 14:B9 — the arithmetic precondition of the reading (the quarter-turn rows 1:B3, 2:D2 at Carrier scale): on61every Carrier `Ω = 4S + 1` prime, `−1` is a square, so a quarter-turn `i` with `i² = −1`, `i⁴ = 1`, `i ≠ ±1`62exists in `𝔽_Ω`. That the Bekenstein–Hawking quarter `S = A/4` is this quarter-turn read on the area face is63B9's realisation clause, not formal content. -/64theorem quarter_turn (S : ℕ) [hp : Fact (Nat.Prime (4 * S + 1))] :65 IsSquare (-1 : ZMod (4 * S + 1)) ∧66 ∃ i : ZMod (4 * S + 1), i ^ 2 = -1 ∧ i ^ 4 = 1 ∧ i ≠ 1 ∧ i ≠ -1 := by67 have hsq : IsSquare (-1 : ZMod (4 * S + 1)) :=68 (ZMod.exists_sq_eq_neg_one_iff (p := 4 * S + 1)).2 (by omega)69 refine ⟨hsq, ?_⟩70 obtain ⟨i, hi⟩ := hsq71 have h2 : (2 : ZMod (4 * S + 1)) ≠ 0 := by72 intro h73 have := (ZMod.natCast_eq_zero_iff 2 (4 * S + 1)).1 (by exact_mod_cast h)74 have h5 : 5 ≤ 4 * S + 1 := by75 have := hp.out.two_le76 have h1 : 4 * S + 1 ≠ 4 := by omega77 have h3 : 4 * S + 1 ≠ 3 := by omega78 have h4 : 4 * S + 1 ≠ 2 := by omega79 omega80 exact absurd (Nat.le_of_dvd (by norm_num) this) (by omega)81 have hi2 : i ^ 2 = -1 := by rw [sq, ← hi]82 exact ⟨i, hi2, quarter_turn_of_sq i h2 hi2⟩8384/-- 14:B9 [chart] — the area law's chart face: with `n_A = S/π` Planck cells in the projected horizon,85`4π n_A = 4S`, the full phase cycle; a chart identity with no finite content (the finite face is86`cardinality`). -/87theorem area_law_chart (S : ℝ) : 4 * π * (S / π) = 4 * S := by88 have := Real.pi_ne_zero89 field_simp9091/-- 14:A2 — the arithmetic behind the triality centre: `S ≡ 1 (mod 3)` gives `3 ∣ Ω + 1` and `3 ∤ Ω − 1 = 4S`,92so the Carrier `𝔽_Ω` carries no element of order three in its unit group (that the centre lives in the93quadratic extension, `C₃ ⊂ C_{Ω+1}`, is the corpus's gloss, not proved here). -/94theorem triality_centre (S : ℕ) (h : S % 3 = 1) [Fact (Nat.Prime (4 * S + 1))] :95 3 ∣ 4 * S + 1 + 1 ∧ ¬ 3 ∣ 4 * S ∧ ∀ x : (ZMod (4 * S + 1))ˣ, orderOf x ≠ 3 := by96 refine ⟨⟨(4 * S + 2) / 3, by omega⟩, by omega, fun x hx => ?_⟩97 have hd := orderOf_dvd_card (x := x)98 rw [ZMod.card_units, hx] at hd99 omega100101/-- 14:A2 — the relation behind the c-square (upstream 2-geometry; Mathlib's quadratic-reciprocity102supplement): on a Carrier `Ω = 4S + 1` prime, `2` is a square in `𝔽_Ω` — equivalently `2⁻¹`, the residue `c²`103of the constants correspondence — exactly when `S` is even (`Ω ≡ 1 (mod 8)`). -/104theorem c_square (S : ℕ) [hp : Fact (Nat.Prime (4 * S + 1))] :105 (IsSquare (2 : ZMod (4 * S + 1)) ↔ Even S) ∧ (IsSquare (2⁻¹ : ZMod (4 * S + 1)) ↔ Even S) := by106 have hne : 4 * S + 1 ≠ 2 := by omega107 have h2 : (IsSquare (2 : ZMod (4 * S + 1)) ↔ Even S) := by108 rw [ZMod.exists_sq_eq_two_iff hne, Nat.even_iff]; omega109 refine ⟨h2, ?_⟩110 rw [← h2]111 have h2z : (2 : ZMod (4 * S + 1)) ≠ 0 := by112 intro h113 have := (ZMod.natCast_eq_zero_iff 2 (4 * S + 1)).1 (by exact_mod_cast h)114 have := Nat.le_of_dvd (by norm_num) this115 have := hp.out.two_le116 omega117 constructor118 · rintro ⟨r, hr⟩119 exact ⟨r⁻¹, by rw [← mul_inv, ← hr, inv_inv]⟩120 · rintro ⟨r, hr⟩121 exact ⟨r⁻¹, by rw [← mul_inv, ← hr]⟩122123/-- 14:A2 — the laboratory Carrier `Ω = 2 408 561`, `S = 602 140`: the three congruences as host-decided124values — `S` even, `S ≡ 1 (mod 3)`, `4S + 1` prime. -/125theorem carrierLab :126 4 * 602140 + 1 = 2408561 ∧ Even 602140 ∧ 602140 % 3 = 1 ∧ Nat.Prime 2408561 :=127 ⟨by norm_num, by decide, by norm_num, by norm_num⟩128129/-- 14:C2 [chart] — the horizon-quarter closure is a consistency loop: the shell entropy `S(p) = (p² − 1)/4`130read at the coherence-horizon point `p² = Ω` returns `(Ω − 1)/4 = S`, the import itself. No shell has `p² = Ω`131(`Ω` is prime); the closure is read at the chart point `√Ω`. -/132theorem horizon_quarter_closure (Ω S : ℕ) (p : ℝ) (hΩ : Ω = 4 * S + 1) (hp : p ^ 2 = Ω) :133 (p ^ 2 - 1) / 4 = S := by134 rw [hp, hΩ]; push_cast; ring135136end carrier137138/-! ## The angle–count dictionary (14:B2, C5, X2) -/139section dictionary140141/-- 14:B2 [chart] — the angle–count dictionary: with the full cycle `2π ↔ 4S`, an angle `θ` is the chart face142of the count `θ/(2π) · 4S`: `π ↔ 2S`, `π/2 ↔ S`, `π/4 ↔ S/2` chronons; the count face is143`FRC.Entropy.octant_count` in the core. -/144theorem dictionary (S : ℝ) :145 π / (2 * π) * (4 * S) = 2 * S ∧ (π / 2) / (2 * π) * (4 * S) = S ∧146 (π / 4) / (2 * π) * (4 * S) = S / 2 := by147 have := Real.pi_ne_zero148 refine ⟨?_, ?_, ?_⟩ <;> field_simp <;> ring149150/-- 14:X2 [chart] — Milgrom's rebooking, the substitution `h = 2πħ`: the floor `a₀ = cH/2π` is `cHħ/h`, the151per-cycle rate budget per step. That the `2π` carries zero freedom is X2's realisation clause (B2 fixes the152convention), not formal content. -/153theorem milgrom_rebooking (c H ħ h : ℝ) (hh : h = 2 * π * ħ) (hħ : ħ ≠ 0) :154 c * H / (2 * π) = c * H * ħ / h := by155 subst hh; have := Real.pi_ne_zero; field_simp156157end dictionary158159/-! ## The octant sector (14:C5, C6, X4) -/160section octant161162/-- 14:C6, 14:X4 — the arithmetic face: the octant sector `C₈ ⊂ C_{4S}` exists exactly when `8 ∣ 4S`, that is163when `S` is even (X4's claim about what certifies the congruence is a realisation clause, not this164equivalence). -/165theorem octant_sector_iff (S : ℕ) : 8 ∣ 4 * S ↔ Even S := by166 rw [Nat.even_iff, Nat.dvd_iff_mod_eq_zero]; omega167168/-- 14:C5, 14:B6 — the closure count, clauses (iii)–(iv): given B6's accounting (a two-way registration of169depth `x` costs `2x` of the one-way budget `S`; the realisation, not formalised), the closable depths are exactly170`x ≤ S/2`, and on a Carrier with `S` even the octant count `S/2` closes the budget, `2 · (S/2) = S`. -/171theorem closure_budget (S : ℕ) :172 (∀ x, 2 * x ≤ S ↔ x ≤ S / 2) ∧ (Even S → 2 * (S / 2) = S) := by173 refine ⟨fun x => by omega, fun hS => ?_⟩174 rw [Nat.even_iff] at hS; omega175176/-- 14:C6 — the octant character: in any field an element `ζ` of order eight (`ζ⁸ = 1`, `ζ⁴ ≠ 1`) has177`ζ⁴ = −1`, and the residue the Tsirelson identity carries has square `(ζ + ζ⁻¹)² = 2`, `(2(ζ + ζ⁻¹))² = 8`. -/178theorem octant_character {K : Type*} [Field K] (ζ : K) (h8 : ζ ^ 8 = 1) (h4 : ζ ^ 4 ≠ 1) :179 ζ ^ 4 = -1 ∧ (ζ + ζ⁻¹) ^ 2 = 2 ∧ (2 * (ζ + ζ⁻¹)) ^ 2 = 8 := by180 have hz : ζ ≠ 0 := by rintro rfl; simp at h8181 have hsq : ζ ^ 4 * ζ ^ 4 = 1 := by rw [← pow_add]; exact h8182 have h4' : ζ ^ 4 = -1 := by183 rcases mul_self_eq_one_iff.1 hsq with h | h184 · exact absurd h h4185 · exact h186 refine ⟨h4', ?_, ?_⟩187 · field_simp; linear_combination h4'188 · field_simp; linear_combination 4 * h4'189190/-- 14:C6, 14:X4 — on every Carrier `Ω = 4S + 1` prime the octant sector is realised exactly when `S` is even:191the unit group of `𝔽_Ω` has an element of order eight iff `8 ∣ 4S`. -/192theorem octant_exists_iff (S : ℕ) [Fact (Nat.Prime (4 * S + 1))] :193 (∃ ζ : (ZMod (4 * S + 1))ˣ, orderOf ζ = 8) ↔ Even S := by194 rw [← octant_sector_iff]195 constructor196 · rintro ⟨ζ, hζ⟩197 have hd := orderOf_dvd_card (x := ζ)198 rwa [ZMod.card_units, hζ, Nat.add_sub_cancel] at hd199 · intro h8200 obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := (ZMod (4 * S + 1))ˣ)201 rw [Nat.card_eq_fintype_card, ZMod.card_units, Nat.add_sub_cancel] at hg202 refine ⟨g ^ (orderOf g / 8), orderOf_pow_orderOf_div ?_ ?_⟩203 · rw [hg]; have := (Fact.out : Nat.Prime (4 * S + 1)).two_le; omega204 · rw [hg]; exact h8205206/-- 14:X4 — the arithmetic face of the second face: the c-square (`2` a square in `𝔽_Ω`) holds exactly when207the octant sector exists — the two congruence faces coincide on every Carrier. The reading of the octant as208the well-definedness of the measured age is X4's realisation clause, not formal content. -/209theorem octant_second_face (S : ℕ) [Fact (Nat.Prime (4 * S + 1))] :210 IsSquare (2 : ZMod (4 * S + 1)) ↔ ∃ ζ : (ZMod (4 * S + 1))ˣ, orderOf ζ = 8 := by211 rw [(c_square S).1, octant_exists_iff]212213end octant214215/-! ## The rival chart's age identity and the locus (14:C3, C7, C8, P3, C4, B8) -/216section age217218/-- 14:A8 [ΛCDM], consumed by 14:C3 — the rival chart's age identity as the import it is: in flat219matter-plus-`Λ` the product of the age and the asymptotic rate is `t₀H_Λ = (2/3) artanh √Ω_Λ`. Moved to the chart220theme (`FRC.Chart.lcdmAge`, 7 October 2026); this name is its alias. It is verified against the chart's own Friedmann221equation in `lcdm_age` below. That a landing of it on `π/4` restates the fit is C3's judgment under B5, not formal222content. -/223
noncomputable def lcdmAge (Ω : ℝ) : ℝ := FRC.Chart.lcdmAge Ω224225/-- 14:C7, 14:X3, 14:X6 [ΛCDM] — the octant inversion, moved to the chart theme (`FRC.Chart.octant_inversion`); this name226is its alias. -/227theorem octant_inversion :228 lcdmAge (tanh (3 * π / 8) ^ 2) = π / 4 ∧229 ∀ Ω : ℝ, 0 ≤ Ω → Ω < 1 → lcdmAge Ω = π / 4 → Ω = tanh (3 * π / 8) ^ 2 :=230 FRC.Chart.octant_inversion231232/-- 14:C8 [ΛCDM] — the channel-1 consistency: with `Λ = 3Ω_Λ H₀²/c²` (the definition of `Ω_Λ`) the asymptotic233rate is `H_Λ = c√(Λ/3) = H₀√Ω_Λ`, and the locus read on it, `H_Λ/tanh(3π/8)`, returns `H₀` exactly when234`Ω_Λ = tanh²(3π/8)`; at the fitted `0.685` the return is within `0.1 %` (`channel_one_numeral`). -/235theorem channel_one_consistency (H0 c Ω Λ : ℝ) (hH0 : 0 < H0) (hc : 0 < c) (hΩ : 0 ≤ Ω)236 (hΛ : Λ = 3 * Ω * H0 ^ 2 / c ^ 2) :237 c * √(Λ / 3) = H0 * √Ω ∧ (H0 * √Ω / tanh (3 * π / 8) = H0 ↔ Ω = tanh (3 * π / 8) ^ 2) := by238 have hpos := FRC.Chart.tanh_octant_pos239 constructor240 · rw [hΛ, show 3 * Ω * H0 ^ 2 / c ^ 2 / 3 = Ω * (H0 / c) ^ 2 by field_simp,241 Real.sqrt_mul hΩ, Real.sqrt_sq (by positivity)]242 field_simp243 · constructor244 · intro h245 have h' : √Ω = tanh (3 * π / 8) := by246 field_simp at h247 nlinarith [h]248 rw [← h', Real.sq_sqrt hΩ]249 · intro h250 rw [h, Real.sqrt_sq hpos.le]; field_simp251252/-- 14:C8 [ΛCDM] — the two-cluster chart identity: with `S = π (r_H/ℓ_P)²`, a `Λ`-face reading253`r_H = c/(H₀√Ω_Λ)` against a rate-face reading `r_H = c/H_rate` gives `S_Λ/S_rate = (H_rate/H₀)²/Ω_Λ` — the254definition of `Ω_Λ` read on the rows, the Hubble tension displayed and no framework content. -/255theorem cluster_identity (c H0 Hr Ω ℓ : ℝ) (hc : c ≠ 0) (hΩ : 0 < Ω) (hℓ : ℓ ≠ 0) :256 (π * (c / (H0 * √Ω) / ℓ) ^ 2) / (π * (c / Hr / ℓ) ^ 2) = (Hr / H0) ^ 2 / Ω := by257 have hs : √Ω ≠ 0 := (Real.sqrt_pos.2 hΩ).ne'258 have hpi := Real.pi_ne_zero259 rcases eq_or_ne H0 0 with rfl | hH0260 · simp261 rcases eq_or_ne Hr 0 with rfl | hr262 · simp263 field_simp264 rw [Real.sq_sqrt hΩ.le]265266/-- 14:B8, 14:P4 [ΛCDM] — the arithmetic of the effective-fluid reading: the rival chart's continuity law267`ρ̇ + 3H(ρ + p) = 0` with `ρ̇ = 0` (a fixed cardinality admits no evolution) and `H ≠ 0` gives `p = −ρ`,268`w = p/ρ = −1` exactly. B8's single-component clause and P4's `w₀w_a` rigidity are realisation content, not269formalised. -/270theorem fluid_w (H ρ p ρ' : ℝ) (hH : H ≠ 0) (hρ : ρ ≠ 0) (hρ' : ρ' = 0) (h : ρ' + 3 * H * (ρ + p) = 0) :271 p = -ρ ∧ p / ρ = -1 := by272 subst hρ'273 have hp : p = -ρ := by274 have : ρ + p = 0 := by275 rcases mul_eq_zero.1 (by linarith : 3 * H * (ρ + p) = 0) with h3 | h3276 · exact absurd (by linarith : H = 0) hH277 · exact h3278 linarith279 exact ⟨hp, by rw [hp, neg_div, div_self hρ]⟩280281282/-- 14:C8 — the channel-1 return bracketed: at the fitted `Ω_Λ = 0.685` (A8, taken as data) the locus returns283`H_Λ/tanh(3π/8) = H₀ √0.685/tanh(3π/8)` with `1 < √0.685/tanh(3π/8) < 1.001` — the channel-1 `H₀` to284`0.1 %`. -/285theorem channel_one_numeral :286 (1 : ℝ) < √0.685 / tanh (3 * π / 8) ∧ √0.685 / tanh (3 * π / 8) < 1.001 := by287 obtain ⟨hl, hu⟩ := FRC.Chart.tanh_octant_bounds288 have hpos : (0 : ℝ) < tanh (3 * π / 8) := by linarith289 have hs1 : (0.82764 : ℝ) < √0.685 := by290 rw [Real.lt_sqrt (by norm_num)]; norm_num291 have hs2 : √(0.685 : ℝ) < 0.82765 := by292 rw [Real.sqrt_lt' (by norm_num)]; norm_num293 constructor294 · rw [lt_div_iff₀ hpos]; linarith295 · rw [div_lt_iff₀ hpos]; linarith296297end age298299/-! ## The rival chart's age identity, verified against its own Friedmann equation (14:A8, C3) -/300section friedmann301302/-- 14:A8 [ΛCDM] — the standard flat matter-plus-`Λ` scale factor of the rival chart, for `t ≥ 0`:303`a(t) = (Ω_m/Ω_Λ)^{1/3} sinh^{2/3}(3H_Λ t/2)`, with `H_Λ` the asymptotic rate. -/304noncomputable def lcdmScale (Ωm ΩΛ HΛ t : ℝ) : ℝ :=305 (Ωm / ΩΛ) ^ ((1 : ℝ) / 3) * sinh (3 * HΛ * t / 2) ^ ((2 : ℝ) / 3)306307/-- The cube of the scale factor for `t ≥ 0`: `a³ = (Ω_m/Ω_Λ) sinh²(3H_Λ t/2)`. -/308theorem lcdmScale_cube (Ωm ΩΛ HΛ t : ℝ) (hm : 0 < Ωm) (hΛ : 0 < ΩΛ) (hH : 0 ≤ HΛ) (ht : 0 ≤ t) :309 lcdmScale Ωm ΩΛ HΛ t ^ 3 = Ωm / ΩΛ * sinh (3 * HΛ * t / 2) ^ 2 := by310 have hs : 0 ≤ sinh (3 * HΛ * t / 2) := by311 rw [← Real.sinh_zero]; exact Real.sinh_le_sinh.2 (by positivity)312 have hq : 0 ≤ Ωm / ΩΛ := by positivity313 unfold lcdmScale314 rw [mul_pow, ← Real.rpow_natCast, ← Real.rpow_natCast, ← Real.rpow_mul hq, ← Real.rpow_mul hs]315 norm_num316317/-- The scale factor is positive for `t > 0`. -/318theorem lcdmScale_pos (Ωm ΩΛ HΛ t : ℝ) (hm : 0 < Ωm) (hΛ : 0 < ΩΛ) (hH : 0 < HΛ) (ht : 0 < t) :319 0 < lcdmScale Ωm ΩΛ HΛ t :=320 mul_pos (Real.rpow_pos_of_pos (by positivity) _)321 (Real.rpow_pos_of_pos (Real.sinh_pos_iff.2 (by positivity)) _)322323/-- The derivative of the scale factor for `t > 0`: `ȧ = H_Λ · (cosh x / sinh x) · a` with `x = 3H_Λ t/2`. -/324theorem lcdm_hasDerivAt (Ωm ΩΛ HΛ t : ℝ) (hm : 0 < Ωm) (hΛ : 0 < ΩΛ) (hH : 0 < HΛ) (ht : 0 < t) :325 HasDerivAt (lcdmScale Ωm ΩΛ HΛ)326 (HΛ * (cosh (3 * HΛ * t / 2) / sinh (3 * HΛ * t / 2)) * lcdmScale Ωm ΩΛ HΛ t) t := by327 set x := 3 * HΛ * t / 2 with hx328 have hxpos : 0 < x := by positivity329 set s := sinh x with hsdef330 have hs : 0 < s := Real.sinh_pos_iff.2 hxpos331 set K := (Ωm / ΩΛ) ^ ((1 : ℝ) / 3) with hK332 have hKpos : 0 < K := Real.rpow_pos_of_pos (by positivity) _333 have ha : lcdmScale Ωm ΩΛ HΛ t = K * s ^ ((2 : ℝ) / 3) := rfl334 have h1 : HasDerivAt (fun y : ℝ => 3 * HΛ * y / 2) (3 * HΛ / 2) t := by335 have := ((hasDerivAt_id t).const_mul (3 * HΛ)).div_const 2336 simpa using this337 have h2 : HasDerivAt (fun y : ℝ => sinh (3 * HΛ * y / 2)) (cosh x * (3 * HΛ / 2)) t := h1.sinh338 have h3 : HasDerivAt (fun y : ℝ => sinh (3 * HΛ * y / 2) ^ ((2 : ℝ) / 3))339 (cosh x * (3 * HΛ / 2) * ((2 : ℝ) / 3) * s ^ ((2 : ℝ) / 3 - 1)) t :=340 h2.rpow_const (Or.inl hs.ne')341 have h4 : HasDerivAt (lcdmScale Ωm ΩΛ HΛ)342 (K * (cosh x * (3 * HΛ / 2) * ((2 : ℝ) / 3) * s ^ ((2 : ℝ) / 3 - 1))) t := h3.const_mul K343 refine h4.congr_deriv ?_344 have hsub : s ^ ((2 : ℝ) / 3 - 1) = s ^ ((2 : ℝ) / 3) / s := by345 rw [Real.rpow_sub hs, Real.rpow_one]346 rw [ha, hsub]; field_simp347348/-- 14:A8, 14:C3 [ΛCDM] — the closed form solves the flat Friedmann equation of the rival chart with matter349and `Λ`: `a(0) = 0`, `a(t) > 0` and `ȧ > 0` for `t > 0` (the expanding branch), and350`(ȧ/a)² = H₀²(Ω_m a⁻³ + Ω_Λ)` with `H_Λ = H₀ √Ω_Λ`; that it is the unique such solution is not formalised. -/351theorem lcdm_friedmann (Ωm ΩΛ H0 t : ℝ) (hm : 0 < Ωm) (hΛ : 0 < ΩΛ) (hH : 0 < H0) (ht : 0 < t) :352 let HΛ := H0 * √ΩΛ353 let a' := HΛ * (cosh (3 * HΛ * t / 2) / sinh (3 * HΛ * t / 2)) * lcdmScale Ωm ΩΛ HΛ t354 lcdmScale Ωm ΩΛ HΛ 0 = 0 ∧ 0 < lcdmScale Ωm ΩΛ HΛ t ∧ 0 < a' ∧355 HasDerivAt (lcdmScale Ωm ΩΛ HΛ) a' t ∧356 (a' / lcdmScale Ωm ΩΛ HΛ t) ^ 2 = H0 ^ 2 * (Ωm / lcdmScale Ωm ΩΛ HΛ t ^ 3 + ΩΛ) := by357 intro HΛ a'358 have hHpos : 0 < HΛ := by positivity359 have hxpos : 0 < 3 * HΛ * t / 2 := by positivity360 have hs : 0 < sinh (3 * HΛ * t / 2) := Real.sinh_pos_iff.2 hxpos361 have hc : 0 < cosh (3 * HΛ * t / 2) := Real.cosh_pos _362 have hapos := lcdmScale_pos Ωm ΩΛ HΛ t hm hΛ hHpos ht363 refine ⟨?_, hapos, by positivity, lcdm_hasDerivAt Ωm ΩΛ HΛ t hm hΛ hHpos ht, ?_⟩364 · unfold lcdmScale365 simp [Real.zero_rpow (by norm_num : (2 : ℝ) / 3 ≠ 0)]366 · have hcube := lcdmScale_cube Ωm ΩΛ HΛ t hm hΛ hHpos.le ht.le367 have hH2 : HΛ ^ 2 = H0 ^ 2 * ΩΛ := by368 show (H0 * √ΩΛ) ^ 2 = H0 ^ 2 * ΩΛ369 rw [mul_pow, Real.sq_sqrt hΛ.le]370 have hratio : a' / lcdmScale Ωm ΩΛ HΛ t = HΛ * (cosh (3 * HΛ * t / 2) / sinh (3 * HΛ * t / 2)) := by371 show HΛ * (cosh (3 * HΛ * t / 2) / sinh (3 * HΛ * t / 2)) * lcdmScale Ωm ΩΛ HΛ t /372 lcdmScale Ωm ΩΛ HΛ t = _373 field_simp374 rw [hratio, hcube, mul_pow, div_pow, Real.cosh_sq, hH2]375 field_simp376 ring377378/-- The scale factor reaches `1` exactly when `sinh²(3H_Λ t/2) = Ω_Λ/Ω_m` (`t > 0`). -/379theorem lcdmScale_eq_one_iff (Ωm ΩΛ HΛ t : ℝ) (hm : 0 < Ωm) (hΛ : 0 < ΩΛ) (hH : 0 < HΛ) (ht : 0 < t) :380 lcdmScale Ωm ΩΛ HΛ t = 1 ↔ sinh (3 * HΛ * t / 2) ^ 2 = ΩΛ / Ωm := by381 have hapos := lcdmScale_pos Ωm ΩΛ HΛ t hm hΛ hH ht382 rw [← pow_eq_one_iff_of_nonneg hapos.le (by norm_num : (3 : ℕ) ≠ 0),383 lcdmScale_cube Ωm ΩΛ HΛ t hm hΛ hH.le ht.le]384 constructor385 · intro h; field_simp at h ⊢; linarith386 · intro h; rw [h]; field_simp387388/-- 14:A8, 14:C3, 14:X6 [ΛCDM] — the age identity verified: with `Ω_m + Ω_Λ = 1` the closed-form scale factor389reaches `1` at the time `t` exactly when `t H_Λ = (2/3) artanh √Ω_Λ`, so the product `t₀H_Λ` of C3 is the390chart's own age–rate relation, a function of the one fitted parameter. -/391theorem lcdm_age (Ωm ΩΛ H0 t : ℝ) (hm : 0 < Ωm) (hΛ : 0 < ΩΛ) (hsum : Ωm + ΩΛ = 1) (hH : 0 < H0)392 (ht : 0 < t) :393 lcdmScale Ωm ΩΛ (H0 * √ΩΛ) t = 1 ↔ t * (H0 * √ΩΛ) = lcdmAge ΩΛ := by394 set HΛ := H0 * √ΩΛ with hHΛ395 have hHpos : 0 < HΛ := by positivity396 set x := 3 * HΛ * t / 2 with hx397 have hxpos : 0 < x := by positivity398 have hs : 0 < sinh x := Real.sinh_pos_iff.2 hxpos399 have hΛ1 : ΩΛ < 1 := by linarith400 have hsq : √ΩΛ ∈ Set.Ioo (-1 : ℝ) 1 := by401 refine ⟨by linarith [Real.sqrt_nonneg ΩΛ], ?_⟩402 rw [Real.sqrt_lt' one_pos]; linarith403 rw [lcdmScale_eq_one_iff Ωm ΩΛ HΛ t hm hΛ hHpos ht]404 have hx' : t * HΛ = lcdmAge ΩΛ ↔ x = artanh √ΩΛ := by405 unfold lcdmAge FRC.Chart.lcdmAge; rw [hx]; constructor <;> intro h <;> linarith406 rw [hx']407 constructor408 · intro h409 have htanh : tanh x = √ΩΛ := by410 have hc : 0 < cosh x := Real.cosh_pos x411 have ht2 : tanh x ^ 2 = ΩΛ := by412 rw [Real.tanh_eq_sinh_div_cosh, div_pow, Real.cosh_sq, h]413 field_simp; linarith414 have htpos : 0 < tanh x := by415 rw [Real.tanh_eq_sinh_div_cosh]; exact div_pos hs hc416 rw [← ht2, Real.sqrt_sq htpos.le]417 rw [← htanh, Real.artanh_tanh]418 · intro h419 show sinh x ^ 2 = ΩΛ / Ωm420 rw [h, Real.sinh_artanh hsq, div_pow, Real.sq_sqrt hΛ.le, Real.sq_sqrt (by linarith)]421 congr 1; linarith422423/-- 14:A8, 14:C3 [ΛCDM] — the rate today: at the time the flat closed form reaches `1`, its derivative is424`H₀` — `H₀` is the present rate of the solution, `H_Λ = H₀√Ω_Λ` its asymptotic rate. -/425theorem lcdm_rate_today (Ωm ΩΛ H0 t : ℝ) (hm : 0 < Ωm) (hΛ : 0 < ΩΛ) (hsum : Ωm + ΩΛ = 1) (hH : 0 < H0)426 (ht : 0 < t) (h1 : lcdmScale Ωm ΩΛ (H0 * √ΩΛ) t = 1) :427 HasDerivAt (lcdmScale Ωm ΩΛ (H0 * √ΩΛ)) H0 t := by428 set HΛ := H0 * √ΩΛ with hHΛ429 have hHpos : 0 < HΛ := by positivity430 have hxpos : 0 < 3 * HΛ * t / 2 := by positivity431 have hs : 0 < sinh (3 * HΛ * t / 2) := Real.sinh_pos_iff.2 hxpos432 have hc : 0 < cosh (3 * HΛ * t / 2) := Real.cosh_pos _433 have hsin := (lcdmScale_eq_one_iff Ωm ΩΛ HΛ t hm hΛ hHpos ht).1 h1434 have hsqrt : 0 < √ΩΛ := Real.sqrt_pos.2 hΛ435 -- `(cosh/sinh)² = 1/Ω_Λ`, both sides positive436 have hcs : cosh (3 * HΛ * t / 2) / sinh (3 * HΛ * t / 2) = (√ΩΛ)⁻¹ := by437 rw [← pow_left_inj₀ (by positivity) (by positivity) (by norm_num : (2 : ℕ) ≠ 0), div_pow,438 Real.cosh_sq, hsin, inv_pow, Real.sq_sqrt hΛ.le]439 field_simp; linarith440 refine (lcdm_hasDerivAt Ωm ΩΛ HΛ t hm hΛ hHpos ht).congr_deriv ?_441 rw [h1, hcs, mul_one, hHΛ]; field_simp442443/-- The Taylor brackets of `e^t` at `t = 0.36118` and `t = 0.36128` (seven terms, Mathlib's tail bound). -/444theorem exp_tail_bounds' : exp (0.36118 : ℝ) < 1.4350218 ∧ (1.4351649 : ℝ) < exp 0.36128 := by445 constructor446 · have h := Real.exp_bound' (x := 0.36118) (by norm_num) (by norm_num) (n := 7) (by norm_num)447 norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢448 linarith449 · have h := abs_le.1 (Real.exp_bound (x := 0.36128) (by rw [abs_of_pos (by norm_num)]; norm_num)450 (n := 7) (by norm_num))451 rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.36128)] at h452 have h1 := h.1453 norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢454 linarith455456/-- 14:C3 — the audit numeral bracketed: at the fitted `Ω_Λ = 0.685` (A8, taken as data) the rival chart's457`t₀H_Λ = (2/3) artanh √0.685` lies in `(0.7870, 0.7871)` — the paper's `0.7871` — and exceeds `π/4` by458between `0.21 %` and `0.22 %` of `π/4`, the audit's "≈ 0.2 %". -/459theorem age_bracket :460 (0.7870 : ℝ) < lcdmAge 0.685 ∧ lcdmAge 0.685 < 0.7871 ∧461 0.0021 * (π / 4) < lcdmAge 0.685 - π / 4 ∧ lcdmAge 0.685 - π / 4 < 0.0022 * (π / 4) := by462 have hs1 : (0.82764 : ℝ) < √0.685 := by rw [Real.lt_sqrt (by norm_num)]; norm_num463 have hs2 : √(0.685 : ℝ) < 0.82765 := by rw [Real.sqrt_lt' (by norm_num)]; norm_num464 have hlog : lcdmAge 0.685 = 2 / 3 * (1 / 2 * log ((1 + √0.685) / (1 - √0.685))) := by465 unfold lcdmAge FRC.Chart.lcdmAge; rw [Real.artanh_eq_half_log ⟨by linarith, by linarith⟩]466 have hy1 : (10.6036 : ℝ) < (1 + √0.685) / (1 - √0.685) := by467 rw [lt_div_iff₀ (by linarith)]; linarith468 have hy2 : (1 + √0.685) / (1 - √0.685) < 10.6044 := by469 rw [div_lt_iff₀ (by linarith)]; linarith470 have he := exp_tail_bounds'471 have he1 := Real.exp_one_gt_d9472 have he2 := Real.exp_one_lt_d9473 have hpos : (0 : ℝ) < exp 1 := Real.exp_pos 1474 have hE1 : exp (2.36118 : ℝ) < 10.6036 := by475 rw [show (2.36118 : ℝ) = 1 + 1 + 0.36118 by norm_num, Real.exp_add, Real.exp_add]476 nlinarith [mul_pos hpos hpos, Real.exp_pos (0.36118 : ℝ)]477 have hE2 : (10.6044 : ℝ) < exp 2.36128 := by478 rw [show (2.36128 : ℝ) = 1 + 1 + 0.36128 by norm_num, Real.exp_add, Real.exp_add]479 nlinarith [mul_pos hpos hpos, Real.exp_pos (0.36128 : ℝ)]480 have hl1 : (2.36118 : ℝ) < log ((1 + √0.685) / (1 - √0.685)) := by481 rw [Real.lt_log_iff_exp_lt (by linarith)]; linarith482 have hl2 : log ((1 + √0.685) / (1 - √0.685)) < 2.36128 := by483 rw [Real.log_lt_iff_lt_exp (by linarith)]; linarith484 have hpi1 := Real.pi_gt_d6485 have hpi2 := Real.pi_lt_d6486 rw [hlog]487 refine ⟨by linarith, by linarith, by linarith, by linarith⟩488489end friedmann490491/-! ## The registrable triangle and the capacity axis (14:C9, C10, B10) -/492section triangle493494/-- 14:C9 [chart] — the count face and its chart dress: `S = π x²` with `x = r_H/ℓ_P > 0` gives `x = √(S/π)`495and `√S = √π · x`, the solid-angle `π` the declared transport between the count face `√S` and the drawn496width. -/497theorem count_face (S x : ℝ) (hx : 0 < x) (h : S = π * x ^ 2) :498 x = √(S / π) ∧ √S = √π * x := by499 have hpi := Real.pi_pos500 constructor501 · rw [h, mul_div_cancel_left₀ _ hpi.ne', Real.sqrt_sq hx.le]502 · rw [h, Real.sqrt_mul hpi.le, Real.sqrt_sq hx.le]503504/-- 14:C10 — the primality behind the capacity axis's identifications: `κ = 1` (the bare proton) is a shell,505`𝔽₅`; `κ = 2` has no shell (`9` is composite); `κ_H = 3` (ground-state hydrogen, the first non-trivial Object)506is the shell `𝔽₁₃`. -/507theorem capacity_zero : Nat.Prime (4 * 1 + 1) ∧ ¬ Nat.Prime (4 * 2 + 1) ∧ Nat.Prime (4 * 3 + 1) :=508 ⟨by norm_num, by norm_num, by norm_num⟩509510/-- 14:B10 — hydrogen units: the shell of capacity `3N` is `𝔽_{12N+1}`, so it exists exactly when `12N + 1` is511prime — `N = 1` (`13`) and `N = 3` (`37`) exist, `N = 2` (`25`) does not; and the nesting bound, the necessity512direction: a shell `q` registered whole by a Subject `p` of the Carrier `Ω` (`q² < p`, `p² < Ω`) has `q⁴ < Ω`,513so `(12N + 1)⁴ < Ω`; the existence of such a Subject is exhibited on the laboratory Carrier (`nesting_lab`). -/514theorem hydrogen_units :515 Nat.Prime 13 ∧ ¬ Nat.Prime 25 ∧ Nat.Prime 37 ∧516 ∀ q p Ω : ℕ, q ^ 2 < p → p ^ 2 < Ω → q ^ 4 < Ω := by517 refine ⟨by norm_num, by norm_num, by norm_num, fun q p Ω hq hp => ?_⟩518 calc q ^ 4 = (q ^ 2) ^ 2 := by ring519 _ < p ^ 2 := by gcongr520 _ < Ω := hp521522/-- 14:B10 — on the laboratory Carrier `Ω = 2 408 561` the bound is `N ≤ 3`: `37⁴ < Ω < 49⁴`; and the shell of523capacity `9` (`q = 37`) nests through the Subject `p = 1373 = 4 · 343 + 1`, prime: `37² < 1373`,524`1373² < Ω`. -/525theorem nesting_lab :526 37 ^ 4 < 2408561 ∧ 2408561 < 49 ^ 4 ∧ (∀ N : ℕ, (12 * N + 1) ^ 4 < 2408561 → N ≤ 3) ∧527 Nat.Prime 1373 ∧ 1373 = 4 * 343 + 1 ∧ 37 ^ 2 < 1373 ∧ 1373 ^ 2 < 2408561 := by528 refine ⟨by norm_num, by norm_num, fun N h => ?_, by norm_num, by norm_num, by norm_num, by norm_num⟩529 by_contra hN530 have h4 : 4 ≤ N := by omega531 have : (12 * 4 + 1) ^ 4 ≤ (12 * N + 1) ^ 4 := by gcongr532 omega533534end triangle535536/-! ## 14:B11–B13 — the additive window, the lock of like units, the shells of capacity `3N` (master F7, returned53715 October 2026) -/538section window539540/-- 14:B11 — the additive window: for modes at heights `hᵢ` with `|hᵢ| ≤ κᵢ` (as a list of pairs `(hᵢ, κᵢ)`) the541total has `|Σhᵢ| ≤ Σκᵢ`; the bound is attained by `hᵢ = κᵢ`; and every total `t` with `|t| ≤ Σκᵢ` occurs — the542first height the clamp of `t` to `[−κ₁, κ₁]`, the rest by induction. -/543theorem additive_window :544 (∀ (l : List (ℤ × ℕ)), (∀ x ∈ l, x.1.natAbs ≤ x.2) → (l.map Prod.fst).sum.natAbs ≤ (l.map Prod.snd).sum) ∧545 (∀ (κ : List ℕ), ((κ.map fun (k : ℕ) => (k : ℤ)).sum).natAbs = κ.sum) ∧546 (∀ (κ : List ℕ) (t : ℤ), t.natAbs ≤ κ.sum →547 ∃ l : List (ℤ × ℕ), l.map Prod.snd = κ ∧ (∀ x ∈ l, x.1.natAbs ≤ x.2) ∧ (l.map Prod.fst).sum = t) := by548 refine ⟨?_, ?_, ?_⟩549 · intro l550 induction l with551 | nil => intro _; simp552 | cons x t ih =>553 intro hb554 have h1 : x.1.natAbs ≤ x.2 := hb x (List.mem_cons_self ..)555 have ih' := ih (fun y hy => hb y (List.mem_cons_of_mem _ hy))556 simp only [List.map_cons, List.sum_cons]557 exact Nat.le_trans (Int.natAbs_add_le _ _) (Nat.add_le_add h1 ih')558 · intro κ559 induction κ with560 | nil => simp561 | cons k t ih =>562 simp only [List.map_cons, List.sum_cons]563 have hnn : 0 ≤ (t.map fun (k : ℕ) => (k : ℤ)).sum := by564 clear ih565 induction t with566 | nil => simp567 | cons a t iht => simp only [List.map_cons, List.sum_cons]; omega568 omega569 · intro κ570 induction κ with571 | nil =>572 intro t ht573 refine ⟨[], rfl, fun x hx => absurd hx List.not_mem_nil, ?_⟩574 simp only [List.sum_nil] at ht; simp only [List.map_nil, List.sum_nil]; omega575 | cons k κ' ih =>576 intro t ht577 let h₀ : ℤ := if t > (k : ℤ) then (k : ℤ) else if t < -(k : ℤ) then -(k : ℤ) else t578 have hk : h₀.natAbs ≤ k := by579 simp only [h₀]; split580 · omega581 · split <;> omega582 have hr : (t - h₀).natAbs ≤ κ'.sum := by583 simp only [List.sum_cons] at ht584 simp only [h₀]; split585 · omega586 · split <;> omega587 obtain ⟨l, hl, hb, hs⟩ := ih (t - h₀) hr588 refine ⟨(h₀, k) :: l, by simp [hl], ?_, ?_⟩589 · intro x hx590 rcases List.mem_cons.mp hx with rfl | hx'591 · exact hk592 · exact hb x hx'593 · simp only [List.map_cons, List.sum_cons, hs]; omega594595/-- 14:B12 — the lock of like units: the joint recurrence of `N + 1` cycles of period `12` is `12` for every `N`,596`lcm (12, …, 12) = 12`, so no element of the lock has order `12N` for `N ≥ 2`; the diagonal drive on `ZMod 12 × ZMod 12`597keeps the offset `x − y` (one superselected `C₁₂` offset per further unit), and `144 = 12 · 12`, `1728 = 144 · 12`598points fall into orbits of length `12`. -/599theorem lock_recurrence :600 (∀ N : ℕ, (List.replicate (N + 1) (12 : ℕ)).foldr Nat.lcm 1 = 12) ∧601 (∀ N : ℕ, 2 ≤ N → 12 * N ≠ 12) ∧602 (∀ x y : ZMod 12, (x + 1) - (y + 1) = x - y) ∧ (∀ x : ZMod 12, x + 12 = x) ∧603 144 = 12 * 12 ∧ 1728 = 144 * 12 := by604 refine ⟨fun N => ?_, fun N hN => by omega, fun x y => by ring, fun x => by605 have h12 : (12 : ZMod 12) = 0 := by decide606 rw [h12, add_zero], by norm_num, by norm_num⟩607 induction N with608 | zero => simp609 | succ n ih => simp only [List.replicate_succ, List.foldr_cons] at ih ⊢; rw [ih]; decide610611/-- 14:B13 — the shell of capacity `3N` is `𝔽_{12N+1}`, `4 · 3N + 1 = 12N + 1`, and exists exactly when `12N + 1` is612prime: below `N = 10` for `N = 1, 3, 5, 6, 8, 9` and not at `N = 2` (`25 = 5²`), `4`, `7`. -/613theorem shells_of_capacity :614 (∀ N : ℕ, 4 * (3 * N) + 1 = 12 * N + 1) ∧615 (∀ N : ℕ, N < 10 → (Nat.Prime (12 * N + 1) ↔ N = 1 ∨ N = 3 ∨ N = 5 ∨ N = 6 ∨ N = 8 ∨ N = 9)) ∧616 25 = 5 ^ 2 := by617 refine ⟨fun N => by ring, fun N hN => ?_, by norm_num⟩618 interval_cases N <;> norm_num619620/-- 14:B13 — fusion of coprime cycles is multiplicative: for coprime periods `n₁, n₂` the joint recurrence is621`lcm n₁ n₂ = n₁ n₂`, and the fused capacity `n₁ n₂ / 4`; hydrogen `(4, 3)`: `lcm = 12`, capacity `3`; like cycles do622not fuse, `lcm (12, 12) = 12 = gcd (12, 12)`, and the capacity-`3` shell `13` is not the lock's register `12`. -/623theorem fusion_capacity :624 (∀ n₁ n₂ : ℕ, Nat.Coprime n₁ n₂ → Nat.lcm n₁ n₂ = n₁ * n₂) ∧625 Nat.lcm 4 3 = 12 ∧ 4 * 3 / 4 = 3 ∧ Nat.lcm 12 12 = 12 ∧ Nat.gcd 12 12 = 12 ∧ (13 : ℕ) ≠ 12 :=626 ⟨fun _ _ h => h.lcm_eq_mul, by decide, by norm_num, by decide, by decide, by norm_num⟩627628end window629630/-! ## The channels, the imports and the predictions: the chart arithmetic each row consumes631(14:C1, X1, X5, X7, X8, P1, P2; 15 October 2026) -/632section channels633634/-- 14:C1 [chart] — the two faces: with `c > 0` the conversion `r = c t` is a bijection between the temporal635and the spatial datum, `r = c t ↔ t = r/c`, and each face returns the other, `(c t)/c = t`, `c (r/c) = r`. That an636instrument reads exactly one of the two faces is C1's realisation clause (a frame supplies one datum of each kind),637not formal content. -/638theorem two_faces (c r t : ℝ) (hc : 0 < c) :639 (r = c * t ↔ t = r / c) ∧ c * t / c = t ∧ c * (r / c) = r := by640 have hc' := hc.ne'641 refine ⟨⟨fun h => ?_, fun h => ?_⟩, mul_div_cancel_left₀ t hc', mul_div_cancel₀ r hc'⟩642 · rw [h, mul_div_cancel_left₀ t hc']643 · rw [h, mul_div_cancel₀ r hc']644645/-- 14:X1 [chart] — the curvature face of the one cardinality: with `Λ = 3/r_H²` (the de Sitter radius) and646`S = π (r_H/ℓ_P)²` (the count face, B9), `Λ ℓ_P² = 3π/S` identically. The constant is the cardinality read on the647curvature face; that no mode sum enters is X1's realisation clause. -/648theorem lambda_face (Λ S r ℓ : ℝ) (hr : r ≠ 0) (hℓ : ℓ ≠ 0) (hΛ : Λ = 3 / r ^ 2)649 (hS : S = π * (r / ℓ) ^ 2) : Λ * ℓ ^ 2 = 3 * π / S := by650 subst hΛ hS651 have hpi := Real.pi_ne_zero652 field_simp653654/-- 14:X5 [chart] — the over-closure exit of the typical-density diagonal: a body of density `ρ₀` (the paper's `c̃`) on the cubic655`M = ρ₀ R³` that sits on its own Schwarzschild radius `R = 2GM/c²` has `M² = c⁶/(8 G³ ρ₀)`, one positive mass —656the exit of C9 read as a bound. Its value `1.8 × 10⁸ M☉` at `ρ₀ = 0.97 × 10³ kg/m³` is the python witness's657(`tri.W`). -/658theorem wall_exit (M R G c ρ₀ : ℝ) (hc : 0 < c) (hG : 0 < G) (hM : 0 < M)659 (hρ : M = ρ₀ * R ^ 3) (hR : R = 2 * G * M / c ^ 2) :660 0 < ρ₀ ∧ M ^ 2 = c ^ 6 / (8 * G ^ 3 * ρ₀) := by661 subst hR662 have hc6 : (c ^ 6) ≠ 0 := by positivity663 have h1 : ρ₀ * (2 * G * M / c ^ 2) ^ 3 = 8 * ρ₀ * G ^ 3 * M ^ 3 / c ^ 6 := by664 field_simp; ring665 have h2 : M * c ^ 6 = 8 * ρ₀ * G ^ 3 * M ^ 3 := by666 have := hρ667 rw [h1, eq_div_iff hc6] at this668 exact this669 have hρpos : 0 < ρ₀ := by670 by_contra h671 have h8 : 8 * ρ₀ ≤ 0 := by linarith [not_lt.1 h]672 have : 8 * ρ₀ * G ^ 3 * M ^ 3 ≤ 0 :=673 mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg h8 (pow_pos hG 3).le) (pow_pos hM 3).le674 have : 0 < M * c ^ 6 := by positivity675 linarith676 refine ⟨hρpos, ?_⟩677 rw [eq_div_iff (by positivity)]678 have h3 : M * c ^ 6 = M * (M ^ 2 * (8 * G ^ 3 * ρ₀)) := by rw [h2]; ring679 exact (mul_left_cancel₀ hM.ne' h3).symm680681/-- 14:X7, 14:X8 [ΛCDM] — the Hubble radius on the black-hole line: the density of a Schwarzschild mass682`M = r c²/2G` spread over its own ball is `ρ_BH(r) = 3c²/(8πG r²)`; at `r = c/H` it is the critical density683`ρ_c = 3H²/(8πG)` identically, and the equality `ρ_BH(r) = ρ_c` holds at `r = c/H` alone — the saturation684identity X7 and X8 share. That the Schwarzschild reading consumes an exterior, and what each interior completion685consumes, is the rows' realisation content. -/686theorem hubble_on_bh_line (c G H r : ℝ) (hc : 0 < c) (hG : 0 < G) (hH : 0 < H) (hr : 0 < r) :687 (r * c ^ 2 / (2 * G)) / (4 / 3 * π * r ^ 3) = 3 * c ^ 2 / (8 * π * G * r ^ 2) ∧688 ((c / H) * c ^ 2 / (2 * G)) / (4 / 3 * π * (c / H) ^ 3) = 3 * H ^ 2 / (8 * π * G) ∧689 (3 * c ^ 2 / (8 * π * G * r ^ 2) = 3 * H ^ 2 / (8 * π * G) ↔ r = c / H) := by690 have hpi := Real.pi_pos691 refine ⟨?_, ?_, ?_⟩692 · field_simp; try ring693 · field_simp; try ring694 · rw [div_eq_div_iff (by positivity) (by positivity)]695 constructor696 · intro h697 have h2 : c ^ 2 * (24 * π * G) = (H * r) ^ 2 * (24 * π * G) := by linear_combination h698 have h3 : c ^ 2 = (H * r) ^ 2 := mul_right_cancel₀ (by positivity) h2699 have h4 : c = H * r := (pow_left_inj₀ hc.le (by positivity) two_ne_zero).1 h3700 rw [h4, mul_div_cancel_left₀ r hH.ne']701 · intro h702 rw [h]; field_simp; try ring703704/-- 14:P1 [ΛCDM] — the running floor: with `a₀(z) = A H(z)/2π` and `H(z) = H₀ E(z)`,705`E(z) = √(Ω_m (1+z)³ + Ω_Λ)`, the floor's ratio to today is the chart's `E(z)` (`E(0) = 1` on a flat chart), and at706`z = 1` on the fitted chart (`Ω_m = 0.315`) it lies in `(1.79, 1.80)`: the floor runs with the registered rate. The707confrontation with the four redshift bins is the python witness's (`est.P1`). -/708theorem running_floor (A H0 Ωm ΩΛ z : ℝ) (hA : A ≠ 0) (hH : H0 ≠ 0) (hsum : Ωm + ΩΛ = 1) :709 (A * (H0 * √(Ωm * (1 + z) ^ 3 + ΩΛ)) / (2 * π)) / (A * (H0 * √(Ωm * (1 + 0) ^ 3 + ΩΛ)) / (2 * π))710 = √(Ωm * (1 + z) ^ 3 + ΩΛ) ∧711 (1.79 : ℝ) < √(0.315 * (1 + 1) ^ 3 + 0.685) ∧ √(0.315 * (1 + 1) ^ 3 + 0.685) < 1.80 := by712 have hpi := Real.pi_ne_zero713 refine ⟨?_, ?_, ?_⟩714 · have h0 : Ωm * (1 + 0) ^ 3 + ΩΛ = 1 := by norm_num; linarith715 rw [h0, Real.sqrt_one]716 field_simp717 · rw [Real.lt_sqrt (by norm_num)]; norm_num718 · rw [Real.sqrt_lt' (by norm_num)]; norm_num719720/-- 14:P2, 14:X8 [chart, ΛCDM] — the registered record depth: the octant's chart conversion `(S/2)/(4S) · 2π r_H/c =721(π/4) r_H/c` (C5) at every frame chronon; the rival chart's `t₀ H_Λ` at the fitted `Ω_Λ = 0.685` exceeds `π/4` by722`0.21–0.22 %` (the "degenerate to 0.2 % now", C3); and a `t₀` growing one Gyr per Gyr of chart time separates from723the fixed `13.79 Gyr` at `1/13.79` per Gyr, which lies in `(7 %, 7.5 %)`. The numeral `13.79 Gyr` and the724confrontation with the cluster ages are the python witness's (`est.P2`). -/725theorem record_depth :726 (∀ S r c : ℝ, S ≠ 0 → (S / 2) / (4 * S) * (2 * π * r / c) = (π / 4) * r / c) ∧727 (0.0021 * (π / 4) < lcdmAge 0.685 - π / 4 ∧ lcdmAge 0.685 - π / 4 < 0.0022 * (π / 4)) ∧728 ((0.07 : ℝ) < 1 / 13.79 ∧ (1 : ℝ) / 13.79 < 0.075) :=729 ⟨fun S r c hS => FRC.Chart.octant_chart S r c hS, age_bracket.2.2, by norm_num, by norm_num⟩730731end channels732733/-! ## Old names (ledger migration, task LM30): the theorems moved to the chart theme (`FRC.Chart`,734`FrcLedger/Theme/Chart.lean`), each under its old name -/735736/-- 14:C5 [chart] — the chart conversion of the octant: `(S/2)/(4S) · 2π r_H/c = (π/4) r_H/c`. -/737theorem octant_chart (S r c : ℝ) (hS : S ≠ 0) :738 (S / 2) / (4 * S) * (2 * π * r / c) = (π / 4) * r / c :=739 FRC.Chart.octant_chart S r c hS740741/-- The octant's rate factor `tanh(3π/8)` is positive. -/742theorem tanh_octant_pos : 0 < tanh (3 * π / 8) :=743 FRC.Chart.tanh_octant_pos744745/-- 14:P3 [ΛCDM] — the algebraic locus `t H₀ = (π/4)/tanh(3π/8)`. -/746theorem age_rate_locus (t H0 HΛ Ω : ℝ) (hoct : t * HΛ = π / 4) (hΛ : HΛ = H0 * √Ω)747 (hΩ : Ω = tanh (3 * π / 8) ^ 2) : t * H0 = (π / 4) / tanh (3 * π / 8) :=748 FRC.Chart.age_rate_locus t H0 HΛ Ω hoct hΛ hΩ749750/-- `tanh x = (e^{2x} − 1)/(e^{2x} + 1)`. -/751theorem tanh_eq_exp_two_mul (x : ℝ) : tanh x = (exp (2 * x) - 1) / (exp (2 * x) + 1) :=752 FRC.Chart.tanh_eq_exp_two_mul x753754/-- The Taylor brackets of `e^t` at the two ends of `t = 3π/4 − 2`. -/755theorem exp_tail_bounds :756 (1.427884 : ℝ) < exp 0.356194 ∧ exp (0.35619475 : ℝ) < 1.4278857 :=757 FRC.Chart.exp_tail_bounds758759/-- `10.55071 < e^{3π/4} < 10.55073`. -/760theorem exp_three_pi_four_bounds : (10.55071 : ℝ) < exp (3 * π / 4) ∧ exp (3 * π / 4) < 10.55073 :=761 FRC.Chart.exp_three_pi_four_bounds762763/-- `0.82685 < tanh(3π/8) < 0.826851`. -/764theorem tanh_octant_bounds : (0.82685 : ℝ) < tanh (3 * π / 8) ∧ tanh (3 * π / 8) < 0.826851 :=765 FRC.Chart.tanh_octant_bounds766767/-- 14:P3 — `0.9498 < (π/4)/tanh(3π/8) < 0.9499`. -/768theorem locus_bracket : (0.9498 : ℝ) < (π / 4) / tanh (3 * π / 8) ∧ (π / 4) / tanh (3 * π / 8) < 0.9499 :=769 FRC.Chart.locus_bracket770771/-- 14:C7, 14:X3 — `0.68368 < tanh²(3π/8) < 0.68369`, a deviation between `0.18σ` and `0.19σ` from `0.685 ± 0.007`. -/772theorem landing_bracket :773 (0.68368 : ℝ) < tanh (3 * π / 8) ^ 2 ∧ tanh (3 * π / 8) ^ 2 < 0.68369 ∧774 0.18 * 0.007 < 0.685 - tanh (3 * π / 8) ^ 2 ∧ 0.685 - tanh (3 * π / 8) ^ 2 < 0.19 * 0.007 :=775 FRC.Chart.landing_bracket776777-- Ledger predicates of 14-entropy (generated by make_predicates.py from docs/14-entropy/14-entropy-ledger.json; edit the ledger, not this section)778/-- 14:A1 (p14001) — The de Sitter entropy $\dS$, the single quantitative import, fixing the cardinality exactly, $\Om=4\dS+1$. -/779theorem p14001 : ∀ {Ω S : ℕ}, Ω = (4 : ℕ) * S + (1 : ℕ) → S = (Ω - (1 : ℕ)) / (4 : ℕ) ∧ (4 : ℕ) ∣ Ω - (1 : ℕ) ∧ Ω % (4 : ℕ) = (1 : ℕ) ∧ (4 : ℕ) * S = Ω - (1 : ℕ) :=780 @FRC.Entropy.cardinality781/-- 14:A2 (p14002) — The Carrier congruences, relations certified by the realisations (the $c$-square $\dS$ even, the triality centre $\dS\equiv1\pmod3$, completeness $4\dS+1$ prime); instantiated on the laboratory Carrier as host-decided values. -/782theorem p14002 : ((4 : ℕ) * (602140 : ℕ) + (1 : ℕ) = (2408561 : ℕ) ∧ Even (602140 : ℕ) ∧ (602140 : ℕ) % (3 : ℕ) = (1 : ℕ) ∧ Nat.Prime (2408561 : ℕ)) ∧ (∀ (S : ℕ) [hp : Fact (Nat.Prime ((4 : ℕ) * S + (1 : ℕ)))], (IsSquare (2 : ZMod ((4 : ℕ) * S + (1 : ℕ))) ↔ Even S) ∧ (IsSquare (2 : ZMod ((4 : ℕ) * S + (1 : ℕ)))⁻¹ ↔ Even S)) ∧ ∀ (S : ℕ), S % (3 : ℕ) = (1 : ℕ) → ∀ [Fact (Nat.Prime ((4 : ℕ) * S + (1 : ℕ)))], (3 : ℕ) ∣ (4 : ℕ) * S + (1 : ℕ) + (1 : ℕ) ∧ ¬(3 : ℕ) ∣ (4 : ℕ) * S ∧ ∀ (x : (ZMod ((4 : ℕ) * S + (1 : ℕ)))ˣ), orderOf x ≠ (3 : ℕ) :=783 And.intro @FRC.Entropy.carrierLab (And.intro @FRC.Entropy.c_square (@FRC.Entropy.triality_centre))784/-- 14:B2 (p14010) — The angle--count dictionary: $2\pi$ the full cycle, $h=2\pi\hbar$; every angular numeral is the chart face of a count ($\pi/4\leftrightarrow\dS/2$ chronons). -/785theorem p14010 : ∀ (S : ℝ), Real.pi / ((2 : ℝ) * Real.pi) * ((4 : ℝ) * S) = (2 : ℝ) * S ∧ Real.pi / (2 : ℝ) / ((2 : ℝ) * Real.pi) * ((4 : ℝ) * S) = S ∧ Real.pi / (4 : ℝ) / ((2 : ℝ) * Real.pi) * ((4 : ℝ) * S) = S / (2 : ℝ) :=786 @FRC.Entropy.dictionary787/-- 14:B8 (p14016) — The effective-fluid correspondence behind P4: the rival chart's continuity law $\dot\rho_\Lambda+3H(\rho_\Lambda+p_\Lambda)=0$ \lcdm{} with $\dot\rho_\Lambda=0$ gives $w=-1$; and the single-component clause --- the framework's dark sector is derived with no second dark-energy component available, so an observed $w_{\mathrm{eff}}\neq-1$ cannot be reassigned to an extra evolving fluid. The clause makes P4's falsifier total rather than escapable. -/788theorem p14016 : ∀ (H ρ p ρ' : ℝ), H ≠ (0 : ℝ) → ρ ≠ (0 : ℝ) → ρ' = (0 : ℝ) → ρ' + (3 : ℝ) * H * (ρ + p) = (0 : ℝ) → p = -ρ ∧ p / ρ = (-1 : ℝ) :=789 @FRC.Entropy.fluid_w790/-- 14:B9 (p14017) — The area law: the projected horizon area in Planck cells is the full phase cycle, $A=4\dS$ \apx{} at the horizon ($4\pi n_A=4\dS$, $n_A=(r_H/\lP)^{2}$ \apx); the Bekenstein--Hawking quarter $\dS=A/4$ is the quarter-turn $Q_4$, the generative four of $\Om=4\dS+1$ and $\p=4\kap+1$; area is a Subject-projection property, the Carrier carrying none. -/791theorem p14017 : (∀ (S : ℕ) [hp : Fact (Nat.Prime ((4 : ℕ) * S + (1 : ℕ)))], IsSquare (-1 : ZMod ((4 : ℕ) * S + (1 : ℕ))) ∧ ∃ i, i ^ (2 : ℕ) = (-1 : ZMod ((4 : ℕ) * S + (1 : ℕ))) ∧ i ^ (4 : ℕ) = (1 : ZMod ((4 : ℕ) * S + (1 : ℕ))) ∧ i ≠ (1 : ZMod ((4 : ℕ) * S + (1 : ℕ))) ∧ i ≠ (-1 : ZMod ((4 : ℕ) * S + (1 : ℕ)))) ∧ ∀ (S : ℝ), (4 : ℝ) * Real.pi * (S / Real.pi) = (4 : ℝ) * S :=792 And.intro @FRC.Entropy.quarter_turn (@FRC.Entropy.area_law_chart)793/-- 14:B10 (p14044) — The capacity axis counts hydrogen units (one gram at $N_A$ to $0.003$ dex \apx): a definition, not a registered shell. The least register window resolving the total winding of $N$ units is $3N$, a theorem about the observing Subject (B11); a phase-locked composite of like units is an aggregate, never one shell (B12; a shell of capacity $3N$ exists only when $12N+1$ is prime, B13); the largest shell any Subject registers whole is the nesting bound $\mathsf{q}<\Om^{1/4}$ (00:B8), $N<(\Om^{1/4}-1)/12$ units, $8\times10^{2}$\,kg at $\dS=3.3\times10^{122}$ \apx{} ($\Om^{1/4}$ units overcounts by $12$); everything heavier an aggregate of locks; the proton's $1$ against $3$ compares a tower label with a chart count. -/794theorem p14044 : (Nat.Prime (13 : ℕ) ∧ ¬Nat.Prime (25 : ℕ) ∧ Nat.Prime (37 : ℕ) ∧ ∀ (q p Ω : ℕ), q ^ (2 : ℕ) < p → p ^ (2 : ℕ) < Ω → q ^ (4 : ℕ) < Ω) ∧ (37 : ℕ) ^ (4 : ℕ) < (2408561 : ℕ) ∧ (2408561 : ℕ) < (49 : ℕ) ^ (4 : ℕ) ∧ (∀ (N : ℕ), ((12 : ℕ) * N + (1 : ℕ)) ^ (4 : ℕ) < (2408561 : ℕ) → N ≤ (3 : ℕ)) ∧ Nat.Prime (1373 : ℕ) ∧ (1373 : ℕ) = (4 : ℕ) * (343 : ℕ) + (1 : ℕ) ∧ (37 : ℕ) ^ (2 : ℕ) < (1373 : ℕ) ∧ (1373 : ℕ) ^ (2 : ℕ) < (2408561 : ℕ) :=795 And.intro @FRC.Entropy.hydrogen_units (@FRC.Entropy.nesting_lab)796/-- 14:B11 (p14046) — The additive window: for $N$ modes at resolvable heights $|\hat h_i|\le\kap_i$ (38:A8) the total winding satisfies $|\sum_i\hat h_i|\le\sum_i\kap_i$, attained, every total in the range occurring; the least register window resolving the total exactly is the capacity sum $\sum_i\kap_i$, $3N$ for $N$ hydrogen units --- a capacity of the observing Subject, not a shell of the composite (B10). -/797theorem p14046 : And (∀ (l : List (Prod Int Nat)), (∀ (x : Prod Int Nat), @Membership.mem (Prod Int Nat) (List (Prod Int Nat)) (@List.instMembership (Prod Int Nat)) l x → @LE.le Nat instLENat (@Prod.fst Int Nat x).natAbs (@Prod.snd Int Nat x)) → @LE.le Nat instLENat (@List.sum Int Int.instAdd (@MulZeroClass.toZero Int (@instMulZeroClassOfSemiring Int Int.instSemiring)) (@List.map (Prod Int Nat) Int (@Prod.fst Int Nat) l)).natAbs (@List.sum Nat instAddNat (@MulZeroClass.toZero Nat Nat.instMulZeroClass) (@List.map (Prod Int Nat) Nat (@Prod.snd Int Nat) l))) (And (∀ (κ : List Nat), @Eq Nat (@List.sum Int Int.instAdd (@MulZeroClass.toZero Int (@instMulZeroClassOfSemiring Int Int.instSemiring)) (@List.map Nat Int (fun k => @Nat.cast Int instNatCastInt k) κ)).natAbs (@List.sum Nat instAddNat (@MulZeroClass.toZero Nat Nat.instMulZeroClass) κ)) (∀ (κ : List Nat) (t : Int), @LE.le Nat instLENat t.natAbs (@List.sum Nat instAddNat (@MulZeroClass.toZero Nat Nat.instMulZeroClass) κ) → ∃ l, And (@Eq (List Nat) (@List.map (Prod Int Nat) Nat (@Prod.snd Int Nat) l) κ) (And (∀ (x : Prod Int Nat), @Membership.mem (Prod Int Nat) (List (Prod Int Nat)) (@List.instMembership (Prod Int Nat)) l x → @LE.le Nat instLENat (@Prod.fst Int Nat x).natAbs (@Prod.snd Int Nat x)) (@Eq Int (@List.sum Int Int.instAdd (@MulZeroClass.toZero Int (@instMulZeroClassOfSemiring Int Int.instSemiring)) (@List.map (Prod Int Nat) Int (@Prod.fst Int Nat) l)) t)))) :=798 @FRC.Entropy.additive_window799/-- 14:B12 (p14047) — The lock of like units: $N$ like units never fuse (00:F6, $\gcd(12,12)=12$): their joint registration (00:F2) recurs on $C_{12}$ with period $12$ for every $N$, one superselected $C_{12}$ offset per further unit --- an aggregate, never one shell. Instances: the diagonal drive on $C_{12}^{2}$ has $12$ orbits of length $12$, on $C_{12}^{3}$ $144$. -/800theorem p14047 : (∀ (N : ℕ), List.foldr Nat.lcm (1 : ℕ) (List.replicate (N + (1 : ℕ)) (12 : ℕ)) = (12 : ℕ)) ∧ (∀ (N : ℕ), (2 : ℕ) ≤ N → (12 : ℕ) * N ≠ (12 : ℕ)) ∧ (∀ (x y : ZMod (12 : ℕ)), x + (1 : ZMod (12 : ℕ)) - (y + (1 : ZMod (12 : ℕ))) = x - y) ∧ (∀ (x : ZMod (12 : ℕ)), x + (12 : ZMod (12 : ℕ)) = x) ∧ (144 : ℕ) = (12 : ℕ) * (12 : ℕ) ∧ (1728 : ℕ) = (144 : ℕ) * (12 : ℕ) :=801 @FRC.Entropy.lock_recurrence802/-- 14:B13 (p14048) — Shells of capacity $3N$ and fusion: the shell of capacity $3N$ is $\F_{12N+1}$ and exists iff $12N+1$ is prime ($N=1,3,5,6,8,9$ below $10$; none at $N=2$, $25=5^{2}$), never the lock's register (B12); fusion of coprime cycles is multiplicative, $\kap=n_{1}n_{2}/4$: hydrogen $(4,3)\to3$, one orbit of length $12$ (00:F6). -/803theorem p14048 : ((∀ (N : ℕ), (4 : ℕ) * ((3 : ℕ) * N) + (1 : ℕ) = (12 : ℕ) * N + (1 : ℕ)) ∧ (∀ N < (10 : ℕ), Nat.Prime ((12 : ℕ) * N + (1 : ℕ)) ↔ N = (1 : ℕ) ∨ N = (3 : ℕ) ∨ N = (5 : ℕ) ∨ N = (6 : ℕ) ∨ N = (8 : ℕ) ∨ N = (9 : ℕ)) ∧ (25 : ℕ) = (5 : ℕ) ^ (2 : ℕ)) ∧ (∀ (n₁ n₂ : ℕ), n₁.Coprime n₂ → n₁.lcm n₂ = n₁ * n₂) ∧ Nat.lcm (4 : ℕ) (3 : ℕ) = (12 : ℕ) ∧ (4 : ℕ) * (3 : ℕ) / (4 : ℕ) = (3 : ℕ) ∧ Nat.lcm (12 : ℕ) (12 : ℕ) = (12 : ℕ) ∧ Nat.gcd (12 : ℕ) (12 : ℕ) = (12 : ℕ) ∧ (13 : ℕ) ≠ (12 : ℕ) :=804 And.intro @FRC.Entropy.shells_of_capacity (@FRC.Entropy.fusion_capacity)805/-- 14:C1 (p14018) — Two faces: a frame supplies one spatial and one temporal datum, so every instrument reading the size of the totality is one of exactly two faces, converted by $c$. -/806theorem p14018 : ∀ (c r t : ℝ), (0 : ℝ) < c → (r = c * t ↔ t = r / c) ∧ c * t / c = t ∧ c * (r / c) = r :=807 @FRC.Entropy.two_faces808/-- 14:C2 (p14019) — The non-channels: the constants correspondence carries no dimensional readout, the horizon-quarter closure is an internal consistency loop, the registered entropy budget is a floor eighteen orders below $\dS$ \apx. -/809theorem p14019 : ∀ (Ω S : ℕ) (p : ℝ), Ω = (4 : ℕ) * S + (1 : ℕ) → p ^ (2 : ℕ) = ↑Ω → (p ^ (2 : ℕ) - (1 : ℝ)) / (4 : ℝ) = ↑S :=810 @FRC.Entropy.horizon_quarter_closure811/-- 14:C3 (p14020) — The same-channel demotion: $t_0H_\Lambda=\tfrac23\artanh\sqrt{\Omega_\Lambda}$ \lcdm{} depends on the one fitted parameter, so the $0.2\%$ landing on $\pi/4$ restates the fit (by B5). Cited definitions (not proofs): FRC.Entropy.lcdmAge. -/812theorem p14020 : (∀ (Ωm ΩΛ H0 t : ℝ), (0 : ℝ) < Ωm → (0 : ℝ) < ΩΛ → Ωm + ΩΛ = (1 : ℝ) → (0 : ℝ) < H0 → (0 : ℝ) < t → (FRC.Entropy.lcdmScale Ωm ΩΛ (H0 * √ΩΛ) t = (1 : ℝ) ↔ t * (H0 * √ΩΛ) = FRC.Entropy.lcdmAge ΩΛ)) ∧ 0.7870 < FRC.Entropy.lcdmAge 0.685 ∧ FRC.Entropy.lcdmAge 0.685 < 0.7871 ∧ 21e-4 * (Real.pi / (4 : ℝ)) < FRC.Entropy.lcdmAge 0.685 - Real.pi / (4 : ℝ) ∧ FRC.Entropy.lcdmAge 0.685 - Real.pi / (4 : ℝ) < 22e-4 * (Real.pi / (4 : ℝ)) :=813 And.intro @FRC.Entropy.lcdm_age (@FRC.Entropy.age_bracket)814/-- 14:C5 (p14022) — The octant lemma: the measured age is $\dS/2$ chronons, $(\pi/4)\,r_H/c$ in the chart \apx; the halving and the sector are exact through the enumerated realisation set $B_{\mathrm{oct}}=\{$A4, A5, B2, B3, B6, B7$\}$, the same class as the constants correspondence. -/815theorem p14022 : (∀ (S r c : ℝ), S ≠ (0 : ℝ) → S / (2 : ℝ) / ((4 : ℝ) * S) * ((2 : ℝ) * Real.pi * r / c) = Real.pi / (4 : ℝ) * r / c) ∧ ∀ (S : ℕ), (∀ (x : ℕ), (2 : ℕ) * x ≤ S ↔ x ≤ S / (2 : ℕ)) ∧ (Even S → (2 : ℕ) * (S / (2 : ℕ)) = S) :=816 And.intro @FRC.Entropy.octant_chart (@FRC.Entropy.closure_budget)817set_option linter.defProp false in818/-- 14:C6 (p14023) — The octant sector: $C_{8}\subset C_{4\dS}$ exists exactly when $\dS$ is even, its character $\zeta_8$ the residue the Tsirelson identity carries; the octant count $\dS/2$ is an integer on every admissible Carrier. -/819def p14023 := And.intro @FRC.Entropy.octant_exists_iff (@FRC.Entropy.octant_character)820/-- 14:C7 (p14024) — The dark-energy output: $\Omega_\Lambda=\tanh^{2}(3\pi/8)=0.6837$ \lcdm{} against the fitted $0.685\pm0.007$, a $0.19\sigma$ landing --- a zero-freedom derivation, not an independent measurement (two-register separation, \S\ref{sec:audit}). -/821theorem p14024 : (FRC.Entropy.lcdmAge (Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) = Real.pi / (4 : ℝ) ∧ ∀ (Ω : ℝ), (0 : ℝ) ≤ Ω → Ω < (1 : ℝ) → FRC.Entropy.lcdmAge Ω = Real.pi / (4 : ℝ) → Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) ∧ 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 :=822 And.intro @FRC.Entropy.octant_inversion (@FRC.Entropy.landing_bracket)823/-- 14:C8 (p14025) — The entailed-rate consistency: with the channel-1 $\Lambda$ the age--rate locus returns the channel-1 $H_0$ (to $0.1\%$), same-channel by the definition $\Lambda=3\Omega_\Lambda H_0^{2}/c^{2}$, a corollary of C7 and not a prediction --- the floor value itself consumed as import (A6) under the role realisation (B4), not derived here; the two-cluster ratio is the chart identity $(H_{\mathrm{rate}}/H_0)^2/\Omega_\Lambda$, displayed, not claimed. -/824theorem p14025 : (∀ (H0 c Ω Λ : ℝ), (0 : ℝ) < H0 → (0 : ℝ) < c → (0 : ℝ) ≤ Ω → Λ = (3 : ℝ) * Ω * H0 ^ (2 : ℕ) / c ^ (2 : ℕ) → c * √(Λ / (3 : ℝ)) = H0 * √Ω ∧ (H0 * √Ω / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) = H0 ↔ Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ))) ∧ ((1 : ℝ) < √0.685 / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ∧ √0.685 / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) < 1.001) ∧ ∀ (c H0 Hr Ω ℓ : ℝ), c ≠ (0 : ℝ) → (0 : ℝ) < Ω → ℓ ≠ (0 : ℝ) → Real.pi * (c / (H0 * √Ω) / ℓ) ^ (2 : ℕ) / (Real.pi * (c / Hr / ℓ) ^ (2 : ℕ)) = (Hr / H0) ^ (2 : ℕ) / Ω :=825 And.intro @FRC.Entropy.channel_one_consistency (And.intro @FRC.Entropy.channel_one_numeral (@FRC.Entropy.cluster_identity))826/-- 14:C9 (p14026) — The registrable triangle \apx: width $\log_{10}(r_H/\lP)=61.0$ dex --- the count face $\sqrt{\dS}$ in its chart dress $\sqrt{\dS/\pi}$, the solid angle the declared transport; the thirteen-object diagonal, slope $3.03$ (intercept $1.00\times10^{3}$ at the metre pivot); the constrained $k=3$ cubic coefficient $\tilde c=m/R^{3}=0.97\times10^{3}\,\mathrm{kg\,m^{-3}}$ (not a density: a sphere's is $0.62$ dex lower); the Compton entry returns its input, the Schwarzschild exit is the chart's one derived quantity, the over-closure bound $1.8\times10^{8}M_\odot$ within the $(1.4\text{--}2.8)\times10^{8}$ sensitivity band --- a bound, no observed scale predicted (X5); classified a consistency chart, not a channel. -/827theorem p14026 : ∀ (S x : ℝ), (0 : ℝ) < x → S = Real.pi * x ^ (2 : ℕ) → x = √(S / Real.pi) ∧ √S = √Real.pi * x :=828 @FRC.Entropy.count_face829/-- 14:C10 (p14027) — The capacity axis \apx: holographic ring capacity $\log_{10}\kap_{q}$, zero at hydrogen ($\kap_H=3$; $\kap_{q}=2$ has no shell), one dex per chart dex, terminating at the count face $\sqrt{\dS}$ --- the triangle's own sixty dex; the one-gram horizontal lands on $N_A$ to $0.0035$ dex (the $1.008$\,u offset), asserted before drawing. -/830theorem p14027 : Nat.Prime ((4 : ℕ) * (1 : ℕ) + (1 : ℕ)) ∧ ¬Nat.Prime ((4 : ℕ) * (2 : ℕ) + (1 : ℕ)) ∧ Nat.Prime ((4 : ℕ) * (3 : ℕ) + (1 : ℕ)) :=831 @FRC.Entropy.capacity_zero832/-- 14:X1 (p14028) — \textbf{The cosmological-constant problem} dissolves: $\Lambda$ is the curvature face of the one cardinality, not a vacuum energy, so there is no mode sum to cancel and the $10^{120}$-order discrepancy does not arise. -/833theorem p14028 : ∀ (Λ S r ℓ : ℝ), r ≠ (0 : ℝ) → ℓ ≠ (0 : ℝ) → Λ = (3 : ℝ) / r ^ (2 : ℕ) → S = Real.pi * (r / ℓ) ^ (2 : ℕ) → Λ * ℓ ^ (2 : ℕ) = (3 : ℝ) * Real.pi / S :=834 @FRC.Entropy.lambda_face835/-- 14:X2 (p14029) — \textbf{Milgrom's coincidence} $a_0\approx cH_0/2\pi$, on record since 1983, becomes a value with zero freedom: the $2\pi$ is the fixed cycle convention, the reverse rebooking of $h=2\pi\hbar$, and the $H$ is the observer's registered rate. -/836theorem p14029 : ∀ (c H ħ h : ℝ), h = (2 : ℝ) * Real.pi * ħ → ħ ≠ (0 : ℝ) → c * H / ((2 : ℝ) * Real.pi) = c * H * ħ / h :=837 @FRC.Entropy.milgrom_rebooking838/-- 14:X3 (p14030) — \textbf{The age coincidence} $t_0H_\Lambda\approx\pi/4$ becomes the octant: $\Omega_\Lambda=\tanh^{2}(3\pi/8)=0.6837$ \lcdm{} is an output of the realisation set, landing at $0.19\sigma$ on the fitted $0.685\pm0.007$ --- never an independent measurement of $\dS$ (same-channel, X6), a zero-freedom derivation in full standing; the $(\Lambda,H_0)$ entailment at the channel-1 $\Lambda$ is this same landing read on $H_0$, not a further prediction. -/839theorem p14030 : (FRC.Entropy.lcdmAge (Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) = Real.pi / (4 : ℝ) ∧ ∀ (Ω : ℝ), (0 : ℝ) ≤ Ω → Ω < (1 : ℝ) → FRC.Entropy.lcdmAge Ω = Real.pi / (4 : ℝ) → Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) ∧ 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 :=840 And.intro @FRC.Entropy.octant_inversion (@FRC.Entropy.landing_bracket)841set_option linter.defProp false in842/-- 14:X4 (p14031) — \textbf{The congruence $\dS$ even} acquires a second physical face: it is the existence of the octant sector, hence the well-definedness of the measured age --- a structure of the Carrier's cycle lattice, certified by realisation and read as an observational condition, never an arithmetic property of the numeral. -/843def p14031 := And.intro @FRC.Entropy.octant_second_face (@FRC.Entropy.octant_sector_iff)844/-- 14:X5 (p14032) — \textbf{The termination of the single-object sequence} is a consistency of the wall structure, the exit of C9 read as a bound: the typical-density diagonal over-closes at $1.8\times10^{8}M_\odot$ \apx{} (sensitivity band $(1.4\text{--}2.8)\times10^{8}$ across fit variants), so every heavier single object continuing the condensed-density sequence is necessarily wall-bound; the supermassive holes are that continuation, not an anomaly beyond it. Classified with the triangle: consistency, not derivation of an observed scale. -/845theorem p14032 : ∀ (M R G c ρ₀ : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < M → M = ρ₀ * R ^ (3 : ℕ) → R = (2 : ℝ) * G * M / c ^ (2 : ℕ) → (0 : ℝ) < ρ₀ ∧ M ^ (2 : ℕ) = c ^ (6 : ℕ) / ((8 : ℝ) * G ^ (3 : ℕ) * ρ₀) :=846 @FRC.Entropy.wall_exit847/-- 14:X6 (p14033) — \textbf{The celebrated sub-percent age agreement} is judged: same-channel by the circularity criterion, a restatement of the fitted dark-energy fraction --- consistency, not evidence --- and the criterion locates exactly which confrontations do carry weight. -/848theorem p14033 : (∀ (Ωm ΩΛ H0 t : ℝ), (0 : ℝ) < Ωm → (0 : ℝ) < ΩΛ → Ωm + ΩΛ = (1 : ℝ) → (0 : ℝ) < H0 → (0 : ℝ) < t → (FRC.Entropy.lcdmScale Ωm ΩΛ (H0 * √ΩΛ) t = (1 : ℝ) ↔ t * (H0 * √ΩΛ) = FRC.Entropy.lcdmAge ΩΛ)) ∧ FRC.Entropy.lcdmAge (Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) = Real.pi / (4 : ℝ) ∧ ∀ (Ω : ℝ), (0 : ℝ) ≤ Ω → Ω < (1 : ℝ) → FRC.Entropy.lcdmAge Ω = Real.pi / (4 : ℝ) → Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) :=849 And.intro @FRC.Entropy.lcdm_age (@FRC.Entropy.octant_inversion)850/-- 14:X7 (p14034) — \textbf{The universe-as-black-hole puzzle dissolves}: the Hubble radius sits on the black-hole line identically ($\rho_{\mathrm{BH}}(r_H)=\rho_c$ \lcdm), but the Schwarzschild reading consumes an exterior, and the containment argument (A3) makes an exterior incoherent --- the totality on its own horizon is the chart's closing point, not a hole in a background. -/851theorem p14034 : ∀ (c G H r : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < H → (0 : ℝ) < r → r * c ^ (2 : ℕ) / ((2 : ℝ) * G) / ((4 / 3 : ℝ) * Real.pi * r ^ (3 : ℕ)) = (3 : ℝ) * c ^ (2 : ℕ) / ((8 : ℝ) * Real.pi * G * r ^ (2 : ℕ)) ∧ c / H * c ^ (2 : ℕ) / ((2 : ℝ) * G) / ((4 / 3 : ℝ) * Real.pi * (c / H) ^ (3 : ℕ)) = (3 : ℝ) * H ^ (2 : ℕ) / ((8 : ℝ) * Real.pi * G) ∧ ((3 : ℝ) * c ^ (2 : ℕ) / ((8 : ℝ) * Real.pi * G * r ^ (2 : ℕ)) = (3 : ℝ) * H ^ (2 : ℕ) / ((8 : ℝ) * Real.pi * G) ↔ r = c / H) :=852 @FRC.Entropy.hubble_on_bh_line853/-- 14:X8 (p14035) — \textbf{The interior completions weighed}: black-hole cosmology keeps the same saturation identity by consuming a parent exterior and a singularity-replacing mechanism (torsion; exclusion pressure); the finite reading consumes neither: the containment argument (A3) closes the chart at $\Om$, and no singularity is available over a finite totality. The registered record-depth bound separates the completions empirically (P2). -/854theorem p14035 : (∀ (c G H r : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < H → (0 : ℝ) < r → r * c ^ (2 : ℕ) / ((2 : ℝ) * G) / ((4 / 3 : ℝ) * Real.pi * r ^ (3 : ℕ)) = (3 : ℝ) * c ^ (2 : ℕ) / ((8 : ℝ) * Real.pi * G * r ^ (2 : ℕ)) ∧ c / H * c ^ (2 : ℕ) / ((2 : ℝ) * G) / ((4 / 3 : ℝ) * Real.pi * (c / H) ^ (3 : ℕ)) = (3 : ℝ) * H ^ (2 : ℕ) / ((8 : ℝ) * Real.pi * G) ∧ ((3 : ℝ) * c ^ (2 : ℕ) / ((8 : ℝ) * Real.pi * G * r ^ (2 : ℕ)) = (3 : ℝ) * H ^ (2 : ℕ) / ((8 : ℝ) * Real.pi * G) ↔ r = c / H)) ∧ (∀ (S r c : ℝ), S ≠ (0 : ℝ) → S / (2 : ℝ) / ((4 : ℝ) * S) * ((2 : ℝ) * Real.pi * r / c) = Real.pi / (4 : ℝ) * r / c) ∧ (21e-4 * (Real.pi / (4 : ℝ)) < FRC.Entropy.lcdmAge 0.685 - Real.pi / (4 : ℝ) ∧ FRC.Entropy.lcdmAge 0.685 - Real.pi / (4 : ℝ) < 22e-4 * (Real.pi / (4 : ℝ))) ∧ 7e-2 < (1 : ℝ) / 13.79 ∧ (1 : ℝ) / 13.79 < 75e-3 :=855 And.intro @FRC.Entropy.hubble_on_bh_line (@FRC.Entropy.record_depth)856/-- 14:P1 (p14036) — \textbf{(Lead.)} The floor runs with the registered rate, $a_0(z)\propto H(z)$, the role statement of the floor closure, against both a constant fundamental $a_0$ and feedback-emergent scaling. Status: the constant-floor branch is excluded --- four redshift bins rising from $1.99$ to $2.71\times10^{-10}\,\mathrm{m/s^2}$ over $z=0.50$--$1.28$ \citep{ciocan2026}, $\Delta\chi^2=23$ against $A\,H(z)/H_0$ \lcdm{} --- and the running form fits the bins at free amplitude ($A=1.39\pm0.03$, $\chi^2=5.4/3$); the binned rate sits on the $\propto H(z)$ chord while the authors' global linear fit runs above it, so the shape waits on the likelihood refit of the resolved tracks, and the amplitude's $0.12$\,dex excess over $cH_0/2\pi$ lies inside the $0.2$\,dex gas systematic. Falsifier: a likelihood refit or a wider-redshift sample excluding the $\propto H(z)$ form after the baryonic-mass and pressure-support systematics close. -/857theorem p14036 : ∀ (A H0 Ωm ΩΛ z : ℝ), A ≠ (0 : ℝ) → H0 ≠ (0 : ℝ) → Ωm + ΩΛ = (1 : ℝ) → A * (H0 * √(Ωm * ((1 : ℝ) + z) ^ (3 : ℕ) + ΩΛ)) / ((2 : ℝ) * Real.pi) / (A * (H0 * √(Ωm * ((1 : ℝ) + (0 : ℝ)) ^ (3 : ℕ) + ΩΛ)) / ((2 : ℝ) * Real.pi)) = √(Ωm * ((1 : ℝ) + z) ^ (3 : ℕ) + ΩΛ) ∧ 1.79 < √(0.315 * ((1 : ℝ) + (1 : ℝ)) ^ (3 : ℕ) + 0.685) ∧ √(0.315 * ((1 : ℝ) + (1 : ℝ)) ^ (3 : ℕ) + 0.685) < 1.80 :=858 @FRC.Entropy.running_floor859/-- 14:P2 (p14037) — The registered record depth is bounded by $(\pi/4)\,r_H/c=13.79$ Gyr \apx{} (channel-1 anchor) at every observational frame chronon, against a $\Lambda$CDM $t_0$ that grows with chart time: degenerate to $0.2\%$ now, separating at ${\sim}7\%$ per Gyr; the octant carries zero parameter freedom at fixed $\Lambda$. Status \citep{valcin2026}: the oldest cluster population $0.5\sigma$ below the bound, the inferred age straddling it within $0.1\sigma$ (\S\ref{sec:open}). Falsifier: one well-dated object older than the octant value, in any frame --- fit-independent, fatal; the same bound excludes interior-bounce black-hole cosmology (X8). -/860theorem p14037 : (∀ (S r c : ℝ), S ≠ (0 : ℝ) → S / (2 : ℝ) / ((4 : ℝ) * S) * ((2 : ℝ) * Real.pi * r / c) = Real.pi / (4 : ℝ) * r / c) ∧ (21e-4 * (Real.pi / (4 : ℝ)) < FRC.Entropy.lcdmAge 0.685 - Real.pi / (4 : ℝ) ∧ FRC.Entropy.lcdmAge 0.685 - Real.pi / (4 : ℝ) < 22e-4 * (Real.pi / (4 : ℝ))) ∧ 7e-2 < (1 : ℝ) / 13.79 ∧ (1 : ℝ) / 13.79 < 75e-3 :=861 @FRC.Entropy.record_depth862/-- 14:P3 (p14038) — 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$). -/863theorem 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 :=864 @FRC.LedgerML.p14038865/-- 14:P4 (p14039) — \textbf{(Lead.)} The dark-energy equation of state is rigid: $\Lambda$ is the curvature face of the fixed cardinality, constant, its effective-fluid reading $w=-1$ exactly with no $w_0w_a$ freedom; the fluid statement consumes the conservation-law correspondence and the single-component clause (B8). Status: DESI-era combined fits prefer evolving dark energy at $3$--$4.2\sigma$ \citep{desi2025}, contested by reanalyses (\S\ref{sec:import}). Falsifier: confirmed evolution of $w$, which kills $\Lambda\sim1/\Om$ outright and exposes P2 through $\Lambda$. -/866theorem p14039 : ∀ (H ρ p ρ' : ℝ), H ≠ (0 : ℝ) → ρ ≠ (0 : ℝ) → ρ' = (0 : ℝ) → ρ' + (3 : ℝ) * H * (ρ + p) = (0 : ℝ) → p = -ρ ∧ p / ρ = (-1 : ℝ) :=867 @FRC.Entropy.fluid_w868-- end ledger predicates869870end FRC.Entropy871