Entropy.lean — FrcCore

1import FrcCore.Frame2import FrcCore.Orbit3import FrcCore.Instances4import FrcCore.Keys.Frame5import FrcCore.Theme.Quantum67/-!8# 14-entropy — the import's congruences, the octant sector and the laboratory Carrier, no axioms910The finite content of *De Sitter Entropy Estimates over Finite Holographic Substrate* (tree11`14-entropy-20260722`) from first principles: the quarter identity `Ω = 4S + 1 ⇒ Ω ≡ 1 (mod 4)`,12`Ω − 1 = 4S` (A1); the triality centre `S ≡ 1 (mod 3) ⇒ 3 ∣ Ω + 1`, `3 ∤ Ω − 1` (A2); the octant sector13`8 ∣ 4S ⟺ 2 ∣ S`, with `S = 2m` the cycle `8m`, its quarter `2m` and its octant `m` (C6, X4, B2); the closure14budget `2x ≤ 2m ⟺ x ≤ m` (C5); on every frame `(τ; 0, 1, g)` of even capacity `κ = 2m` the octant character15`ζ = g^m` — `ζ⁴ = −1`, `ζ⁸ = 1`, its inverse `g^{7m}`, the Tsirelson square `(ζ + ζ⁻¹)² = 2`,16`(2(ζ + ζ⁻¹))² = 8`, hence `2` a square on every such shell; and the converses — an element with `ζ⁴ = −1`,17`ζ⁸ = 1` forces the capacity even, and a square root `r` of `2` gives one, `ζ = (r + i r)/2` with `ζ² = i` —18so that, on every frame at tier 0, the octant sector exists ⟺ the capacity is even ⟺ `2` is a square: the19octant and the c-square are one condition (C6, X4); the nesting bound `q² < p`, `p² < Ω ⇒ q⁴ < Ω` (B10);20primality by trial division up to the square root; the additive window `|Σhᵢ| ≤ Σκᵢ`, attained, every total21occurring (B11), the lock of like units with recurrence `12` and its offset (B12), the shells of capacity `3N` and22the multiplicative fusion of coprime cycles (B13). Decided by the kernel: the octant on `𝔽₁₇` and its absence23on `𝔽₁₃` and `𝔽₂₉`, the characters `ζ₈` of the Carriers `233` and `2 408 561`; the laboratory Carrier —24`S = 602 140` even, `≡ 1 (mod 3)`, `4S + 1` prime (A2); the capacity axis `𝔽₅`, no shell at `κ = 2`, `𝔽₁₃` at25hydrogen, `12N + 1` prime at `N = 1, 3` and not at `N = 2` (C10, B10); the nesting `37 → 1373 → 2 408 561` and26the bound `N ≤ 3` on the laboratory Carrier (B10). The realisation premises of the octant lemma (A4, A5, B6,27B7) are outside this module: it decides the lemma's arithmetic. Every declaration is checked to depend on no28axiom (`check_core_axioms.py`).2930Since the ledger migration (task LM17) the octant character and its converse live in the frame theme (`Orbit.lean`)31and `isPrime` in `Nat.lean`; since task LM22 `isPrime_of_bounded` lives in `Nat.lean` too. Every old name stays as32an alias.33-/3435namespace FRC.Entropy3637open FRC.Shell3839section40open FRC.Shell.Frame (lit_mul add_one_add_one_neg even_capacity_powers octant_residue tsirelson_square two_is_square lit_add neg_one_ne_one neg_one_ne_zero octant_of_two_square even_of_order_eight even_capacity_of_octant octant_iff even_capacity_of_two_square two_is_square_iff)4142/-! ## The import and its congruences (14:A1, A2) -/43section congruences4445/-- 14:A1, 14:B9, 14:C2 — the quarter identity: `Ω = 4S + 1` has `Ω ≡ 1 (mod 4)` and `Ω − 1 = 4S`, so the import fixes the46cardinality exactly; the finite face of B9's area law `A = 4S`, and the integer face of C2's horizon-quarter closure47`(Ω − 1)/4 = S`. -/48theorem quarter_identity (S : Nat) : (4 * S + 1) % 4 = 1 ∧ 4 * S + 1 - 1 = 4 * S :=49  ⟨FRC.Nat.add_mul_mod_self_left 1 S 4 (Nat.zero_lt_succ 3), FRC.Nat.add_sub_cancel (4 * S) 1⟩5051/-- 14:A2 — the triality centre: `S ≡ 1 (mod 3)` gives `(Ω + 1) % 3 = 0` and `(Ω − 1) % 3 = 1`, so the centre52`3 ∣ Ω + 1` is carried and `3 ∤ 4S`. -/53theorem triality_residues (S : Nat) (h : S % 3 = 1) : (4 * S + 2) % 3 = 0 ∧ (4 * S) % 3 = 1 := by54  have h3 : 0 < 3 := Nat.zero_lt_succ 255  have h4S : (4 * S) % 3 = 1 := by56    rw [FRC.Nat.mul_mod 4 S 3 h3, h]57  refine ⟨?_, h4S⟩58  rw [FRC.Nat.add_mod (4 * S) 2 3 h3, h4S]5960/-- 14:C6, 14:X4 — the octant sector `C₈ ⊂ C_{4S}` exists (`8 ∣ 4S`) exactly when `S` is even. -/61theorem octant_divides (S : Nat) : (∃ k, 4 * S = 8 * k) ↔ (∃ m, S = 2 * m) := by62  constructor63  · rintro ⟨k, hk⟩64    refine ⟨k, Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ 3) ?_⟩65    rw [hk, ← FRC.Nat.mul_assoc]66  · rintro ⟨m, hm⟩67    exact ⟨m, by rw [hm, ← FRC.Nat.mul_assoc]⟩6869/-- 14:B2, 14:C5 — the dictionary on the count face: the full cycle is `4S` (`2π`); the half-cycle `2S` (`π`)70twice over is the cycle, and with `S = 2m` the octant `m = S/2` (`π/4`) eight times over is the cycle — an71integer count on every admissible Carrier. -/72theorem octant_count (S m : Nat) (h : S = 2 * m) : 2 * (2 * S) = 4 * S ∧ 8 * m = 4 * S :=73  ⟨by rw [← FRC.Nat.mul_assoc], by rw [h, ← FRC.Nat.mul_assoc]⟩7475/-- 14:C5, 14:B6 — the closure count: given B6's accounting (a two-way registration of depth `x` costs `2x` of76the one-way budget `S = 2m`; the realisation, not formalised), the closable depths are exactly `x ≤ m`, and the77octant `x = m` closes the budget. -/78theorem closure_count (m x : Nat) : 2 * x ≤ 2 * m ↔ x ≤ m := by79  constructor80  · intro h81    match Nat.lt_or_ge m x with82    | .inr hle => exact hle83    | .inl hlt =>84      have : m * 2 < x * 2 := FRC.Nat.mul_lt_mul_of_lt_of_pos hlt (Nat.zero_lt_succ 1)85      rw [Nat.mul_comm m 2, Nat.mul_comm x 2] at this86      exact absurd (Nat.lt_of_lt_of_le this h) (Nat.lt_irrefl _)87  · intro h; exact Nat.mul_le_mul_left 2 h8889end congruences9091/-! ## The nesting bound and trial division (14:B10) -/92section nesting9394/-- 14:B10 — the nesting bound, the necessity direction: a shell `q` registered whole by a Subject `p` of the95Carrier `Ω` (`q² < p`, `p² < Ω`) has `q⁴ < Ω`; for `q = 12N + 1` this bounds the hydrogen count `N`; a Subject96between the two is exhibited on the laboratory Carrier (`lab_nesting`, `p = 1373`). -/97theorem nesting_bound (q p Ω : Nat) (hq : q * q < p) (hp : p * p < Ω) : q * q * (q * q) < Ω := by98  have hp0 : 0 < p := FRC.Nat.pos_of_lt hq99  have h1 : q * q * (q * q) < p * p := by100    match Nat.lt_or_ge 0 (q * q) with101    | .inl hpos =>102      have ha : q * q * (q * q) < p * (q * q) := FRC.Nat.mul_lt_mul_of_lt_of_pos hq hpos103      have hb : q * q * p < p * p := FRC.Nat.mul_lt_mul_of_lt_of_pos hq hp0104      rw [Nat.mul_comm (q * q) p] at hb105      exact Nat.lt_trans ha hb106    | .inr hz =>107      have h0 : q * q = 0 := Nat.le_antisymm hz (Nat.zero_le _)108      rw [h0]; exact Nat.mul_pos hp0 hp0109  exact Nat.lt_trans h1 hp110111/-- Trial division up to `B` decides primality when `n < (B + 1)²`: a divisor `d ≥ 2` of `n` with112`d > B` has a cofactor `q = n/d` with `2 ≤ q ≤ B`, itself a divisor. Since task LM22 the base theme's113`FRC.Nat.isPrime_of_bounded`, under its old name. -/114theorem isPrime_of_bounded (n B : Nat) (h2 : 2 ≤ n) (hB : n < (B + 1) * (B + 1))115    (hd : ∀ d, d < B + 1 → 2 ≤ d → n % d ≠ 0) : FRC.Nat.isPrime n :=116  FRC.Nat.isPrime_of_bounded n B h2 hB hd117118end nesting119120/-! ## The values decided by the kernel (14:A2, C6, C10, B10) -/121section values122123/-- 14:C6, 14:X4 — the octant on `𝔽₁₇` (`κ = 4`, `g = 3`): `ζ = 3² = 9` has `9⁴ = −1`, `9⁸ = 1`,124`ζ⁻¹ = 2`, `(9 + 2)² = 2`, `(2 · 11)² = 8`; on `𝔽₁₃` (`κ = 3`) and `𝔽₂₉` (`κ = 7`) no residue has `x⁴ = −1`,125and `2` is not a square. -/126theorem octant17 :127    (9 : Shell 17) = 3 ^ 2 ∧ (9 : Shell 17) ^ 4 = -1 ∧ (9 : Shell 17) ^ 8 = 1 ∧ (9 : Shell 17) * 2 = 1 ∧128    ((9 : Shell 17) + 2) ^ 2 = 2 ∧ (2 * ((9 : Shell 17) + 2)) ^ 2 = 8 ∧129    (∀ x : Shell 13, x ^ 4 ≠ -1) ∧ (∀ x : Shell 13, x * x ≠ 2) ∧130    (∀ x : Shell 29, x ^ 4 ≠ -1) ∧ (∀ x : Shell 29, x * x ≠ 2) := by decide +kernel131132/-- 14:C6 — an octant character of the Carrier `Ω = 233` (`S = 58` even), host-decided in the chart with drive133`3`: `ζ₈ = 3²⁹ = 221`, `ζ₈⁴ = −1`, `ζ₈⁸ = 1`, `ζ₈⁻¹ = 97`, `(ζ₈ + ζ₈⁻¹)² = 2`, `(2(ζ₈ + ζ₈⁻¹))² = 8`. -/134theorem octant233 :135    (221 : Shell 233) ^ 4 = -1 ∧ (221 : Shell 233) ^ 8 = 1 ∧ (221 : Shell 233) * 97 = 1 ∧136    ((221 : Shell 233) + 97) ^ 2 = 2 ∧ (2 * ((221 : Shell 233) + 97)) ^ 2 = 8 := by decide +kernel137138/-- 14:A2, 14:C6 — the laboratory Carrier `Ω = 2 408 561`, host-decided values: `4S + 1 = Ω` with139`S = 602 140` even and `≡ 1 (mod 3)`, the octant sector realised — in the chart with drive `6`,140`ζ₈ = 6³⁰¹⁰⁷⁰ = 1 639 587`, `ζ₈⁴ = −1`, `ζ₈⁸ = 1`, `ζ₈⁻¹ = 1 111 186`, `(ζ₈ + ζ₈⁻¹)² = 2`,141`(2(ζ₈ + ζ₈⁻¹))² = 8`. -/142theorem lab_carrier :143    4 * 602140 + 1 = 2408561 ∧ 602140 % 2 = 0 ∧ 602140 % 3 = 1 ∧144    (1639587 : Shell 2408561) ^ 4 = -1 ∧ (1639587 : Shell 2408561) ^ 8 = 1 ∧145    (1639587 : Shell 2408561) * 1111186 = 1 ∧ ((1639587 : Shell 2408561) + 1111186) ^ 2 = 2 ∧146    (2 * ((1639587 : Shell 2408561) + 1111186)) ^ 2 = 8 := by decide +kernel147148/-- 14:A2 — the laboratory Carrier is prime: `2 408 561 < 1553²`, and no `d ≤ 1552` divides it. -/149theorem carrierLab_prime : FRC.Nat.isPrime 2408561 :=150  isPrime_of_bounded 2408561 1552 (by decide) (by decide) (by decide +kernel)151152/-- 14:C10, 14:B10 — the primality behind the capacity axis: `κ = 1` (the bare proton) is the shell `𝔽₅`, `κ = 2`153has no shell (`9` composite), `κ_H = 3` (hydrogen, `N = 1`) is `𝔽₁₃`; the `3N` shell at `N = 3` (`37`), none at154`N = 2` (`25`). -/155theorem capacity_axis :156    FRC.Nat.isPrime 5 ∧ ¬ FRC.Nat.isPrime 9 ∧ FRC.Nat.isPrime (12 * 1 + 1) ∧157    ¬ FRC.Nat.isPrime (12 * 2 + 1) ∧ FRC.Nat.isPrime (12 * 3 + 1) := by decide +kernel158159/-- 14:B10 — the nesting on the laboratory Carrier: the capacity-`9` shell `q = 37` nests through the Subject160`p = 1373 = 4 · 343 + 1`, prime (`1373 < 38²`, no `d ≤ 37` divides it), `37² < 1373`, `1373² < Ω`; and the bound161`N ≤ 3`: `37⁴ < Ω < 49⁴`. -/162theorem lab_nesting :163    FRC.Nat.isPrime 1373 ∧ 1373 = 4 * 343 + 1 ∧ 37 * 37 < 1373 ∧ 1373 * 1373 < 2408561 ∧164    37 * 37 * (37 * 37) < 2408561 ∧ 2408561 < 49 * 49 * (49 * 49) :=165  ⟨isPrime_of_bounded 1373 37 (by decide) (by decide) (by decide +kernel), by decide, by decide,166    by decide, by decide, by decide⟩167168end values169170/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/171end172173section aliases174variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}175176/-- `a b (c d) = a c (b d)` on every shell. -/177theorem mul_mul_mul_comm (a b c d : Shell p) : a * b * (c * d) = a * c * (b * d) :=178  FRC.Shell.mul_mul_mul_comm a b c d179180/-- Literals multiply as their values: `a · b = ab` on every shell. -/181theorem lit_mul (a b : Nat) : (OfNat.ofNat a : Shell p) * OfNat.ofNat b = (OfNat.ofNat (a * b) : Shell p) :=182  FRC.Shell.Frame.lit_mul a b183184/-- `a + 1 + (1 − a) = 2` on every shell. -/185theorem add_one_add_one_neg (a : Shell p) : a + 1 + (1 + -a) = 2 :=186  FRC.Shell.Frame.add_one_add_one_neg a187188/-- On a frame of capacity `κ = 2m`: `g^{4m} = −1` (the half-period) and `g^{8m} = 1`. -/189theorem even_capacity_powers (F : Frame p κ g) (m : Nat) (hm : κ = 2 * m) :190    g ^ (4 * m) = -1 ∧ g ^ (8 * m) = 1 :=191  FRC.Shell.Frame.even_capacity_powers F m hm192193/-- 14:C6 — the octant character: on every frame `(τ; 0, 1, g)` of even capacity `κ = 2m`, `ζ = g^m` has194`ζ⁴ = −1` and `ζ⁸ = 1` — the sector `C₈ ⊂ C_{4κ}` is realised and `ζ` is its residue `ζ₈`. -/195theorem octant_residue (F : Frame p κ g) (m : Nat) (hm : κ = 2 * m) :196    (g ^ m) ^ 4 = -1 ∧ (g ^ m) ^ 8 = 1 :=197  FRC.Shell.Frame.octant_residue F m hm198199/-- 14:C6, 14:X4 — the Tsirelson square: with `ζ = g^m` and `ζ' = g^{7m}` its inverse (`ζζ' = 1`),200`(ζ + ζ')² = 2` and `(2(ζ + ζ'))² = 8` on every frame of capacity `κ = 2m`; hence `2` is a square on every201such shell — the direction "octant ⇒ c-square" of X4's second face (the converse is202`even_capacity_of_two_square` below; the equivalence `two_is_square_iff`). -/203theorem tsirelson_square (F : Frame p κ g) (m : Nat) (hm : κ = 2 * m) :204    g ^ m * g ^ (7 * m) = 1 ∧ (g ^ m + g ^ (7 * m)) ^ 2 = 2 ∧205    (2 * (g ^ m + g ^ (7 * m))) ^ 2 = 8 :=206  FRC.Shell.Frame.tsirelson_square F m hm207208/-- 14:X4 — the direction "even capacity ⇒ `2` a square" at tier 0: on every frame of even capacity `2` is a209square, `(ζ + ζ⁻¹)² = 2`; the converse is `even_capacity_of_two_square`, the equivalence `two_is_square_iff`. -/210theorem two_is_square (F : Frame p κ g) (m : Nat) (hm : κ = 2 * m) : ∃ r : Shell p, r * r = 2 :=211  FRC.Shell.Frame.two_is_square F m hm212213/-- Literals add as their values: `a + b = (a + b)` on every shell. -/214theorem lit_add (a b : Nat) : (OfNat.ofNat a : Shell p) + OfNat.ofNat b = (OfNat.ofNat (a + b) : Shell p) :=215  FRC.Shell.Frame.lit_add a b216217/-- `−1 ≠ 1` on every frame (`2 ≠ 0`). -/218theorem neg_one_ne_one (F : Frame p κ g) : (-1 : Shell p) ≠ 1 :=219  FRC.Shell.Frame.neg_one_ne_one F220221/-- `−1 ≠ 0` on every frame. -/222theorem neg_one_ne_zero (F : Frame p κ g) : (-1 : Shell p) ≠ 0 :=223  FRC.Shell.Frame.neg_one_ne_zero F224225/-- A square root of `2` gives a square root of the quarter-turn: with `i² = −1`, `2h = 1` and `r² = 2`,226`ζ = (r + i r) h` has `ζ² = i`, hence `ζ⁴ = −1` and `ζ⁸ = 1` — an element of order eight wherever `−1 ≠ 1`,227that is on every frame. -/228theorem octant_of_two_square {r i h : Shell p} (hr : r * r = 2) (hi : i * i = -1)229    (hh : 2 * h = 1) :230    ∃ ζ : Shell p, ζ * ζ = i ∧ ζ ^ 4 = -1 ∧ ζ ^ 8 = 1 :=231  FRC.Shell.Frame.octant_of_two_square hr hi hh232233/-- The arithmetic of the order: `(k · 8) % 4κ = 0` and `(k · 4) % 4κ ≠ 0` force `κ` even (a divisor `4κ` of234`8k` that misses `4k` cannot be `4 · odd`; `0 < κ` is only what `mod_spec` needs). -/235theorem even_of_order_eight {κ k : Nat} (hκ : 0 < κ) (h8 : (k * 8) % (4 * κ) = 0)236    (h4 : (k * 4) % (4 * κ) ≠ 0) : ∃ m, κ = 2 * m :=237  FRC.Shell.Frame.even_of_order_eight hκ h8 h4238239/-- 14:C6 — the octant forces even capacity: on every frame, an element `ζ` with `ζ⁴ = −1` and `ζ⁸ = 1` (an240element of order eight) gives `8 ∣ 4κ`, so the capacity is even. -/241theorem even_capacity_of_octant (F : Frame p κ g) {ζ : Shell p} (hz4 : ζ ^ 4 = -1) (hz8 : ζ ^ 8 = 1) :242    ∃ m, κ = 2 * m :=243  FRC.Shell.Frame.even_capacity_of_octant F hz4 hz8244245/-- 14:C6 — the octant sector at tier 0, as an equivalence: on every frame, an element with `ζ⁴ = −1` and246`ζ⁸ = 1` exists exactly when the capacity is even. -/247theorem octant_iff (F : Frame p κ g) : (∃ ζ : Shell p, ζ ^ 4 = -1 ∧ ζ ^ 8 = 1) ↔ ∃ m, κ = 2 * m :=248  FRC.Shell.Frame.octant_iff F249250/-- 14:X4 — the converse of the second face at tier 0: on every frame, a square root of `2` forces the251capacity even — `ζ = (r + i r)/2` has `ζ² = i`, so an element of order eight exists and `8 ∣ 4κ`. -/252theorem even_capacity_of_two_square (F : Frame p κ g) {r : Shell p} (hr : r * r = 2) :253    ∃ m, κ = 2 * m :=254  FRC.Shell.Frame.even_capacity_of_two_square F hr255256/-- 14:X4 — the second face as an equivalence at tier 0: on every frame `(τ; 0, 1, g)`, `2` is a square257exactly when the capacity is even — the c-square congruence and the octant sector are one condition. -/258theorem two_is_square_iff (F : Frame p κ g) : (∃ r : Shell p, r * r = 2) ↔ ∃ m, κ = 2 * m :=259  FRC.Shell.Frame.two_is_square_iff F260261end aliases262263/-! ## 14:B11–B13 — the additive window, the lock of like units, the shells of capacity `3N` (master F7, returned26415 October 2026). Heights `hᵢ` with `|hᵢ| ≤ κᵢ` are read as `uᵢ = hᵢ + κᵢ ≤ 2κᵢ`, so that the window `|Σhᵢ| ≤ Σκᵢ` is265`Σuᵢ ≤ 2Σκᵢ` and "every total occurs" is "every `s ≤ 2Σκᵢ` is a sum": the statements stay in `Nat`, with no axiom. -/266267section window268269/-- The total of the modes `u 0, …, u (m − 1)` (as the quantum theme's `prodN`, for sums). -/270def sumN (u : Nat → Nat) : Nat → Nat271  | 0 => 0272  | m + 1 => sumN u m + u m273274theorem sumN_congr (u v : Nat → Nat) : ∀ m, (∀ j, j < m → u j = v j) → sumN u m = sumN v m275  | 0, _ => rfl276  | m + 1, h => by277    show sumN u m + u m = sumN v m + v m278    rw [sumN_congr u v m (fun j hj => h j (Nat.lt_succ_of_lt hj)), h m (Nat.lt_succ_self m)]279280theorem sumN_mul (c : Nat) (κ : Nat → Nat) : ∀ m, sumN (fun j => c * κ j) m = c * sumN κ m281  | 0 => (Nat.mul_zero c).symm282  | m + 1 => by283    show sumN (fun j => c * κ j) m + c * κ m = c * (sumN κ m + κ m)284    rw [sumN_mul c κ m, Nat.mul_add]285286/-- 14:B11 — the additive window, the bound: `m` modes at heights `uᵢ ≤ 2κᵢ` total at most `2Σκᵢ`287(`|Σhᵢ| ≤ Σκᵢ` for `hᵢ = uᵢ − κᵢ`). -/288theorem additive_window_bound (u κ : Nat → Nat) : ∀ m, (∀ j, j < m → u j ≤ 2 * κ j) → sumN u m ≤ 2 * sumN κ m289  | 0, _ => Nat.le_refl 0290  | m + 1, h => by291    show sumN u m + u m ≤ 2 * (sumN κ m + κ m)292    rw [Nat.mul_add]293    exact Nat.add_le_add (additive_window_bound u κ m (fun j hj => h j (Nat.lt_succ_of_lt hj))) (h m (Nat.lt_succ_self m))294295/-- 14:B11 — the window is attained: the heights `uᵢ = 2κᵢ` (`hᵢ = κᵢ`) total `2Σκᵢ`. -/296theorem additive_window_attained (κ : Nat → Nat) (m : Nat) : sumN (fun j => 2 * κ j) m = 2 * sumN κ m :=297  sumN_mul 2 κ m298299/-- 14:B11 — every total occurs: for every `s ≤ 2Σκᵢ` there are heights `uᵢ ≤ 2κᵢ` with `Σuᵢ = s` — the last300height `s` itself when `s ≤ 2κ_m`, else `2κ_m` with the rest by induction. -/301theorem additive_window_every (κ : Nat → Nat) :302    ∀ m s, s ≤ 2 * sumN κ m → ∃ u : Nat → Nat, (∀ j, j < m → u j ≤ 2 * κ j) ∧ sumN u m = s303  | 0, s, hs => ⟨fun _ => 0, fun j hj => absurd hj (Nat.not_lt_zero j), (Nat.eq_zero_of_le_zero hs).symm⟩304  | m + 1, s, hs => by305    have hs' : s ≤ 2 * sumN κ m + 2 * κ m := by306      have e : 2 * sumN κ (m + 1) = 2 * sumN κ m + 2 * κ m := Nat.mul_add 2 (sumN κ m) (κ m)307      exact e ▸ hs308    match Nat.lt_or_ge (2 * κ m) s with309    | .inr hle =>310      obtain ⟨u', hu', hsum'⟩ := additive_window_every κ m 0 (Nat.zero_le _)311      refine ⟨fun j => if j = m then s else u' j, ?_, ?_⟩312      · intro j hj313        match Nat.decEq j m with314        | isTrue e => show (if j = m then s else u' j) ≤ 2 * κ j; rw [if_pos e, e]; exact hle315        | isFalse ne =>316          show (if j = m then s else u' j) ≤ 2 * κ j317          rw [if_neg ne]; exact hu' j (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) ne)318      · show sumN (fun j => if j = m then s else u' j) m + (if m = m then s else u' m) = s319        rw [if_pos rfl, sumN_congr (fun j => if j = m then s else u' j) u' m (fun j hj => if_neg (Nat.ne_of_lt hj)),320          hsum']321        exact Nat.zero_add s322    | .inl hlt =>323      obtain ⟨s', hs'eq⟩ := Nat.le.dest (Nat.le_of_lt hlt)324      have hs'le : s' ≤ 2 * sumN κ m := by325        apply FRC.Nat.le_of_add_le_add_left (a := 2 * κ m)326        rw [hs'eq]327        exact Nat.le_trans hs' (Nat.le_of_eq (Nat.add_comm _ _))328      obtain ⟨u', hu', hsum'⟩ := additive_window_every κ m s' hs'le329      refine ⟨fun j => if j = m then 2 * κ m else u' j, ?_, ?_⟩330      · intro j hj331        match Nat.decEq j m with332        | isTrue e => show (if j = m then 2 * κ m else u' j) ≤ 2 * κ j; rw [if_pos e, e]; exact Nat.le_refl _333        | isFalse ne =>334          show (if j = m then 2 * κ m else u' j) ≤ 2 * κ j335          rw [if_neg ne]; exact hu' j (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) ne)336      · show sumN (fun j => if j = m then 2 * κ m else u' j) m + (if m = m then 2 * κ m else u' m) = s337        rw [if_pos rfl, sumN_congr (fun j => if j = m then 2 * κ m else u' j) u' m (fun j hj => if_neg (Nat.ne_of_lt hj)),338          hsum', Nat.add_comm]339        exact hs'eq340341/-- 14:B11 — the additive window as one statement: the bound, its attainment and every total in the range342(heights read as `uᵢ = hᵢ + κᵢ ≤ 2κᵢ`). -/343theorem additive_window :344    (∀ (u κ : Nat → Nat) (m : Nat), (∀ j, j < m → u j ≤ 2 * κ j) → sumN u m ≤ 2 * sumN κ m) ∧345    (∀ (κ : Nat → Nat) (m : Nat), sumN (fun j => 2 * κ j) m = 2 * sumN κ m) ∧346    (∀ (κ : Nat → Nat) (m s : Nat), s ≤ 2 * sumN κ m →347      ∃ u : Nat → Nat, (∀ j, j < m → u j ≤ 2 * κ j) ∧ sumN u m = s) :=348  ⟨additive_window_bound, additive_window_attained, additive_window_every⟩349350/-- 14:B11 — hydrogen units: `N` modes of capacity `3` have the window `3N` (`2 · 3N` in the shifted reading);351on the hydrogen shell `𝔽₁₃` two heights `≤ 3` sum to at most `6 = 2κ` (38:A8), and three can exceed it,352`3 + 3 + 3 = 9 > 6` — the window grows with `N`. -/353theorem additive_window_hydrogen :354    (∀ N : Nat, sumN (fun _ => 2 * 3) N = 2 * (3 * N)) ∧355    (∀ u, u < 7 → ∀ v, v < 7 → u + v ≤ 12) ∧ 6 + 6 + 6 > 12 := by356  refine ⟨fun N => ?_, by decide, by decide⟩357  have e := sumN_mul 2 (fun _ => 3) N358  rw [e]359  have h3 : ∀ n, sumN (fun _ => 3) n = 3 * n := fun n => by360    induction n with361    | zero => rfl362    | succ k ih => show sumN (fun _ => 3) k + 3 = 3 * (k + 1); rw [ih, Nat.mul_succ]363  rw [h3]364365end window366367section lock368369/-- 14:B12 — the lock of like units: `m ≥ 1` cycles of period `12` return jointly exactly at the multiples of370`12` (the quantum theme's `Joint`), so the joint recurrence is `12` for every `m` and no element has order `12m`371for `m ≥ 2`. -/372theorem lock_recurrence (m : Nat) (hm : 0 < m) (t : Nat) :373    FRC.Quantum.Joint (fun _ => 12) m t ↔ t % 12 = 0 :=374  ⟨fun h => h 0 hm, fun h _ _ => h⟩375376/-- 14:B12 — the instances on the lock `C₁₂ × C₁₂`: the diagonal drive `(x, y) ↦ (x + 1, y + 1)` returns every377point after `12` steps, `x + 12 = x`, and not before, `x + k ≠ x` for `0 < k < 12`; it keeps the offset,378`(x + 1) − (y + 1) = x − y` (one superselected `C₁₂` offset per further unit); so the `144` points fall into `12`379orbits of length `12`, and the `1728` points of `C₁₂³` into `144`. -/380theorem lock_orbits :381    (∀ x : Shell 12, x + 12 = x) ∧382    (∀ x : Shell 12, ∀ k, k < 12 → 0 < k → x + FRC.Shell.ofNat k ≠ x) ∧383    (∀ x : Shell 12, ∀ y : Shell 12, (x + 1) + -(y + 1) = x + -y) ∧ 144 = 12 * 12 ∧ 1728 = 144 * 12 := by384  refine ⟨by decide +kernel, by decide +kernel, by decide +kernel, by decide, by decide⟩385386end lock387388section shells389390/-- 14:B13 — the shell of capacity `3N` is `𝔽_{12N+1}`, `4 · 3N + 1 = 12N + 1`; below `N = 10` it exists exactly for391`N = 1, 3, 5, 6, 8, 9` (`12N + 1` prime), and not at `N = 2` (`25 = 5²`), `4`, `7`. -/392theorem shells_of_capacity :393    (∀ N : Nat, 4 * (3 * N) + 1 = 12 * N + 1) ∧394    (∀ N : Nat, N < 10 → (FRC.Nat.isPrime (12 * N + 1) ↔ N = 1 ∨ N = 3 ∨ N = 5 ∨ N = 6 ∨ N = 8 ∨ N = 9)) ∧395    25 = 5 * 5 := by396  refine ⟨fun N => ?_, ?_, by decide⟩397  · rw [← FRC.Nat.mul_assoc]398  · intro N hN399    match N, hN with400    | 0, _ => decide +kernel401    | 1, _ => decide +kernel402    | 2, _ => decide +kernel403    | 3, _ => decide +kernel404    | 4, _ => decide +kernel405    | 5, _ => decide +kernel406    | 6, _ => decide +kernel407    | 7, _ => decide +kernel408    | 8, _ => decide +kernel409    | 9, _ => decide +kernel410    | n + 10, h => exact absurd (Nat.lt_of_lt_of_le h (Nat.le_add_left 10 n)) (Nat.lt_irrefl _)411412/-- 14:B13 — fusion of coprime cycles is multiplicative, the instances: hydrogen `(4, 3)` returns jointly exactly413at the multiples of `12 = 4 · 3` (searched below `24`), the diagonal drive on `C₄ × C₃` is one orbit of length `12`414(the twelve points `(k, k)`, `k < 12`, distinct), and the fused capacity is `4 · 3 / 4 = 3`; like cycles do not415fuse — `(12, 12)` returns at the multiples of `12`, `gcd (12, 12) = 12` — and the capacity-`3` shell `13` is not416the lock's register `12`. The general law, `lcm (n₁, n₂) = n₁ n₂` for coprime cycles, is the Mathlib declaration. -/417theorem fusion_capacity :418    (∀ t, t < 24 → (FRC.Quantum.Joint (fun j => if j = 0 then 4 else 3) 2 t ↔ t % 12 = 0)) ∧419    (∀ k, k < 12 → ∀ k', k' < 12 →420      (FRC.Shell.ofNat k : Shell 4) = FRC.Shell.ofNat k' → (FRC.Shell.ofNat k : Shell 3) = FRC.Shell.ofNat k' → k = k') ∧421    4 * 3 / 4 = 3 ∧ Nat.lcm 4 3 = 12 ∧422    (∀ t, t < 24 → (FRC.Quantum.Joint (fun _ => 12) 2 t ↔ t % 12 = 0)) ∧ Nat.gcd 12 12 = 12 ∧ (13 : Nat) ≠ 12 :=423  ⟨by decide +kernel, by decide +kernel, by decide, by decide, by decide +kernel, by decide, by decide⟩424425end shells426427/-! ## The concordance in integers (14:C4) -/428section concordance429430/-- 14:C4 [approx] — the concordance as integer arithmetic: the five evidence readings of `r_H` (rows 1, 2a, 2b, 3,4314b of the instrument table) are `166, 127, 133, 119, 164` in units of `10²⁴ m`, the gauge reading 4a (`129`) displayed432and excluded; the count face `√S = √π · r_H/ℓ_P` is monotone in `r_H`, so rows 1 and 3 are the extremes. Clauses:433the five lie in `[119, 166]`; the half-range `(166 − 119)/(166 + 119)` lies in `(16 %, 17 %)`, the paper's `±17 %`;434the full-range factor on `S`, `(166/119)²`, lies in `(1.9, 2.0)`, the paper's `1.9`; with `ℓ_P = 1.616255 × 10⁻³⁵ m`435the two extremes of `r_H/ℓ_P` lie in `(7.36, 7.37) × 10⁶⁰` and `(10.27, 10.28) × 10⁶⁰`; with `√π ∈ (1.772, 1.773)`436(`1772² < 3 141 592 < 3 141 593 < 1773²`) the count face lies in `(1.30, 1.31) × 10⁶¹` and `(1.80, 1.83) × 10⁶¹`,437the paper's `√S = (1.3–1.8) × 10⁶¹`. The readings, `ℓ_P` and `π` are chart data (taken as given); the arithmetic is438decided. -/439theorem concordance :440    (119 ≤ 127 ∧ 127 ≤ 166 ∧ 119 ≤ 133 ∧ 133 ≤ 166 ∧ 119 ≤ 164 ∧ 164 ≤ 166) ∧441    (16 * (166 + 119) < 100 * (166 - 119) ∧ 100 * (166 - 119) < 17 * (166 + 119)) ∧442    (19 * (119 * 119) < 10 * (166 * 166) ∧ 10 * (166 * 166) < 20 * (119 * 119)) ∧443    (736 * 1616255 < 1190 * 1000000 ∧ 1190 * 1000000 < 737 * 1616255 ∧444      1027 * 1616255 < 1660 * 1000000 ∧ 1660 * 1000000 < 1028 * 1616255) ∧445    (1772 * 1772 < 3141592 ∧ 3141593 < 1773 * 1773) ∧446    (1300000 < 1772 * 736 ∧ 1773 * 737 < 1310000 ∧ 1800000 < 1772 * 1027 ∧ 1773 * 1028 < 1830000) := by447  decide448449end concordance450451-- Ledger predicates of 14-entropy (generated by make_predicates.py from docs/14-entropy/14-entropy-ledger.json; edit the ledger, not this section)452/-- 14:A1 (p14001) — The de Sitter entropy $\dS$, the single quantitative import, fixing the cardinality exactly, $\Om=4\dS+1$. -/453theorem p14001 : ∀ (S : Nat), ((4 : Nat) * S + (1 : Nat)) % (4 : Nat) = (1 : Nat) ∧ (4 : Nat) * S + (1 : Nat) - (1 : Nat) = (4 : Nat) * S :=454  @FRC.Entropy.quarter_identity455/-- 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. -/456theorem p14002 : FRC.Nat.isPrime (2408561 : Nat) :=457  @FRC.Entropy.carrierLab_prime458/-- 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). -/459theorem p14010 : ∀ (S m : Nat), S = (2 : Nat) * m → (2 : Nat) * ((2 : Nat) * S) = (4 : Nat) * S ∧ (8 : Nat) * m = (4 : Nat) * S :=460  @FRC.Entropy.octant_count461/-- 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. -/462theorem p14017 : ∀ (S : Nat), ((4 : Nat) * S + (1 : Nat)) % (4 : Nat) = (1 : Nat) ∧ (4 : Nat) * S + (1 : Nat) - (1 : Nat) = (4 : Nat) * S :=463  @FRC.Entropy.quarter_identity464/-- 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. -/465theorem p14044 : (∀ (q p Ω : Nat), q * q < p → p * p < Ω → q * q * (q * q) < Ω) ∧ FRC.Nat.isPrime (1373 : Nat) ∧ (1373 : Nat) = (4 : Nat) * (343 : Nat) + (1 : Nat) ∧ (37 : Nat) * (37 : Nat) < (1373 : Nat) ∧ (1373 : Nat) * (1373 : Nat) < (2408561 : Nat) ∧ (37 : Nat) * (37 : Nat) * ((37 : Nat) * (37 : Nat)) < (2408561 : Nat) ∧ (2408561 : Nat) < (49 : Nat) * (49 : Nat) * ((49 : Nat) * (49 : Nat)) :=466  And.intro @FRC.Entropy.nesting_bound (@FRC.Entropy.lab_nesting)467/-- 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). -/468theorem p14046 : ((∀ (u κ : Nat → Nat) (m : Nat), (∀ (j : Nat), j < m → u j ≤ (2 : Nat) * κ j) → FRC.Entropy.sumN u m ≤ (2 : Nat) * FRC.Entropy.sumN κ m) ∧ (∀ (κ : Nat → Nat) (m : Nat), FRC.Entropy.sumN (fun j => (2 : Nat) * κ j) m = (2 : Nat) * FRC.Entropy.sumN κ m) ∧ ∀ (κ : Nat → Nat) (m s : Nat), s ≤ (2 : Nat) * FRC.Entropy.sumN κ m → ∃ u, (∀ (j : Nat), j < m → u j ≤ (2 : Nat) * κ j) ∧ FRC.Entropy.sumN u m = s) ∧ (∀ (N : Nat), FRC.Entropy.sumN (fun x => (2 : Nat) * (3 : Nat)) N = (2 : Nat) * ((3 : Nat) * N)) ∧ (∀ (u : Nat), u < (7 : Nat) → ∀ (v : Nat), v < (7 : Nat) → u + v ≤ (12 : Nat)) ∧ (6 : Nat) + (6 : Nat) + (6 : Nat) > (12 : Nat) :=469  And.intro @FRC.Entropy.additive_window (@FRC.Entropy.additive_window_hydrogen)470/-- 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$. -/471theorem p14047 : (∀ (m : Nat), (0 : Nat) < m → ∀ (t : Nat), FRC.Quantum.Joint (fun x => (12 : Nat)) m t ↔ t % (12 : Nat) = (0 : Nat)) ∧ (∀ (x : FRC.Shell (12 : Nat)), x + (12 : FRC.Shell (12 : Nat)) = x) ∧ (∀ (x : FRC.Shell (12 : Nat)) (k : Nat), k < (12 : Nat) → (0 : Nat) < k → x + FRC.Shell.ofNat k ≠ x) ∧ (∀ (x y : FRC.Shell (12 : Nat)), x + (1 : FRC.Shell (12 : Nat)) + -(y + (1 : FRC.Shell (12 : Nat))) = x + -y) ∧ (144 : Nat) = (12 : Nat) * (12 : Nat) ∧ (1728 : Nat) = (144 : Nat) * (12 : Nat) :=472  And.intro @FRC.Entropy.lock_recurrence (@FRC.Entropy.lock_orbits)473set_option linter.defProp false in474/-- 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). -/475def p14048 := And.intro @FRC.Entropy.shells_of_capacity (@FRC.Entropy.fusion_capacity)476/-- 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. -/477theorem p14019 : ∀ (S : Nat), ((4 : Nat) * S + (1 : Nat)) % (4 : Nat) = (1 : Nat) ∧ (4 : Nat) * S + (1 : Nat) - (1 : Nat) = (4 : Nat) * S :=478  @FRC.Entropy.quarter_identity479/-- 14:C4 (p14021) — The concordance: five evidence readings return $\sqrt{\dS}=(1.3\text{--}1.8)\times10^{61}$ \apx, $\pm17\%$ half-range on the count face, factor $1.9$ on $\dS$; the gauge reading 4a is displayed and excluded from every statistic. -/480theorem p14021 : ((119 : Nat) ≤ (127 : Nat) ∧ (127 : Nat) ≤ (166 : Nat) ∧ (119 : Nat) ≤ (133 : Nat) ∧ (133 : Nat) ≤ (166 : Nat) ∧ (119 : Nat) ≤ (164 : Nat) ∧ (164 : Nat) ≤ (166 : Nat)) ∧ ((16 : Nat) * ((166 : Nat) + (119 : Nat)) < (100 : Nat) * ((166 : Nat) - (119 : Nat)) ∧ (100 : Nat) * ((166 : Nat) - (119 : Nat)) < (17 : Nat) * ((166 : Nat) + (119 : Nat))) ∧ ((19 : Nat) * ((119 : Nat) * (119 : Nat)) < (10 : Nat) * ((166 : Nat) * (166 : Nat)) ∧ (10 : Nat) * ((166 : Nat) * (166 : Nat)) < (20 : Nat) * ((119 : Nat) * (119 : Nat))) ∧ ((736 : Nat) * (1616255 : Nat) < (1190 : Nat) * (1000000 : Nat) ∧ (1190 : Nat) * (1000000 : Nat) < (737 : Nat) * (1616255 : Nat) ∧ (1027 : Nat) * (1616255 : Nat) < (1660 : Nat) * (1000000 : Nat) ∧ (1660 : Nat) * (1000000 : Nat) < (1028 : Nat) * (1616255 : Nat)) ∧ ((1772 : Nat) * (1772 : Nat) < (3141592 : Nat) ∧ (3141593 : Nat) < (1773 : Nat) * (1773 : Nat)) ∧ (1300000 : Nat) < (1772 : Nat) * (736 : Nat) ∧ (1773 : Nat) * (737 : Nat) < (1310000 : Nat) ∧ (1800000 : Nat) < (1772 : Nat) * (1027 : Nat) ∧ (1773 : Nat) * (1028 : Nat) < (1830000 : Nat) :=481  @FRC.Entropy.concordance482/-- 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. -/483theorem p14022 : (∀ (m x : Nat), (2 : Nat) * x ≤ (2 : Nat) * m ↔ x ≤ m) ∧ ∀ (S m : Nat), S = (2 : Nat) * m → (2 : Nat) * ((2 : Nat) * S) = (4 : Nat) * S ∧ (8 : Nat) * m = (4 : Nat) * S :=484  And.intro @FRC.Entropy.closure_count (@FRC.Entropy.octant_count)485/-- 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. -/486theorem p14023 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (m : Nat), κ = (2 : Nat) * m → g ^ m * g ^ ((7 : Nat) * m) = (1 : FRC.Shell p) ∧ (g ^ m + g ^ ((7 : Nat) * m)) ^ (2 : Nat) = (2 : FRC.Shell p) ∧ ((2 : FRC.Shell p) * (g ^ m + g ^ ((7 : Nat) * m))) ^ (2 : Nat) = (8 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ((∃ ζ, ζ ^ (4 : Nat) = (-1 : FRC.Shell p) ∧ ζ ^ (8 : Nat) = (1 : FRC.Shell p)) ↔ ∃ m, κ = (2 : Nat) * m)) ∧ (4 : Nat) * (602140 : Nat) + (1 : Nat) = (2408561 : Nat) ∧ (602140 : Nat) % (2 : Nat) = (0 : Nat) ∧ (602140 : Nat) % (3 : Nat) = (1 : Nat) ∧ (1639587 : FRC.Shell (2408561 : Nat)) ^ (4 : Nat) = (-1 : FRC.Shell (2408561 : Nat)) ∧ (1639587 : FRC.Shell (2408561 : Nat)) ^ (8 : Nat) = (1 : FRC.Shell (2408561 : Nat)) ∧ (1639587 : FRC.Shell (2408561 : Nat)) * (1111186 : FRC.Shell (2408561 : Nat)) = (1 : FRC.Shell (2408561 : Nat)) ∧ ((1639587 : FRC.Shell (2408561 : Nat)) + (1111186 : FRC.Shell (2408561 : Nat))) ^ (2 : Nat) = (2 : FRC.Shell (2408561 : Nat)) ∧ ((2 : FRC.Shell (2408561 : Nat)) * ((1639587 : FRC.Shell (2408561 : Nat)) + (1111186 : FRC.Shell (2408561 : Nat)))) ^ (2 : Nat) = (8 : FRC.Shell (2408561 : Nat)) :=487  And.intro @FRC.Entropy.tsirelson_square (And.intro @FRC.Entropy.octant_iff (@FRC.Entropy.lab_carrier))488/-- 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. -/489theorem p14027 : FRC.Nat.isPrime (5 : Nat) ∧ ¬FRC.Nat.isPrime (9 : Nat) ∧ FRC.Nat.isPrime ((12 : Nat) * (1 : Nat) + (1 : Nat)) ∧ ¬FRC.Nat.isPrime ((12 : Nat) * (2 : Nat) + (1 : Nat)) ∧ FRC.Nat.isPrime ((12 : Nat) * (3 : Nat) + (1 : Nat)) :=490  @FRC.Entropy.capacity_axis491/-- 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. -/492theorem p14031 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ((∃ r, r * r = (2 : FRC.Shell p)) ↔ ∃ m, κ = (2 : Nat) * m) :=493  @FRC.Ledger.p14031494-- end ledger predicates495496end FRC.Entropy497