Theme/Carrier.lean — FrcCore

1import FrcCore.Theme.Field2import FrcCore.Theme.Foundation34/-!5# FrcCore.Theme.Carrier — the Carrier on its chart, without a generator (the carrier theme, task LM22)67Master block B on the Carrier's chart `Ω = 4S + 1`, `Ω` prime (`FRC.Nat.isPrime`), and no drive assumed. Every8residue below is found by the prime shell's arithmetic (`Theme/Field.lean`): Fermat's little theorem, the root9bound, the quarter-turn criterion.1011* **B5, the substrate residue.** `4 ∣ Ω − 1` and `3 ∣ Ω + 1` jointly hold iff `Ω ≡ 5 (mod 12)`; on a prime12  `Ω > 3` the same as structure: a quarter-turn `ħ² = −1` and no triality root `ω² + ω + 1 = 0` iff `Ω ≡ 5 (mod 12)`.13* **B7, the register in `S` alone.** `c² := 2S + 1 = 2⁻¹`; `G := 2S = −c²`, `2G = −1`, `G` the only solution;14  `ħ² = −1` solvable; `c` exists iff `S` is even; `k_B c = ħ` forces `k_B² = −2`; each defining square fixes its15  root up to sign; `h := −ħ` the distinct partner of `ħ`.16* **B8, the window ladder.** A nested Subject `p² < Ω` has its horizon below the Carrier's quarter-root and its17  shell below the coherence horizon; the saturating Subject `p² < Ω ≤ (p + 1)²` locks both; one square root per18  embedding; the laboratory nesting `37 → 1373 → 2 408 561`.19* **B10, one gauge bit.** `−1` a square; the square class blind to the pair `x ↔ −x`; integer parity flipped by it;20  the faces `x²` pair-invariant and `{ħ, −ħ}` two distinct roots of `−1`.21* **B14, the octant sector.** An element of order eight exists iff `S` is even.2223Since task LM24 the chart's generic lemmas (`chart_gt_two`, the octant sector, the Tsirelson square, the half-square24behind `c_exists_iff`, the parity flip) are `Shell.Prime`'s in `Theme/Field.lean`; the old names here are aliases.25No axioms.26-/2728namespace FRC29namespace Carrier3031open Shell Shell.Prime3233/-! ## B5: the substrate residue -/3435theorem mod_of_eq {n d k t : Nat} (hd : 0 < d) (h : n = d * k + t) : n % d = t % d := by36  rw [h]; exact FRC.Nat.add_mul_mod_self_left t k d hd3738/-- The residues mod `12` of `Ω − 1 ≡ 0 (mod 4)` and `Ω + 1 ≡ 0 (mod 3)`, written for `Ω = n + 1`. -/39theorem mod12_table : ∀ r, r < 12 → ((r % 4 = 0 ∧ (r + 2) % 3 = 0) ↔ (r + 1) % 12 = 5)40  | 0, _ => by decide | 1, _ => by decide | 2, _ => by decide | 3, _ => by decide41  | 4, _ => by decide | 5, _ => by decide | 6, _ => by decide | 7, _ => by decide42  | 8, _ => by decide | 9, _ => by decide | 10, _ => by decide | 11, _ => by decide43  | k + 12, h => absurd h (Nat.not_lt_of_le (Nat.le_add_left 12 k))4445/-- B5, the congruence: `4 ∣ Ω − 1` and `3 ∣ Ω + 1` jointly hold iff `Ω ≡ 5 (mod 12)`. -/46theorem substrate_arith (Ω : Nat) : (4 ∣ Ω - 1 ∧ 3 ∣ Ω + 1) ↔ Ω % 12 = 5 := by47  match Ω with48  | 0 => exact ⟨fun h => absurd ((FRC.Nat.dvd_iff_mod (by decide)).1 h.2) (by decide), fun h => absurd h (by decide)⟩49  | n + 1 =>50    rw [FRC.Nat.add_sub_cancel]51    obtain ⟨q, hq⟩ := FRC.Nat.mod_spec 12 (by decide) n52    have hr := Nat.mod_lt n (by decide : 0 < 12)53    generalize n % 12 = r at hq hr54    subst hq55    have e4 : (12 * q + r) % 4 = r % 4 := mod_of_eq (k := 3 * q) (by decide) (by rw [← FRC.Nat.mul_assoc])56    have e3 : (12 * q + r + 1 + 1) % 3 = (r + 2) % 3 :=57      mod_of_eq (k := 4 * q) (by decide) (by rw [← FRC.Nat.mul_assoc, Nat.add_assoc, Nat.add_assoc])58    have e12 : (12 * q + r + 1) % 12 = (r + 1) % 12 := mod_of_eq (k := q) (by decide) (by rw [Nat.add_assoc])59    have key := mod12_table r hr60    constructor61    · intro ⟨h4, h3⟩62      exact e12.trans (key.1 ⟨e4.symm.trans ((FRC.Nat.dvd_iff_mod (by decide)).1 h4),63        e3.symm.trans ((FRC.Nat.dvd_iff_mod (by decide)).1 h3)⟩)64    · intro h65      have k := key.2 (e12.symm.trans h)66      exact ⟨(FRC.Nat.dvd_iff_mod (by decide)).2 (e4.trans k.1), (FRC.Nat.dvd_iff_mod (by decide)).2 (e3.trans k.2)⟩6768theorem mod12_table' : ∀ r, r < 12 → ((r % 4 = 1 ∧ r % 3 = 2) ↔ r = 5)69  | 0, _ => by decide | 1, _ => by decide | 2, _ => by decide | 3, _ => by decide70  | 4, _ => by decide | 5, _ => by decide | 6, _ => by decide | 7, _ => by decide71  | 8, _ => by decide | 9, _ => by decide | 10, _ => by decide | 11, _ => by decide72  | k + 12, h => absurd h (Nat.not_lt_of_le (Nat.le_add_left 12 k))7374/-- `Ω ≡ 1 (mod 4)` and `Ω ≡ 2 (mod 3)` iff `Ω ≡ 5 (mod 12)`. -/75theorem mod12_iff (n : Nat) : (n % 4 = 1 ∧ n % 3 = 2) ↔ n % 12 = 5 := by76  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec 12 (by decide) n77  have hr := Nat.mod_lt n (by decide : 0 < 12)78  have e4 : n % 4 = n % 12 % 4 := mod_of_eq (k := 3 * q) (by decide) (by rw [← FRC.Nat.mul_assoc]; exact hq)79  have e3 : n % 3 = n % 12 % 3 := mod_of_eq (k := 4 * q) (by decide) (by rw [← FRC.Nat.mul_assoc]; exact hq)80  have key := mod12_table' (n % 12) hr81  exact ⟨fun ⟨h4, h3⟩ => key.1 ⟨e4.symm.trans h4, e3.symm.trans h3⟩,82    fun h => have k := key.2 h; ⟨e4.trans k.1, e3.trans k.2⟩⟩8384variable {Ω : Nat} [Pos Ω]8586/-- `(x² + x + 1)(x − 1) = x³ − 1`. -/87theorem cube_identity (x : Shell Ω) : (x * x + x + 1) * (x + -1) = x ^ 3 + -1 := by88  have h := geom_sum_mul x 389  rw [show sumRange (fun l => x ^ l) 3 = x * x + x + 1 by90    show 0 + x ^ 0 + x ^ 1 + x ^ 2 = x * x + x + 191    rw [zero_add, pow_zero, pow_one, pow_two, add_comm 1 x, add_comm (x + 1) (x * x), ← add_assoc]] at h92  exact h9394theorem three_ne_zero (h3 : 3 < Ω) : (1 : Shell Ω) + 1 + 1 ≠ 0 := fun h => by95  have v := val_injective h96  change ((1 % Ω + 1 % Ω) % Ω + 1 % Ω) % Ω = 0 at v97  rw [FRC.Nat.mod_eq_of_lt (Nat.lt_trans (by decide : 1 < 3) h3)] at v98  change (2 % Ω + 1) % Ω = 0 at v99  rw [FRC.Nat.mod_eq_of_lt (Nat.lt_trans (by decide : 2 < 3) h3)] at v100  change 3 % Ω = 0 at v101  rw [FRC.Nat.mod_eq_of_lt h3] at v102  exact absurd v (by decide)103104/-- B4's criterion, the triality root: on a prime `Ω > 3`, `ω² + ω + 1 = 0` is solvable iff `Ω ≡ 1 (mod 3)`.105Forward, `ω³ = 1` with `ω ≠ 1`, so `ω^{(Ω−1) mod 3} = 1` leaves only `3 ∣ Ω − 1`; backward, `ω = a^{(Ω−1)/3}` for a106residue `a` that `X^{(Ω−1)/3} − 1` misses. -/107theorem triality_iff (hp : FRC.Nat.isPrime Ω) (h3 : 3 < Ω) :108    (∃ ω : Shell Ω, ω * ω + ω + 1 = 0) ↔ Ω % 3 = 1 := by109  have h1Ω : 1 ≤ Ω := Nat.le_of_lt (Nat.lt_trans (by decide : 1 < 3) h3)110  constructor111  · intro ⟨ω, hω⟩112    have hc : ω ^ 3 = 1 := by113      have e := cube_identity ω114      rw [hω, zero_mul] at e115      exact eq_of_sub_eq_zero e.symm116    have h0 : ω ≠ 0 := fun e => by117      rw [e, mul_zero, zero_add, zero_add] at hω; exact one_ne_zero hp hω118    have h1 : ω ≠ 1 := fun e => by rw [e, mul_one] at hω; exact three_ne_zero h3 hω119    have hcase : (Ω - 1) % 3 = 0 := by120      have hr := pow_mod_eq_one hp h0 (by decide : 0 < 3) hc121      have hlt := Nat.mod_lt (Ω - 1) (by decide : 0 < 3)122      generalize (Ω - 1) % 3 = r at hr hlt123      match r, hr, hlt with124      | 0, _, _ => rfl125      | 1, hr, _ => rw [pow_one] at hr; exact absurd hr h1126      | 2, hr, _ =>127        rw [show (3 : Nat) = 2 + 1 from rfl, pow_succ, hr, one_mul] at hc; exact absurd hc h1128      | k + 3, _, hlt => exact absurd hlt (Nat.not_lt_of_le (Nat.le_add_left 3 k))129    obtain ⟨q, hq⟩ := FRC.Nat.mod_spec 3 (by decide) (Ω - 1)130    rw [hcase, Nat.add_zero] at hq131    exact FRC.Nat.mod_unique (by decide) (by rw [← hq, FRC.Nat.sub_add_cancel h1Ω])132  · intro h133    obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 3 (by decide) Ω134    rw [h] at hm135    have hm0 : 0 < m := by136      match m, hm with137      | 0, hm => rw [hm] at h3; exact absurd h3 (by decide)138      | k + 1, _ => exact Nat.zero_lt_succ k139    have hΩ1 : Ω - 1 = 3 * m := by rw [hm, FRC.Nat.add_sub_cancel]140    have hlt : m < Ω - 1 := by141      rw [hΩ1]142      have := FRC.Nat.mul_lt_mul_of_lt_of_pos (by decide : 1 < 3) hm0143      rw [Nat.one_mul] at this; exact this144    obtain ⟨a, ha, ham⟩ := exists_pow_ne_one hp hm0 hlt145    have hc : (a ^ m) ^ 3 = 1 := by rw [← pow_mul, Nat.mul_comm m 3, ← hΩ1, fermat hp ha]146    have e := cube_identity (a ^ m)147    rw [hc, add_neg] at e148    refine ⟨a ^ m, ?_⟩149    match mul_eq_zero hp e with150    | .inl e1 => exact e1151    | .inr e2 => exact absurd (eq_of_sub_eq_zero e2) ham152153/-- B5 as structure: on a prime `Ω > 3`, the quarter-turn (`ħ² = −1` solvable, B3) and the triality centre (no root154of `ω² + ω + 1`, B4) jointly hold iff `Ω ≡ 5 (mod 12)`. -/155theorem substrate_shell (hp : FRC.Nat.isPrime Ω) (h3 : 3 < Ω) :156    ((∃ ħ : Shell Ω, ħ * ħ = -1) ∧ ¬ ∃ ω : Shell Ω, ω * ω + ω + 1 = 0) ↔ Ω % 12 = 5 := by157  have h2 : 2 < Ω := Nat.lt_trans (by decide) h3158  have hq := quarter_turn_iff hp h2159  have ht := triality_iff hp h3160  have h30 : Ω % 3 ≠ 0 := hp.2 3 h3 (by decide)161  have hlt := Nat.mod_lt Ω (by decide : 0 < 3)162  constructor163  · intro ⟨hħ, hω⟩164    refine (mod12_iff Ω).1 ⟨hq.1 hħ, ?_⟩165    have h31 : Ω % 3 ≠ 1 := fun e => hω (ht.2 e)166    generalize Ω % 3 = r at h30 h31 hlt167    match r, h30, h31, hlt with168    | 0, h, _, _ => exact absurd rfl h169    | 1, _, h, _ => exact absurd rfl h170    | 2, _, _, _ => rfl171    | k + 3, _, _, hlt => exact absurd hlt (Nat.not_lt_of_le (Nat.le_add_left 3 k))172  · intro h173    have k := (mod12_iff Ω).2 h174    exact ⟨hq.2 k.1, fun hω => absurd ((ht.1 hω).symm.trans k.2) (by decide)⟩175176/-- **B5 (p00015), the substrate residue.** The congruences: `4 ∣ Ω − 1` and `3 ∣ Ω + 1` jointly hold iff177`Ω ≡ 5 (mod 12)`. The structure: on every prime `Ω > 3`, a quarter-turn exists and the triality polynomial has no178root iff `Ω ≡ 5 (mod 12)`. -/179theorem substrate_residue :180    (∀ Ω : Nat, (4 ∣ Ω - 1 ∧ 3 ∣ Ω + 1) ↔ Ω % 12 = 5) ∧181    ∀ {Ω : Nat} [Pos Ω], FRC.Nat.isPrime Ω → 3 < Ω →182      (((∃ ħ : Shell Ω, ħ * ħ = -1) ∧ ¬ ∃ ω : Shell Ω, ω * ω + ω + 1 = 0) ↔ Ω % 12 = 5) :=183  ⟨substrate_arith, fun hp h3 => substrate_shell hp h3⟩184185/-! ## B7: the register in `S` alone -/186187/-- `G := 2S`, the Carrier's half-period, as a residue of the chart `Ω = 4S + 1`. -/188def grav (Ω : Nat) [Pos Ω] (S : Nat) : Shell Ω := ofNat (2 * S)189190/-- `c² := 2S + 1`, the residue the register names `c²` (B7: `c² = 2⁻¹`). -/191def csq (Ω : Nat) [Pos Ω] (S : Nat) : Shell Ω := ofNat (2 * S + 1)192193/-- `c² := 2S + 1` is `2⁻¹` on the chart. -/194theorem two_mul_half {S : Nat} (hS : Ω = 4 * S + 1) : (2 : Shell Ω) * csq Ω S = 1 := ext (by195  show (2 % Ω * ((2 * S + 1) % Ω)) % Ω = 1 % Ω196  rw [← FRC.Nat.mul_mod _ _ _ Pos.pos,197    show 2 * (2 * S + 1) = Ω * 1 + 1 by rw [hS, Nat.mul_one, Nat.left_distrib, ← FRC.Nat.mul_assoc],198    FRC.Nat.add_mul_mod_self_left 1 1 Ω Pos.pos])199200/-- `G := 2S` is `−c²`. -/201theorem grav_eq {S : Nat} (hS : Ω = 4 * S + 1) : grav Ω S = -csq Ω S := by202  have e : csq Ω S + grav Ω S = 0 := ext (by203    show ((2 * S + 1) % Ω + (2 * S) % Ω) % Ω = 0204    rw [← FRC.Nat.add_mod _ _ _ Pos.pos,205      show 2 * S + 1 + 2 * S = Ω by rw [hS, Nat.add_right_comm, ← Nat.two_mul, ← FRC.Nat.mul_assoc],206      FRC.Nat.mod_self Ω Pos.pos])207  exact (neg_eq_of_add_eq_zero e).symm208209theorem two_ne_zero {S : Nat} (hS : Ω = 4 * S + 1) (hp : FRC.Nat.isPrime Ω) : (2 : Shell Ω) ≠ 0 := fun e => by210  have h := two_mul_half hS211  rw [e, zero_mul] at h; exact one_ne_zero hp h.symm212213/-- `k_B c = ħ` with `c² = 2⁻¹` and `ħ² = −1` forces `k_B² = −2`. -/214theorem kB_sq {S : Nat} (hS : Ω = 4 * S + 1) {c ħ k : Shell Ω} (hc : c * c = csq Ω S)215    (hħ : ħ * ħ = -1) (hk : k * c = ħ) : k * k = -2 :=216  calc k * k = k * k * 1 := (mul_one _).symm217    _ = k * k * ((2 : Shell Ω) * csq Ω S) := by rw [two_mul_half hS]218    _ = 2 * (k * k * (c * c)) := by rw [hc, mul_left_comm]219    _ = 2 * (ħ * ħ) := by rw [mul_mul_mul_comm, hk]220    _ = -2 := by rw [hħ, ← mul_neg, mul_one]221222/-- The root-pair partner: `h := −ħ` is a second, distinct root of `−1`. -/223theorem partner (hp : FRC.Nat.isPrime Ω) (h2 : 2 < Ω) {ħ : Shell Ω} (hh : ħ * ħ = -1) :224    (-ħ) * (-ħ) = -1 ∧ -ħ ≠ ħ := by225  refine ⟨by rw [neg_mul_neg]; exact hh, fun e => ?_⟩226  have h0 := ne_zero_of_mul_self (neg_one_ne_zero hp) hh227  have hs : (1 + 1) * ħ = 0 := by228    rw [right_distrib, one_mul]229    calc ħ + ħ = -ħ + ħ := by rw [e]230      _ = 0 := neg_add ħ231  match mul_eq_zero hp hs with232  | .inl e1 => exact neg_one_ne_one h2 (neg_eq_of_add_eq_zero e1)233  | .inr e2 => exact h0 e2234235/-- `c` exists iff `S` is even (`Shell.Prime.half_square_iff`, task LM24): a root `c` of `c² = 2⁻¹` gives `ζ = c (1 + i)`236with `ζ² = i`, an element of order eight; conversely the octant's `ζ` gives `(ζ + ζ⁷)² = 2` and `c = (ζ + ζ⁷)/2`. -/237theorem c_exists_iff (hp : FRC.Nat.isPrime Ω) {S : Nat} (hS : Ω = 4 * S + 1) :238    (∃ c : Shell Ω, c * c = csq Ω S) ↔ S % 2 = 0 :=239  half_square_iff hp hS240241/-- **B7 (p00165), the register in `S` alone**, on the chart `Ω = 4S + 1`, `Ω` prime, without a generator:242`c² := 2S + 1` (`csq`) is `2⁻¹`; `G := 2S` (`grav`) is `−c²`, `2G = −1`, and `G` is the only solution (exact);243`ħ² = −1` has a solution; `c` exists iff `S` is even; `k_B c = ħ` forces `k_B² = −2`; a square fixes its root up to244sign; `h := −ħ` is a second, distinct root of `−1`. -/245theorem register {Ω : Nat} [Pos Ω] (S : Nat) (hp : FRC.Nat.isPrime Ω) (hS : Ω = 4 * S + 1) :246    (2 : Shell Ω) * csq Ω S = 1 ∧247    grav Ω S = -csq Ω S ∧248    (2 : Shell Ω) * grav Ω S = -1 ∧ (∀ x : Shell Ω, 2 * x = -1 → x = grav Ω S) ∧249    (∃ ħ : Shell Ω, ħ * ħ = -1) ∧250    ((∃ c : Shell Ω, c * c = csq Ω S) ↔ S % 2 = 0) ∧251    (∀ c ħ k : Shell Ω, c * c = csq Ω S → ħ * ħ = -1 → k * c = ħ → k * k = -2) ∧252    (∀ x y : Shell Ω, x * x = y * y → x = y ∨ x = -y) ∧253    (∀ ħ : Shell Ω, ħ * ħ = -1 → (-ħ) * (-ħ) = -1 ∧ -ħ ≠ ħ) := by254  have hG2 : (2 : Shell Ω) * grav Ω S = -1 := by rw [grav_eq hS, ← mul_neg, two_mul_half hS]255  exact ⟨two_mul_half hS, grav_eq hS, hG2,256    fun x hx => mul_left_cancel hp (two_ne_zero hS hp) (hx.trans hG2.symm),257    exists_quarter_turn hp hS, c_exists_iff hp hS,258    fun _ _ _ hc hħ hk => kB_sq hS hc hħ hk,259    fun _ _ h => sq_eq_sq hp h,260    fun _ hh => partner hp (chart_gt_two hp hS) hh⟩261262/-! ## B8: the window ladder -/263264theorem lt_of_mul_self_lt {a b : Nat} (h : a * a < b * b) : a < b :=265  match Nat.lt_or_ge a b with266  | .inl hl => hl267  | .inr hge => absurd h (Nat.not_lt_of_le (Nat.mul_le_mul hge hge))268269/-- A nested Subject `p² < Ω`: its horizon `√p` lies below the Carrier's quarter-root (`x² ≤ p ⇒ x⁴ < Ω`) and its270shell below the coherence horizon (`x ≤ p ⇒ x² < Ω`). -/271theorem nested_windows {p Ω : Nat} (h : p * p < Ω) :272    (∀ x, x * x ≤ p → x * x * (x * x) < Ω) ∧ (∀ x, x ≤ p → x * x < Ω) :=273  ⟨fun _ hx => Nat.lt_of_le_of_lt (Nat.mul_le_mul hx hx) h,274   fun _ hx => Nat.lt_of_le_of_lt (Nat.mul_le_mul hx hx) h⟩275276/-- The saturating Subject `p² < Ω ≤ (p + 1)²` locks the ladder: its horizon is the Carrier's quarter-root window277and its shell the coherence window, exactly. -/278theorem saturated_windows {p Ω : Nat} (h : p * p < Ω) (hs : Ω ≤ (p + 1) * (p + 1)) :279    (∀ x, x * x ≤ p ↔ x * x * (x * x) < Ω) ∧ (∀ x, x ≤ p ↔ x * x < Ω) :=280  ⟨fun x => ⟨(nested_windows h).1 x, fun hx => Nat.le_of_lt_succ (lt_of_mul_self_lt (Nat.lt_of_lt_of_le hx hs))⟩,281   fun x => ⟨(nested_windows h).2 x, fun hx => Nat.le_of_lt_succ (lt_of_mul_self_lt (Nat.lt_of_lt_of_le hx hs))⟩⟩282283/-- One square-root horizon per embedding: `q² < p` and `p² < Ω` give `q⁴ < Ω`. -/284theorem nesting {q p Ω : Nat} (hq : q * q < p) (hp : p * p < Ω) : q * q * (q * q) < Ω :=285  (nested_windows hp).1 q (Nat.le_of_lt hq)286287/-- The laboratory ladder: `37 → 1373 → 2 408 561`, each prime, `37² < 1373`, `1373² < 2 408 561`. -/288theorem lab_ladder :289    FRC.Nat.isPrime 37 ∧ FRC.Nat.isPrime 1373 ∧ FRC.Nat.isPrime 2408561 ∧ 37 * 37 < 1373 ∧290    1373 * 1373 < 2408561 :=291  ⟨by decide, FRC.Nat.isPrime_of_bounded 1373 37 (by decide) (by decide) (by decide +kernel),292    FRC.Nat.isPrime_of_bounded 2408561 1552 (by decide) (by decide) (by decide +kernel), by decide, by decide⟩293294/-- **B8 (p00166), the window ladder.** A nested Subject `p² < Ω` has its horizon below the Carrier's quarter-root295and its shell below the coherence horizon; the saturating Subject `p² < Ω ≤ (p + 1)²` locks both windows; one296square-root horizon per embedding; laboratory-verified on `Ω = 2 408 561` with the nesting `37 → 1373`. -/297theorem window_ladder :298    (∀ p Ω : Nat, p * p < Ω → (∀ x, x * x ≤ p → x * x * (x * x) < Ω) ∧ (∀ x, x ≤ p → x * x < Ω)) ∧299    (∀ p Ω : Nat, p * p < Ω → Ω ≤ (p + 1) * (p + 1) →300      (∀ x, x * x ≤ p ↔ x * x * (x * x) < Ω) ∧ (∀ x, x ≤ p ↔ x * x < Ω)) ∧301    (∀ q p Ω : Nat, q * q < p → p * p < Ω → q * q * (q * q) < Ω) ∧302    (FRC.Nat.isPrime 37 ∧ FRC.Nat.isPrime 1373 ∧ FRC.Nat.isPrime 2408561 ∧ 37 * 37 < 1373 ∧303      1373 * 1373 < 2408561) :=304  ⟨fun _ _ h => nested_windows h, fun _ _ h hs => saturated_windows h hs, fun _ _ _ hq hp => nesting hq hp,305    lab_ladder⟩306307/-! ## B10: one gauge bit closes the sign sector -/308309/-- The square class is pair-blind: `x` is a square iff `−x` is (`(ħy)² = −y²`). -/310theorem square_pair_blind (hp : FRC.Nat.isPrime Ω) {S : Nat} (hS : Ω = 4 * S + 1) (x : Shell Ω) :311    (∃ y : Shell Ω, y * y = x) ↔ (∃ y : Shell Ω, y * y = -x) := by312  obtain ⟨h, hh⟩ := exists_quarter_turn hp hS313  exact ⟨fun ⟨y, hy⟩ => ⟨h * y, by rw [mul_mul_mul_comm, hh, hy, neg_one_mul]⟩,314    fun ⟨y, hy⟩ => ⟨h * y, by rw [mul_mul_mul_comm, hh, hy, neg_one_mul, neg_neg]⟩⟩315316/-- **B10 (p00168), one gauge bit closes the sign sector**, on the chart `Ω = 4S + 1`, `Ω` prime: `−1` is a317square; the square class is blind to the pair `x ↔ −x`; integer parity is flipped by it, so it is frame data; the318registered faces are pair-invariant, `(−x)² = x²`, and `{ħ, −ħ}` are two distinct roots of `−1`. -/319theorem sign_sector {Ω : Nat} [Pos Ω] (S : Nat) (hp : FRC.Nat.isPrime Ω) (hS : Ω = 4 * S + 1) :320    (∃ ħ : Shell Ω, ħ * ħ = -1) ∧321    (∀ x : Shell Ω, (∃ y : Shell Ω, y * y = x) ↔ (∃ y : Shell Ω, y * y = -x)) ∧322    (∀ x : Shell Ω, x ≠ 0 → (x.val % 2 = 0 ↔ ¬ (-x).val % 2 = 0)) ∧323    (∀ x : Shell Ω, (-x) * (-x) = x * x) ∧324    (∀ ħ : Shell Ω, ħ * ħ = -1 → (-ħ) * (-ħ) = -1 ∧ -ħ ≠ ħ) :=325  ⟨exists_quarter_turn hp hS, square_pair_blind hp hS, fun _ hx => parity_flips hS hx, fun x => neg_mul_neg x x,326    fun _ hh => partner hp (chart_gt_two hp hS) hh⟩327328/-- **B14 (p00170)**, as a key: on the chart, `C₈ ⊂ C_{4S}` exists exactly when `S` is even. -/329theorem octant {Ω : Nat} [Pos Ω] (S : Nat) (hp : FRC.Nat.isPrime Ω) (hS : Ω = 4 * S + 1) :330    (∃ ζ : Shell Ω, ζ ^ 8 = 1 ∧ ζ ^ 4 ≠ 1) ↔ S % 2 = 0 :=331  octant_sector hp hS332333/-! ## Old names (task LM24): the chart's lemmas are `Shell.Prime`'s, in `Theme/Field.lean` -/334335omit [Pos Ω] in336theorem chart_gt_two (hp : FRC.Nat.isPrime Ω) {S : Nat} (hS : Ω = 4 * S + 1) : 2 < Ω := Prime.chart_gt_two hp hS337theorem two_eq : (2 : Shell Ω) = 1 + 1 := Prime.two_eq338theorem add_one_add_one_neg (a : Shell Ω) : a + 1 + (1 + -a) = 1 + 1 := Prime.add_one_add_one_neg a339theorem octant_sector (hp : FRC.Nat.isPrime Ω) {S : Nat} (hS : Ω = 4 * S + 1) :340    (∃ ζ : Shell Ω, ζ ^ 8 = 1 ∧ ζ ^ 4 ≠ 1) ↔ S % 2 = 0 := Prime.octant_sector hp hS341theorem tsirelson {ζ : Shell Ω} (h4 : ζ ^ 4 = -1) : (ζ + ζ ^ 7) * (ζ + ζ ^ 7) = 2 := Prime.tsirelson h4342theorem parity_flips {S : Nat} (hS : Ω = 4 * S + 1) {x : Shell Ω} (hx : x ≠ 0) :343    x.val % 2 = 0 ↔ ¬ (-x).val % 2 = 0 := Prime.parity_flips hS hx344345end Carrier346end FRC347