Theme/Field.lean — FrcCore

1import FrcCore.Series2import FrcCore.Poly34/-!5# FrcCore.Theme.Field — the prime shell is a field, without a generator (the foundation theme, tasks LM22 and LM24)67The shell `𝔽_p` of a prime `p` (`FRC.Nat.isPrime`, trial division), with no drive assumed, on `Series.lean` and8`Poly.lean` alone: Euclid's lemma; no zero divisors, cancellation and the square roots of one; Fermat's9little theorem by the permutation `x ↦ a x` of the nonzero residues (`prod_perm`); the roots of `x^m − 1`, bounded by10the degree, so some residue escapes `x^m = 1` for `m < p − 1`; hence a residue `a` with `a^{(p−1)/2} = −1`, and the11quarter-turn criterion: `x² = −1` is solvable iff `p ≡ 1 (mod 4)`, with `ħ = a^S` on `p = 4S + 1`; a shell without12zero divisors is prime; and the chart `p = 4S + 1`: the octant sector, the half-square and the parity flip. Task LM2413split this file from `Theme/Foundation.lean` under the size budget (G10), so that the programme themes take the field14without the foundation's rows; every name is unchanged. No axioms.15-/1617namespace FRC1819namespace Nat2021theorem mod_eq_zero_of_add {a r p : Nat} (hp : 0 < p) (h : (a + r) % p = 0) (ha : a % p = 0) : r % p = 0 := by22  rw [FRC.Nat.add_mod _ _ _ hp, ha, Nat.zero_add, FRC.Nat.mod_mod _ _ hp] at h23  exact h2425theorem mul_mod_eq_zero_left {a b p : Nat} (hp : 0 < p) (ha : a % p = 0) : (a * b) % p = 0 := by26  rw [FRC.Nat.mul_mod_left' _ _ _ hp, ha, Nat.zero_mul]; rfl2728/-- Euclid's lemma, the step: for a prime `p` and `p ∤ b`, no `k` with `0 < k < p` has `p ∣ k b`. If `p ∣ k b` with29`2 ≤ k`, write `p = q k + r`: `p ∤ k` gives `0 < r < k`, and `r b = p b − q (k b)` is again divisible by `p`. -/30theorem prime_not_dvd_mul_aux {p b : Nat} (hp : isPrime p) (hb : b % p ≠ 0) :31    ∀ n k, k < n → 0 < k → k < p → (k * b) % p ≠ 0 := by32  have hp0 : 0 < p := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hp.133  intro n34  induction n with35  | zero => intro k hk; exact absurd hk (Nat.not_lt_zero k)36  | succ n ih =>37    intro k hk hk0 hkp hkb38    match k, hk, hk0, hkp, hkb with39    | 0, _, hk0, _, _ => exact absurd hk0 (Nat.lt_irrefl 0)40    | 1, _, _, _, hkb => rw [Nat.one_mul] at hkb; exact hb hkb41    | k + 2, hk, _, hkp, hkb =>42      have hk2 : 0 < k + 2 := Nat.zero_lt_succ _43      have hpk : p % (k + 2) ≠ 0 := hp.2 (k + 2) hkp (Nat.le_add_left 2 k)44      obtain ⟨q, hq⟩ := FRC.Nat.mod_spec (k + 2) hk2 p45      have hr : p % (k + 2) < k + 2 := Nat.mod_lt _ hk246      have e : p * b = (k + 2) * b * q + p % (k + 2) * b := by47        calc p * b = ((k + 2) * q + p % (k + 2)) * b := by rw [← hq]48          _ = (k + 2) * q * b + p % (k + 2) * b := FRC.Nat.add_mul _ _ _49          _ = (k + 2) * b * q + p % (k + 2) * b := by50              rw [FRC.Nat.mul_assoc, Nat.mul_comm q b, ← FRC.Nat.mul_assoc]51      have hpb : (p * b) % p = 0 := mul_mod_eq_zero_left hp0 (FRC.Nat.mod_self p hp0)52      have hA : ((k + 2) * b * q) % p = 0 := mul_mod_eq_zero_left hp0 hkb53      have hR : (p % (k + 2) * b) % p = 0 := mod_eq_zero_of_add hp0 (e ▸ hpb) hA54      exact ih (p % (k + 2)) (Nat.lt_of_lt_of_le hr (Nat.le_of_lt_succ hk)) (Nat.pos_of_ne_zero hpk)55        (Nat.lt_trans hr hkp) hR5657/-- Euclid's lemma: a prime dividing a product divides a factor. -/58theorem prime_mul_mod {p a b : Nat} (hp : isPrime p) (h : (a * b) % p = 0) : a % p = 0 ∨ b % p = 0 := by59  have hp0 : 0 < p := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hp.160  match Nat.decEq (b % p) 0 with61  | .isTrue hb => exact .inr hb62  | .isFalse hb =>63    match Nat.decEq (a % p) 0 with64    | .isTrue ha => exact .inl ha65    | .isFalse ha =>66      have h' : (a % p * b) % p = 0 := by rw [FRC.Nat.mod_mul_mod _ _ _ hp0]; exact h67      exact absurd h' (prime_not_dvd_mul_aux hp hb (a % p + 1) (a % p) (Nat.lt_succ_self _)68        (Nat.pos_of_ne_zero ha) (Nat.mod_lt _ hp0))6970/-- `d ∣ n` iff `n % d = 0`. -/71theorem dvd_iff_mod {d n : Nat} (hd : 0 < d) : d ∣ n ↔ n % d = 0 :=72  ⟨fun ⟨c, hc⟩ => FRC.Nat.mod_unique hd (by rw [Nat.add_zero]; exact hc),73   fun h => match FRC.Nat.mod_spec d hd n with74     | ⟨q, hq⟩ => ⟨q, by rw [h, Nat.add_zero] at hq; exact hq⟩⟩7576/-- Parity: `n % 2` is `0` or `1`. -/77theorem mod_two_cases (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 := by78  have h := Nat.mod_lt n (Nat.zero_lt_succ 1)79  match n % 2, h with80  | 0, _ => exact .inl rfl81  | 1, _ => exact .inr rfl82  | k + 2, h => exact absurd h (Nat.not_lt_of_le (Nat.le_add_left 2 k))8384theorem succ_lt_of_lt_pred {j n : Nat} (h : j < n - 1) : j + 1 < n := by85  match n, h with86  | 0, h => exact absurd h (Nat.not_lt_zero j)87  | n + 1, h => rw [FRC.Nat.add_sub_cancel] at h; exact Nat.succ_lt_succ h8889theorem pred_lt_pred {v n : Nat} (hv : 0 < v) (h : v < n) : v - 1 < n - 1 := by90  match v, n, hv, h with91  | 0, _, hv, _ => exact absurd hv (Nat.lt_irrefl 0)92  | v + 1, 0, _, h => exact absurd h (Nat.not_lt_zero _)93  | v + 1, n + 1, _, h => rw [FRC.Nat.add_sub_cancel, FRC.Nat.add_sub_cancel]; exact Nat.lt_of_succ_lt_succ h9495theorem eq_of_pred_eq {u v : Nat} (hu : 0 < u) (hv : 0 < v) (h : u - 1 = v - 1) : u = v := by96  rw [← FRC.Nat.sub_add_cancel hu, ← FRC.Nat.sub_add_cancel hv, h]9798/-- An odd number is no sum of two numbers of equal parity. -/99theorem parity_split {a b n : Nat} (h : a + b = 2 * n + 1) : a % 2 = 0 ↔ ¬ b % 2 = 0 := by100  have h2 : (0 : Nat) < 2 := Nat.zero_lt_succ 1101  have hodd : (a + b) % 2 = 1 := by rw [h, FRC.Nat.add_mul_mod_self_left 1 n 2 h2]102  rw [FRC.Nat.add_mod _ _ _ h2] at hodd103  constructor104  · intro ha hb; rw [ha, hb] at hodd; exact absurd hodd (by decide)105  · intro hb106    match mod_two_cases a, mod_two_cases b with107    | .inl ha, _ => exact ha108    | .inr _, .inl hb' => exact absurd hb' hb109    | .inr ha, .inr hb' => rw [ha, hb'] at hodd; exact absurd hodd (by decide)110111end Nat112113namespace Shell114115variable {p : Nat} [Pos p]116117/-! ## The polynomial `X^n − 1` -/118119namespace Poly120121/-- `X^n − 1`, for `n ≥ 1`. -/122def xn1 (n : Nat) : Poly p := fun i => if i = n then 1 else if i = 0 then -1 else 0123124theorem xn1_bound (n : Nat) : Bound (xn1 n : Poly p) n := fun i hi => by125  show (if i = n then 1 else if i = 0 then -1 else 0 : Shell p) = 0126  rw [ite_eq_right (Nat.ne_of_gt hi), ite_eq_right (Nat.ne_of_gt (Nat.lt_of_le_of_lt (Nat.zero_le n) hi))]127128theorem xn1_top (n : Nat) : (xn1 n : Poly p) n = 1 := by129  show (if n = n then 1 else if n = 0 then -1 else 0 : Shell p) = 1130  rw [ite_eq_left rfl]131132theorem eval_xn1 {n : Nat} (hn : 0 < n) (a : Shell p) : eval (xn1 n : Poly p) n a = a ^ n + -1 := by133  unfold eval134  rw [sumRange_succ, sum_eq_single hn (fun l hl hne => by135    show (if l = n then 1 else if l = 0 then -1 else 0 : Shell p) * a ^ l = 0136    rw [ite_eq_right (Nat.ne_of_lt hl), ite_eq_right hne, zero_mul])]137  show (if 0 = n then 1 else if 0 = 0 then -1 else 0 : Shell p) * a ^ 0 + xn1 n n * a ^ n = a ^ n + -1138  rw [ite_eq_right (Nat.ne_of_lt hn), ite_eq_left rfl, xn1_top, pow_zero, mul_one, one_mul, add_comm]139140end Poly141142namespace Prime143144/-! ## The prime shell is a field: no zero divisors, cancellation, the square roots of one -/145146omit [Pos p] in147theorem one_lt (hp : FRC.Nat.isPrime p) : 1 < p := hp.1148149theorem one_ne_zero (hp : FRC.Nat.isPrime p) : (1 : Shell p) ≠ 0 := fun h => by150  have := val_injective h151  rw [val_one, val_zero, FRC.Nat.mod_eq_of_lt (one_lt hp)] at this152  exact Nat.noConfusion this153154theorem eq_zero_of_val_mod {a : Shell p} (h : a.val % p = 0) : a = 0 :=155  ext (by rw [← FRC.Nat.mod_eq_of_lt a.lt]; exact h)156157/-- No zero divisors on a prime shell (Euclid's lemma on the representatives). -/158theorem mul_eq_zero (hp : FRC.Nat.isPrime p) {a b : Shell p} (h : a * b = 0) : a = 0 ∨ b = 0 :=159  match FRC.Nat.prime_mul_mod hp (val_injective h) with160  | .inl ha => .inl (eq_zero_of_val_mod ha)161  | .inr hb => .inr (eq_zero_of_val_mod hb)162163theorem mul_ne_zero (hp : FRC.Nat.isPrime p) {a b : Shell p} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=164  fun h => match mul_eq_zero hp h with165    | .inl e => ha e166    | .inr e => hb e167168theorem eq_of_sub_eq_zero {b c : Shell p} (e : b + -c = 0) : b = c :=169  calc b = b + 0 := (add_zero b).symm170    _ = b + (-c + c) := by rw [neg_add]171    _ = (b + -c) + c := (add_assoc _ _ _).symm172    _ = c := by rw [e, zero_add]173174/-- Cancellation: `a b = a c` with `a ≠ 0` gives `b = c`. -/175theorem mul_left_cancel (hp : FRC.Nat.isPrime p) {a b c : Shell p} (ha : a ≠ 0) (h : a * b = a * c) : b = c := by176  have : a * (b + -c) = 0 := by rw [left_distrib, ← mul_neg, h, add_neg]177  match mul_eq_zero hp this with178  | .inl e => exact absurd e ha179  | .inr e => exact eq_of_sub_eq_zero e180181/-- The square roots of a square are `±` its root: `x² = y²` gives `x = y` or `x = −y`. -/182theorem sq_eq_sq (hp : FRC.Nat.isPrime p) {x y : Shell p} (h : x * x = y * y) : x = y ∨ x = -y := by183  have e : (x + -y) * (x + y) = 0 := by184    rw [right_distrib, left_distrib, left_distrib, ← neg_mul, ← neg_mul, mul_comm y x, ← h,185      add_comm (-(x * y)) (-(x * x)), add_add_add_comm, add_neg, add_neg, add_zero]186  match mul_eq_zero hp e with187  | .inl e1 => exact .inl (eq_of_sub_eq_zero e1)188  | .inr e2 => exact .inr (eq_neg_of_add_eq_zero e2)189190/-- The square roots of one are `±1`. -/191theorem sq_eq_one (hp : FRC.Nat.isPrime p) {x : Shell p} (h : x * x = 1) : x = 1 ∨ x = -1 :=192  sq_eq_sq hp (h.trans (mul_one 1).symm)193194/-! ## Fermat's little theorem without a generator -/195196theorem val_pos {a : Shell p} (h : a ≠ 0) : 0 < a.val := Nat.pos_of_ne_zero (fun e => h (ext e))197198theorem ofNat_ne_zero {k : Nat} (hk0 : 0 < k) (hk : k < p) : (ofNat k : Shell p) ≠ 0 := fun h => by199  have := val_injective h200  rw [val_ofNat, val_zero, FRC.Nat.mod_eq_of_lt hk] at this201  exact Nat.ne_of_gt hk0 this202203theorem prodRange_ne_zero (hp : FRC.Nat.isPrime p) {f : Nat → Shell p} :204    ∀ n, (∀ j, j < n → f j ≠ 0) → prodRange f n ≠ 0205  | 0, _ => one_ne_zero hp206  | n + 1, h => mul_ne_zero hp (prodRange_ne_zero hp n (fun j hj => h j (Nat.lt_succ_of_lt hj))) (h n (Nat.lt_succ_self n))207208/-- The nonzero residues `1, …, p − 1`, indexed from `0`. -/209def nonzero (j : Nat) : Shell p := ofNat (j + 1)210211/-- Where multiplication by `a` sends the `j`-th nonzero residue. -/212def nonzeroIndex (a : Shell p) (j : Nat) : Nat := (a * nonzero j).val - 1213214theorem nonzero_ne_zero {j : Nat} (hj : j < p - 1) : (nonzero j : Shell p) ≠ 0 :=215  ofNat_ne_zero (Nat.zero_lt_succ j) (FRC.Nat.succ_lt_of_lt_pred hj)216217/-- Fermat's little theorem, generator-free: `a^{p−1} = 1` for `a ≠ 0`. Multiplication by `a` permutes the nonzero218residues, so `a^{p−1} · Π u = Π u`, and the product, nonzero, cancels. -/219theorem fermat (hp : FRC.Nat.isPrime p) {a : Shell p} (ha : a ≠ 0) : a ^ (p - 1) = 1 := by220  have hv : ∀ j, j < p - 1 → 0 < (a * nonzero j).val := fun j hj =>221    val_pos (mul_ne_zero hp ha (nonzero_ne_zero hj))222  have hlt : ∀ j, j < p - 1 → nonzeroIndex a j < p - 1 := fun j hj =>223    FRC.Nat.pred_lt_pred (hv j hj) (a * nonzero j).lt224  have hinj : ∀ i j, i < p - 1 → j < p - 1 → nonzeroIndex a i = nonzeroIndex a j → i = j := fun i j hi hj e => by225    have e2 : (nonzero i : Shell p) = nonzero j :=226      mul_left_cancel hp ha (ext (FRC.Nat.eq_of_pred_eq (hv i hi) (hv j hj) e))227    exact Nat.succ.inj (Poly.Frame.ofNat_inj_lt (FRC.Nat.succ_lt_of_lt_pred hi) (FRC.Nat.succ_lt_of_lt_pred hj) e2)228  have hF : ∀ j, j < p - 1 → nonzero (nonzeroIndex a j) = a * nonzero j := fun j hj => by229    show ofNat ((a * nonzero j).val - 1 + 1) = a * nonzero j230    rw [FRC.Nat.sub_add_cancel (hv j hj), ofNat_val]231  have hperm := prod_perm (nonzero : Nat → Shell p) (nonzeroIndex a) (p - 1) hlt hinj232  rw [prodRange_congr (p - 1) hF, prodRange_mul_left] at hperm233  have hP := prodRange_ne_zero hp (f := (nonzero : Nat → Shell p)) (p - 1) (fun j hj => nonzero_ne_zero hj)234  exact mul_left_cancel hp hP (by rw [mul_comm, hperm, mul_one])235236omit [Pos p] in237theorem two_le (hp : FRC.Nat.isPrime p) : 2 ≤ p := hp.1238239/-- On a shell of more than two residues, `−1 ≠ 1`. -/240theorem neg_one_ne_one (h2 : 2 < p) : (-1 : Shell p) ≠ 1 := fun e => by241  have h : (1 : Shell p) + 1 = 0 :=242    calc (1 : Shell p) + 1 = -1 + 1 := by rw [e]243      _ = 0 := neg_add 1244  have v := val_injective h245  change (1 % p + 1 % p) % p = 0 at v246  rw [FRC.Nat.mod_eq_of_lt (Nat.lt_trans (Nat.lt_succ_self 1) h2)] at v247  change 2 % p = 0 at v248  rw [FRC.Nat.mod_eq_of_lt h2] at v249  exact absurd v (by decide)250251theorem ne_zero_of_mul_self {h c : Shell p} (hc : c ≠ 0) (hh : h * h = c) : h ≠ 0 := fun e => by252  rw [e, zero_mul] at hh; exact hc hh.symm253254theorem neg_one_ne_zero (hp : FRC.Nat.isPrime p) : (-1 : Shell p) ≠ 0 := fun e => by255  have : (1 : Shell p) = 0 := by rw [← neg_neg (1 : Shell p), e, neg_zero]256  exact one_ne_zero hp this257258/-! ## The roots of `X^m − 1`, and the residues they miss -/259260/-- Some nonzero residue escapes `x^m = 1` when `0 < m < p − 1`: else `X^m − 1` had `m + 1` roots. -/261theorem exists_pow_ne_one (hp : FRC.Nat.isPrime p) {m : Nat} (hm : 0 < m) (hlt : m < p - 1) :262    ∃ a : Shell p, a ≠ 0 ∧ a ^ m ≠ 1 :=263  match decExistsLT (fun j => (nonzero j : Shell p) ^ m ≠ 1) (p - 1) with264  | .isTrue ⟨j, hj, h⟩ => ⟨nonzero j, nonzero_ne_zero hj, h⟩265  | .isFalse hno => by266    have hm1 : m + 1 < p := FRC.Nat.succ_lt_of_lt_pred hlt267    have hone : ∀ i, i ≤ m → (nonzero i : Shell p) ^ m = 1 := fun i hi =>268      match decEq ((nonzero i : Shell p) ^ m) 1 with269      | .isTrue e => e270      | .isFalse ne => absurd ⟨i, Nat.lt_of_le_of_lt hi hlt, ne⟩ hno271    have hz := Poly.root_bound_of (fun h => mul_eq_zero hp h) m (Poly.xn1 m) (Poly.xn1_bound m) (nonzero : Nat → Shell p)272      (fun i j hi hj e => Nat.succ.inj (Poly.Frame.ofNat_inj_lt (Nat.lt_of_le_of_lt (Nat.succ_le_succ hi) hm1)273        (Nat.lt_of_le_of_lt (Nat.succ_le_succ hj) hm1) e))274      (fun i hi => by rw [Poly.eval_xn1 hm, hone i hi, add_neg]) m275    rw [Poly.xn1_top] at hz276    exact absurd hz (one_ne_zero hp)277278/-- On an odd prime `p = 2n + 1`, some residue has `aⁿ = −1`: a non-square, by Fermat and `x² = 1 ⇒ x = ±1`. -/279theorem exists_pow_half (hp : FRC.Nat.isPrime p) {n : Nat} (hn : p = 2 * n + 1) : ∃ a : Shell p, a ^ n = -1 := by280  have hn0 : 0 < n := by281    match n, hn with282    | 0, hn => have h := hp.1; rw [hn] at h; exact absurd h (by decide)283    | k + 1, _ => exact Nat.zero_lt_succ k284  have hp1 : p - 1 = n + n := by rw [hn, FRC.Nat.add_sub_cancel, Nat.two_mul]285  have hlt : n < p - 1 := by rw [hp1]; exact Nat.lt_add_of_pos_right hn0286  obtain ⟨a, ha, han⟩ := exists_pow_ne_one hp hn0 hlt287  have hsq : a ^ n * a ^ n = 1 := by rw [← pow_add, ← hp1, fermat hp ha]288  exact ⟨a, match sq_eq_one hp hsq with289    | .inl e => absurd e han290    | .inr e => e⟩291292/-! ## The quarter-turn on the chart `p = 4S + 1` (the criterion: `Theme/Foundation.lean`) -/293294/-- The quarter-turn on the chart `p = 4S + 1`, generator-free: `ħ = a^S` with `a^{2S} = −1`. -/295theorem exists_quarter_turn (hp : FRC.Nat.isPrime p) {S : Nat} (hS : p = 4 * S + 1) :296    ∃ h : Shell p, h * h = -1 := by297  obtain ⟨a, ha⟩ := exists_pow_half hp (n := 2 * S) (by rw [hS, ← FRC.Nat.mul_assoc])298  exact ⟨a ^ S, by rw [← pow_add, ← Nat.two_mul, ha]⟩299300/-! ## A shell without zero divisors is prime -/301302theorem ofNat_mul (a b : Nat) : (ofNat a * ofNat b : Shell p) = ofNat (a * b) :=303  ext (by show (a % p * (b % p)) % p = (a * b) % p; rw [← FRC.Nat.mul_mod _ _ _ Pos.pos])304305theorem ofNat_self : (ofNat p : Shell p) = 0 := ext (FRC.Nat.mod_self p Pos.pos)306307/-- A shell of at least two residues without zero divisors is prime: a factorisation `p = d q` with `2 ≤ d < p`308makes `d · q = 0` with both factors nonzero. -/309theorem isPrime_of_no_zero_divisors (h2 : 2 ≤ p) (hz : ∀ {a b : Shell p}, a * b = 0 → a = 0 ∨ b = 0) :310    FRC.Nat.isPrime p := by311  refine ⟨h2, fun d hdp hd2 hmod => ?_⟩312  have hd0 : 0 < d := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hd2313  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec d hd0 p314  rw [hmod, Nat.add_zero] at hq315  have hq0 : 0 < q := by316    match q, hq with317    | 0, hq => rw [Nat.mul_zero] at hq; rw [hq] at h2; exact absurd h2 (by decide)318    | k + 1, _ => exact Nat.zero_lt_succ k319  have hqp : q < p := by320    have h1 : 1 * q < d * q := FRC.Nat.mul_lt_mul_of_lt_of_pos (Nat.lt_of_lt_of_le (Nat.lt_succ_self 1) hd2) hq0321    rw [Nat.one_mul, ← hq] at h1; exact h1322  have e : (ofNat d * ofNat q : Shell p) = 0 := by rw [ofNat_mul, ← hq, ofNat_self]323  match hz e with324  | .inl e1 => exact ofNat_ne_zero hd0 hdp e1325  | .inr e2 => exact ofNat_ne_zero hq0 hqp e2326327/-! ## The chart `p = 4S + 1`: the half-square and the parity flip (moved from the Carrier's theme by task LM24, so that328every programme theme stands on them without the Carrier; `FRC.Carrier` keeps the old names) -/329330omit [Pos p] in331theorem chart_gt_two (hp : FRC.Nat.isPrime p) {S : Nat} (hS : p = 4 * S + 1) : 2 < p := by332  match S, hS with333  | 0, hS => have h := hp.1; rw [hS] at h; exact absurd h (by decide)334  | k + 1, hS =>335    rw [hS, Nat.left_distrib]336    exact Nat.lt_of_lt_of_le (by decide : 2 < 5) (Nat.le_add_left 5 (4 * k))337338/-- `2 = 1 + 1` on every shell. -/339theorem two_eq : (2 : Shell p) = 1 + 1 :=340  ext (by show 2 % p = (1 % p + 1 % p) % p; rw [← FRC.Nat.add_mod _ _ _ Pos.pos])341342/-- `a + 1 + (1 − a) = 1 + 1`. -/343theorem add_one_add_one_neg (a : Shell p) : a + 1 + (1 + -a) = 1 + 1 := by344  rw [add_assoc, ← add_assoc 1 1 (-a), add_comm (1 + 1) (-a), ← add_assoc a (-a) (1 + 1), add_neg, zero_add]345346/-- The octant sector: on the chart `p = 4S + 1`, an element of order eight (`ζ⁸ = 1`,347`ζ⁴ ≠ 1`) exists iff `S` is even: `C₈ ⊂ C_{4S}` exactly when `8 ∣ 4S`. Forward, `ζ⁴ = −1` and Fermat give348`ζ^{4S} = 1`, which an odd `S = 2m + 1` turns into `ζ⁴ = 1`; backward, `ζ = a^{S/2}` with `a^{2S} = −1`. -/349theorem octant_sector (hp : FRC.Nat.isPrime p) {S : Nat} (hS : p = 4 * S + 1) :350    (∃ ζ : Shell p, ζ ^ 8 = 1 ∧ ζ ^ 4 ≠ 1) ↔ S % 2 = 0 := by351  have h2 := chart_gt_two hp hS352  constructor353  · intro ⟨ζ, h8, h4⟩354    have hz0 : ζ ≠ 0 := fun e => by355      rw [e, show (8 : Nat) = 7 + 1 from rfl, pow_succ, mul_zero] at h8; exact one_ne_zero hp h8.symm356    have h4' : ζ ^ 4 = -1 :=357      match sq_eq_one hp (by rw [← pow_add]; exact h8 : ζ ^ 4 * ζ ^ 4 = 1) with358      | .inl e => absurd e h4359      | .inr e => e360    match FRC.Nat.mod_two_cases S with361    | .inl e => exact e362    | .inr e =>363      obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 2 (by decide) S364      rw [e] at hm365      have hf := fermat hp hz0366      have hp1 : p - 1 = 8 * m + 4 := by367        rw [hS, FRC.Nat.add_sub_cancel, hm, Nat.left_distrib, ← FRC.Nat.mul_assoc]368      rw [hp1, pow_add, pow_mul, h8, one_pow, one_mul, h4'] at hf369      exact absurd hf (neg_one_ne_one h2)370  · intro he371    obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 2 (by decide) S372    rw [he, Nat.add_zero] at hm373    obtain ⟨a, ha⟩ := exists_pow_half hp (n := 2 * S) (by rw [hS, ← FRC.Nat.mul_assoc])374    have h4 : (a ^ m) ^ 4 = -1 := by375      rw [← pow_mul, show m * 4 = 2 * S by rw [hm, ← FRC.Nat.mul_assoc, Nat.mul_comm m 4]]; exact ha376    exact ⟨a ^ m, by rw [show (8 : Nat) = 4 * 2 from rfl, pow_mul, h4, pow_two, neg_mul_neg, mul_one],377      by rw [h4]; exact neg_one_ne_one h2⟩378379/-- 00:C8, 22:C17, 22:C25, 22:X7, 22:P3 — the Tsirelson square without a generator: `ζ⁴ = −1` gives `(ζ + ζ⁷)² = 2`. -/380theorem tsirelson {ζ : Shell p} (h4 : ζ ^ 4 = -1) : (ζ + ζ ^ 7) * (ζ + ζ ^ 7) = 2 := by381  have h8 : ζ ^ 8 = 1 := by rw [show (8 : Nat) = 4 + 4 from rfl, pow_add, h4, neg_mul_neg, mul_one]382  have hz : ζ * ζ ^ 7 = 1 := by rw [mul_comm, ← pow_succ]; exact h8383  have h14 : ζ ^ 7 * ζ ^ 7 = -(ζ * ζ) := by384    rw [← pow_add, show 7 + 7 = 8 + (4 + 2) from rfl, pow_add, pow_add, h8, h4, one_mul, neg_one_mul, pow_two]385  rw [left_distrib, right_distrib, right_distrib, hz, mul_comm (ζ ^ 7) ζ, hz, h14, two_eq]386  exact add_one_add_one_neg _387388/-- 38:A6 — `2S + 1` is `2⁻¹` on the chart `p = 4S + 1`. -/389theorem two_mul_chart_half {S : Nat} (hS : p = 4 * S + 1) : (2 : Shell p) * ofNat (2 * S + 1) = 1 := ext (by390  show (2 % p * ((2 * S + 1) % p)) % p = 1 % p391  rw [← FRC.Nat.mul_mod _ _ _ Pos.pos,392    show 2 * (2 * S + 1) = p * 1 + 1 by rw [hS, Nat.mul_one, Nat.left_distrib, ← FRC.Nat.mul_assoc],393    FRC.Nat.add_mul_mod_self_left 1 1 p Pos.pos])394395/-- The half-square: on the chart `p = 4S + 1`, `2⁻¹ = 2S + 1` is a square iff `S` is even (Carrier B7, `c² = 2⁻¹`).396A root `c` of `c² = 2⁻¹` gives `ζ = c (1 + i)` with `ζ² = i`, an element of order eight; conversely the octant's `ζ`397gives `(ζ + ζ⁷)² = 2` and `c = (ζ + ζ⁷)/2`. -/398theorem half_square_iff (hp : FRC.Nat.isPrime p) {S : Nat} (hS : p = 4 * S + 1) :399    (∃ c : Shell p, c * c = ofNat (2 * S + 1)) ↔ S % 2 = 0 := by400  have h2 := chart_gt_two hp hS401  have hh := two_mul_chart_half hS402  constructor403  · intro ⟨c, hc⟩404    -- with `i² = −1`, `ζ = c (1 + i)` has `ζ² = c² · 2i = i`: an element of order eight405    obtain ⟨i, hi⟩ := exists_quarter_turn hp hS406    have hh' : (ofNat (2 * S + 1) : Shell p) * (1 + 1) = 1 := by rw [mul_comm, ← two_eq]; exact hh407    have e : (1 + i) * (1 + i) = (1 + 1) * i := by408      rw [left_distrib, right_distrib, right_distrib, one_mul, one_mul, mul_one, hi, right_distrib, one_mul,409        add_comm i (-1), add_add_add_comm, add_neg, zero_add]410    have hz : (c * (1 + i)) * (c * (1 + i)) = i := by411      rw [mul_mul_mul_comm, hc, e, ← mul_assoc, hh', one_mul]412    have hz4 : (c * (1 + i)) ^ 4 = -1 := by413      rw [show (4 : Nat) = 2 * 2 from rfl, pow_mul, pow_two (c * (1 + i)), hz, pow_two, hi]414    exact (octant_sector hp hS).1 ⟨c * (1 + i), by415      rw [show (8 : Nat) = 4 * 2 from rfl, pow_mul, hz4, pow_two, neg_mul_neg, mul_one],416      by rw [hz4]; exact neg_one_ne_one h2⟩417  · intro he418    obtain ⟨ζ, h8, h4⟩ := (octant_sector hp hS).2 he419    have h4' : ζ ^ 4 = -1 :=420      match sq_eq_one hp (by rw [← pow_add]; exact h8 : ζ ^ 4 * ζ ^ 4 = 1) with421      | .inl e => absurd e h4422      | .inr e => e423    refine ⟨(ζ + ζ ^ 7) * ofNat (2 * S + 1), ?_⟩424    rw [mul_mul_mul_comm, tsirelson h4', ← mul_assoc, hh, one_mul]425426/-- Integer parity is frame data: on an odd shell the pair `x ↔ −x` flips the parity of the representative. -/427theorem parity_flips {S : Nat} (hS : p = 4 * S + 1) {x : Shell p} (hx : x ≠ 0) :428    x.val % 2 = 0 ↔ ¬ (-x).val % 2 = 0 := by429  have hneg : (-x).val = p - x.val := by430    show (p - x.val) % p = p - x.val431    exact FRC.Nat.mod_eq_of_lt (Nat.sub_lt Pos.pos (val_pos hx))432  rw [hneg]433  exact FRC.Nat.parity_split (n := 2 * S)434    (by rw [FRC.Nat.add_sub_of_le (Nat.le_of_lt x.lt), hS, ← FRC.Nat.mul_assoc])435436end Prime437end Shell438end FRC439