Algebra.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Fourier34/-!5# 1-algebra — the ledger predicates in Lean (2026-09-16)67Predicates of the paper's ledger (Appendix A of `1-algebra-axioms`, keys `p01001`–`p01033`), stated as the8paper's ledger states them.9Every universal statement is over an arbitrary finite field `F` with `Fintype.card F = 4κ + 1`10(the shell); the window law is on `ZMod p`; instance checks and counts are decided. The section11`conjecture` decides the conclusion's conjecture clause by clause (rows E3, D7, E4; E5, the `SO(3)` obstruction,12is numerical and imported). The section `lie` proves the counting clauses of the Lie-algebra layer: the axis group13of 1:E7, cyclic of order `p − (N|p)`, the window count `2H² + 2H`, and the heights and read-back of 1:E8.14Every docstring opens with the ledger predicate(s) the declaration decides (`1:B2`); theorem numbers are the paper's15(Axioms 2025, 14, 636).16-/1718namespace FRC.Algebra1920open Polynomial2122section shell2324variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]2526/-! ## Block B — the shell -/2728omit [DecidableEq F] in29/-- 1:B2 (Theorem 1, existence clause): on the shell `card F = 4κ+1` a quarter-turn `u` with30`u² = −1` exists. Mathlib: `FiniteField.isSquare_neg_one_iff`. -/31theorem quarter_turn_exists (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) :32    ∃ u : F, u ^ 2 = -1 := by33  have h : IsSquare (-1 : F) := by34    rw [FiniteField.isSquare_neg_one_iff, hκ]; omega35  obtain ⟨u, hu⟩ := h36  exact ⟨u, by rw [sq, ← hu]⟩3738omit [DecidableEq F] in39/-- Helper: the shell has odd cardinality, so `2 ≠ 0` in `F`. -/40theorem two_ne_zero_shell (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) : (2 : F) ≠ 0 := by41  intro h242  have hdvd : ringChar F ∣ 2 := (ringChar.spec F 2).1 (by exact_mod_cast h2)43  have hchar : ringChar F = 2 :=44    ((Nat.dvd_prime Nat.prime_two).1 hdvd).resolve_left CharP.ringChar_ne_one45  have := FiniteField.even_card_of_char_two hchar46  omega4748omit [Fintype F] [DecidableEq F] in49/-- 1:B2 (Theorem 1, orbit clause), 2:D7: for a unit `x` with `x² ≠ 1` and `x² ≠ −1` the four50elements `x, −x, x⁻¹, −x⁻¹` of the Klein-four orbit are pairwise distinct (any field of51characteristic `≠ 2`); the structural set `{1, i, −1, −i}` is exactly the complement. -/52theorem klein_orbit_four (hchar : (2 : F) ≠ 0) (x : F) (hx : x ≠ 0) (h1 : x ^ 2 ≠ 1)53    (hi : x ^ 2 ≠ -1) :54    x ≠ -x ∧ x ≠ x⁻¹ ∧ x ≠ -x⁻¹ ∧ -x ≠ x⁻¹ ∧ -x ≠ -x⁻¹ ∧ x⁻¹ ≠ -x⁻¹ := by55  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩56  · intro h; have : (2 : F) * x = 0 := by linear_combination h57    exact hx ((mul_eq_zero.1 this).resolve_left hchar)58  · intro h; apply h1; rw [sq]; nth_rewrite 2 [h]; exact mul_inv_cancel₀ hx59  · intro h; apply hi; rw [sq]; nth_rewrite 2 [h]; rw [mul_neg, mul_inv_cancel₀ hx]60  · intro h; apply hi; rw [sq]61    have h' : x = -x⁻¹ := by rw [← h, neg_neg]62    nth_rewrite 2 [h']; rw [mul_neg, mul_inv_cancel₀ hx]63  · intro h; apply h1; rw [sq]; have h' : x = x⁻¹ := neg_injective h64    nth_rewrite 2 [h']; exact mul_inv_cancel₀ hx65  · intro h; have : (2 : F) * x⁻¹ = 0 := by linear_combination h66    exact inv_ne_zero hx ((mul_eq_zero.1 this).resolve_left hchar)6768omit [DecidableEq F] in69/-- 1:B2 (Theorem 1, the structural set): the fourth roots of unity number exactly `4` on the70shell. Mathlib: `IsPrimitiveRoot.card_rootsOfUnity`. -/71theorem card_fourth_roots (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) :72    Nat.card (rootsOfUnity 4 F) = 4 := by73  obtain ⟨u, hu⟩ := quarter_turn_exists κ hκ74  have h2 := two_ne_zero_shell κ hκ75  have hm1 : (-1 : F) ≠ 1 := by76    intro h; apply h2; linear_combination -h77  have hu4 : IsPrimitiveRoot u 4 := by78    refine IsPrimitiveRoot.mk_of_lt u (by norm_num) (by rw [show (4:ℕ) = 2 * 2 by rfl, pow_mul, hu]; ring) ?_79    intro l hl hl480    interval_cases l81    · intro h; apply hm1; rw [← hu, pow_one] at *; rw [h]; ring82    · rw [hu]; exact hm183    · intro h; apply hm184      have : u = -1 := by85        have h3 : u ^ 3 = u ^ 2 * u := by ring86        rw [h3, hu] at h; linear_combination -h87      rw [← hu, this]; ring88  exact hu4.card_rootsOfUnity8990omit [DecidableEq F] in91/-- 1:B3 (convention 4, the oriented quarter-turn): `i := −g^κ` satisfies `i² = −1`; and92`g^(2κ) = −1`, the involution behind Definition 5. From `FrcLedger.Fourier`. -/93theorem quarter_turn (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)94    (hg : IsPrimitiveRoot g (Fintype.card F - 1)) :95    (-(g ^ κ)) ^ 2 = -1 ∧ g ^ (2 * κ) = -1 := by96  have h := FRC.DFT.quarter_turn_sq κ hκ g hg97  refine ⟨h, ?_⟩98  rw [← h]; ring99100omit [Fintype F] [DecidableEq F] in101/-- 1:B4 (Definition 2, Lemma 1): in the affine frame `(a, b)`, `φ x = a + b x`102carries `+` and `·` to `⊕` and `⊗`, is a bijection, and the multiplicative unit of the103relabelled field is `a + b`; `b` is the unit only when `a = 0`. -/104theorem affine_frame (a b : F) (hb : b ≠ 0) :105    let φ : F → F := fun x => a + b * x106    let oplus : F → F → F := fun x y => a + b * ((x - a) / b + (y - a) / b)107    let otimes : F → F → F := fun x y => a + b * ((x - a) / b * ((y - a) / b))108    (∀ x y, φ (x + y) = oplus (φ x) (φ y)) ∧109    (∀ x y, φ (x * y) = otimes (φ x) (φ y)) ∧110    Function.Bijective φ ∧111    (∀ y, otimes (a + b) y = y) ∧112    (a ≠ 0 → otimes b (a + b) ≠ a + b) := by113  intro φ oplus otimes114  refine ⟨?_, ?_, ?_, ?_, ?_⟩115  · intro x y; simp only [φ, oplus]; field_simp; ring116  · intro x y; simp only [φ, otimes]; field_simp; ring117  · constructor118    · intro x y h; simp only [φ] at h119      exact mul_left_cancel₀ hb (add_left_cancel h)120    · intro y; exact ⟨(y - a) / b, by simp only [φ]; field_simp; ring⟩121  · intro y; simp only [otimes]; field_simp122    ring123  · intro ha h; simp only [otimes] at h124    -- a + b·((b−a)/b · b/b) = a + b  ⇒  ab = 0  ⇒  a = 0125    field_simp at h126    have hab : a * b = 0 := by linear_combination -h127    exact ha ((mul_eq_zero.1 hab).resolve_right hb)128129omit [DecidableEq F] in130/-- 1:C4 (Definition 5 (a)): the meridian involution `(−a)·g^(n + 2κ) = a·g^n`. -/131theorem meridian_involution (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)132    (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (a : F) (n : ℕ) :133    (-a) * g ^ (n + 2 * κ) = a * g ^ n := by134  rw [pow_add, (quarter_turn κ hκ g hg).2]; ring135136/-! ## Block D — framed numbers -/137138/-- 1:D2 (Definition 6 made precise): the framed-integer window. Integers of absolute value139`≤ H` with `2H < card F` have distinct residues: the cast `ℤ → ZMod p` is injective on the140window. Stated on `ZMod p`. -/141theorem framed_integer_window (p : ℕ) [NeZero p] (H : ℕ) (hH : 2 * H < p) (x y : ℤ)142    (hx : |x| ≤ H) (hy : |y| ≤ H) (h : (x : ZMod p) = (y : ZMod p)) : x = y := by143  have hd : (p : ℤ) ∣ x - y := (ZMod.intCast_eq_intCast_iff_dvd_sub y x p).1 h.symm144  have hlt : |x - y| < (p : ℤ) := by145    calc |x - y| ≤ |x| + |y| := abs_sub _ _146      _ ≤ H + H := by omega147      _ < p := by omega148  have := Int.eq_zero_of_abs_lt_dvd hd hlt149  omega150151omit [DecidableEq F] in152/-- 1:D4 (Lemma 2 restated in the field — scale-periodicity): the scale map153`S n x = x · g^(−n)` on the shell is `(card F − 1)`-periodic in `n`: the residue grids154`G_n = S_n(0..p−1)` coincide as ordered lists. -/155theorem scale_periodic (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (n : ℕ) (x : F) :156    x * (g ^ (n + (Fintype.card F - 1)))⁻¹ = x * (g ^ n)⁻¹ := by157  rw [pow_add, hg.pow_eq_one, mul_one]158159omit [Fintype F] [DecidableEq F] in160/-- 1:E2 (Proposition 5 reversed): adjoining a root of `X² + 1` to a field that already161contains one gives zero divisors — `F[X]/(X²+1)` is not a field on the shell. With `u² = −1`,162`(X + u)(X − u) = 0` in the quotient while both factors are nonzero. -/163theorem complex_chart_zero_divisor (u : F) (hu : u ^ 2 = -1) :164    let R := AdjoinRoot ((X : F[X]) ^ 2 + 1)165    ∃ α β : R, α ≠ 0 ∧ β ≠ 0 ∧ α * β = 0 := by166  intro R167  have hmonic : ((X : F[X]) ^ 2 + 1).Monic := by monicity!168  have hdeg : ((X : F[X]) ^ 2 + 1).natDegree = 2 := by compute_degree!169  refine ⟨AdjoinRoot.root _ + AdjoinRoot.of _ u, AdjoinRoot.root _ - AdjoinRoot.of _ u, ?_, ?_, ?_⟩170  · -- X + u is not divisible by X² + 1171    intro h172    have h' : AdjoinRoot.mk ((X : F[X]) ^ 2 + 1) (X + C u) = 0 := by173      rw [map_add, AdjoinRoot.mk_X, AdjoinRoot.mk_C]; exact h174    rw [AdjoinRoot.mk_eq_zero] at h'175    have hne : (X + C u : F[X]) ≠ 0 := X_add_C_ne_zero u176    have := Polynomial.natDegree_le_of_dvd h' hne177    rw [hdeg, natDegree_X_add_C] at this178    omega179  · intro h180    have h' : AdjoinRoot.mk ((X : F[X]) ^ 2 + 1) (X - C u) = 0 := by181      rw [map_sub, AdjoinRoot.mk_X, AdjoinRoot.mk_C]; exact h182    rw [AdjoinRoot.mk_eq_zero] at h'183    have hne : (X - C u : F[X]) ≠ 0 := X_sub_C_ne_zero u184    have := Polynomial.natDegree_le_of_dvd h' hne185    rw [hdeg, natDegree_X_sub_C] at this186    omega187  · -- (root + u)(root − u) = root² − u² = −1 − (−1) = 0188    have hroot : (AdjoinRoot.root ((X : F[X]) ^ 2 + 1)) ^ 2 = -1 := by189      have := AdjoinRoot.eval₂_root ((X : F[X]) ^ 2 + 1)190      simp only [eval₂_add, eval₂_pow, eval₂_X, eval₂_one] at this191      linear_combination this192    have hu' : (AdjoinRoot.of ((X : F[X]) ^ 2 + 1) u) ^ 2 = -1 := by193      rw [← map_pow, hu, map_neg, map_one]194    linear_combination hroot - hu'195196omit [Fintype F] [DecidableEq F] in197/-- 1:Z1 (Theorem 3): `2s = 0 ⇒ s = 0` in a field of characteristic `≠ 2`: the additive cycle198has no element of order two; the antipode of the origin is not a residue. -/199theorem no_south_pole (hchar : (2 : F) ≠ 0) (s : F) (h : 2 * s = 0) : s = 0 :=200  (mul_eq_zero.1 h).resolve_left hchar201202end shell203204/-! ## Instance predicates on the prime shell `ZMod p` -/205206/-- 1:B3 on `𝔽₁₃`: `g = 2`, `i = −2³ = 5`, `5² = −1`. -/207theorem s13_quarter_turn : (-(2 : ZMod 13) ^ 3) = 5 ∧ (5 : ZMod 13) ^ 2 = -1 := by decide208209/-- 1:V1 the Euclidean step count: the number of non-zero remainders of the Euclidean algorithm on210`(987, 610)` is `13`, against `⌊log₂ 1009⌋ + 1 = 10`; the pair `(55, 34)` needs `7` against211`⌊log₂ 59⌋ + 1 = 6`, the first prime where the count exceeds the logarithmic bound. -/212def euclidSteps : ℕ → ℕ → ℕ → ℕ213  | 0, _, _ => 0214  | fuel + 1, a, b => if b = 0 then 0 else (if a % b = 0 then 0 else 1) + euclidSteps fuel b (a % b)215216theorem euclid_step_count :217    euclidSteps 40 987 610 = 13 ∧ Nat.log 2 1009 + 1 = 10 ∧218    euclidSteps 40 55 34 = 7 ∧ Nat.log 2 59 + 1 = 6 := by219  decide220221/-- 1:D6 (Theorem approx, the range at `p = 13`, `g = 2`): every grid point222`x/2^n` with `0 ≤ x < 13` and `n ≥ 3` is `≤ 3/2`, so no grid point at resolution `1/8` lies223within `1/16` of `33/10`: range and resolution trade off at fixed window. -/224theorem approx_obstruction :225    ∀ n : ℕ, 3 ≤ n → ∀ x : ℕ, x < 13 → ((x : ℚ) / 2 ^ n) ≤ 3 / 2 := by226  intro n hn x hx227  have h2 : (8 : ℚ) ≤ 2 ^ n := by228    calc (8 : ℚ) = 2 ^ 3 := by norm_num229      _ ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) hn230  have hx' : (x : ℚ) ≤ 12 := by exact_mod_cast (by omega : x ≤ 12)231  rw [div_le_iff₀ (by positivity)]232  nlinarith233234section conjecture235236open Real237238/-- 1:E3 (the conjecture's first clause, solving): `f ∈ F_p[X]` has a root in `F_p` iff `f` and239`X^p − X = ∏_a (X − a)` are not coprime — the root test is a gcd, exact in the substrate. -/240theorem root_iff_not_coprime (p : ℕ) [hp : Fact p.Prime] (f : (ZMod p)[X]) :241    (∃ a : ZMod p, f.eval a = 0) ↔ ¬ IsCoprime f (X ^ p - X) := by242  constructor243  · rintro ⟨a, ha⟩ hcop244    have h1 : (X - C a) ∣ f := dvd_iff_isRoot.mpr ha245    have h2 : (X - C a) ∣ (X ^ p - X : (ZMod p)[X]) := by246      rw [dvd_iff_isRoot]247      simp [IsRoot, ZMod.pow_card]248    exact (not_isUnit_X_sub_C a) (hcop.isUnit_of_dvd' h1 h2)249  · intro h250    by_contra hno251    push Not at hno252    apply h253    have hprod : (X ^ p - X : (ZMod p)[X]) = ∏ a : ZMod p, (X - C a) := by254      have hroots : (X ^ p - X : (ZMod p)[X]).roots = Finset.univ.val := by255        have := FiniteField.roots_X_pow_card_sub_X (ZMod p); rwa [ZMod.card] at this256      have hmon : (X ^ p - X : (ZMod p)[X]).Monic := by257        apply monic_X_pow_sub258        simpa using hp.out.one_lt259      have hdeg : (X ^ p - X : (ZMod p)[X]).natDegree = p := FiniteField.X_pow_card_sub_X_natDegree_eq (ZMod p) hp.out.one_lt260      have := (prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmon (by rw [hroots, hdeg]; simp)).symm261      rw [this, hroots]262      rfl263    rw [hprod]264    refine IsCoprime.prod_right fun a _ => ?_265    have hirr : Irreducible (X - C a : (ZMod p)[X]) := irreducible_X_sub_C a266    exact (hirr.coprime_iff_not_dvd.mpr (fun hd => hno a (dvd_iff_isRoot.mp hd))).symm267268/-- 1:D7 (second clause, limit-like approximation): the tower of shells resolves every real — for every269`r` and `ε > 0` some shell `p = 4κ + 1` carries a framed rational `x / 2^n`, `|x| ≤ 2κ`, within `ε` of `r`270(Dirichlet for primes `≡ 1 (mod 4)`, `Nat.exists_prime_gt_modEq_one`). -/271theorem tower_density (r ε : ℝ) (hε : 0 < ε) :272    ∃ p κ n : ℕ, ∃ x : ℤ, p.Prime ∧ p = 4 * κ + 1 ∧ |x| ≤ 2 * κ ∧ |r - x / 2 ^ n| < ε := by273  obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hε (by norm_num : (1 / 2 : ℝ) < 1)274  set x : ℤ := round (r * 2 ^ n) with hx275  obtain ⟨p, hp, hgt, hmod⟩ := Nat.exists_prime_gt_modEq_one (2 * x.natAbs + 1) (by norm_num : (4 : ℕ) ≠ 0)276  have hmod' : p % 4 = 1 := by277    have := hmod; unfold Nat.ModEq at this; simpa using this278  refine ⟨p, p / 4, n, x, hp, ?_, ?_, ?_⟩279  · have := Nat.div_add_mod p 4; omega280  · have h1 : x.natAbs < 2 * (p / 4) := by omega281    have h2 : (|x| : ℤ) = x.natAbs := (Int.natCast_natAbs x).symm282    rw [h2]; exact_mod_cast h1.le283  · have hr : |r * 2 ^ n - x| ≤ 1 / 2 := abs_sub_round (r * 2 ^ n)284    have h2n : (0 : ℝ) < 2 ^ n := by positivity285    have : r - x / 2 ^ n = (r * 2 ^ n - x) / 2 ^ n := by field_simp286    rw [this, abs_div, abs_of_pos h2n]287    calc |r * 2 ^ n - x| / 2 ^ n ≤ (1 / 2) / 2 ^ n := by gcongr288      _ = (1 / 2) ^ n / 2 := by rw [one_div_pow]; ring289      _ < ε := by linarith290291/-- 1:E4 (third clause, the abelian case): the rounding `k(θ) = round(Nθ/2π)` puts `2πk/N` within `π/N`292of `θ` — `C_N ≅ F_p^×` (`N = p − 1`) is a `π/N`-net of `U(1)`. -/293theorem circle_net (N : ℕ) (hN : 0 < N) (θ : ℝ) :294    |θ - 2 * π * (round (N * θ / (2 * π)) : ℝ) / N| ≤ π / N := by295  have hπ : (0 : ℝ) < π := pi_pos296  have hN' : (0 : ℝ) < N := by exact_mod_cast hN297  set t := N * θ / (2 * π) with ht298  have hθ : θ = 2 * π * t / N := by rw [ht]; field_simp299  have hr : |t - round t| ≤ 1 / 2 := abs_sub_round t300  have : θ - 2 * π * (round t : ℝ) / N = (2 * π / N) * (t - round t) := by rw [hθ]; field_simp301  rw [this, abs_mul, abs_of_pos (by positivity : (0 : ℝ) < 2 * π / N)]302  calc 2 * π / N * |t - round t| ≤ 2 * π / N * (1 / 2) := by gcongr303    _ = π / N := by ring304305/-- 1:E4 (third clause): the group-law defect of the rounding is at most one step. -/306theorem group_law_defect (N : ℕ) (θ₁ θ₂ : ℝ) :307    |round (N * θ₁ / (2 * π)) + round (N * θ₂ / (2 * π)) - round (N * (θ₁ + θ₂) / (2 * π))| ≤ 1 := by308  set t₁ := N * θ₁ / (2 * π) with ht₁309  set t₂ := N * θ₂ / (2 * π) with ht₂310  have hsum : N * (θ₁ + θ₂) / (2 * π) = (t₁ - round t₁) + (t₂ - round t₂) + ((round t₁ + round t₂ : ℤ) : ℝ) := by311    rw [ht₁, ht₂]; push_cast; ring312  rw [hsum, round_add_intCast]313  have h1 : |t₁ - round t₁| ≤ 1 / 2 := abs_sub_round t₁314  have h2 : |t₂ - round t₂| ≤ 1 / 2 := abs_sub_round t₂315  set z := (t₁ - round t₁) + (t₂ - round t₂) with hz316  have hz1 : |z| ≤ 1 := by rw [hz]; calc |_| ≤ |t₁ - round t₁| + |t₂ - round t₂| := abs_add_le _ _317    _ ≤ 1 := by linarith318  have hrz : |z - round z| ≤ 1 / 2 := abs_sub_round z319  have hlt : (|round z| : ℝ) < 2 := by320    have : |(round z : ℝ)| ≤ |z| + |z - round z| := by321      calc |(round z : ℝ)| = |z - (z - round z)| := by ring_nf322        _ ≤ |z| + |z - round z| := abs_sub _ _323    linarith324  have hlt' : |round z| < 2 := by exact_mod_cast hlt325  have hz' : round t₁ + round t₂ - (round z + (round t₁ + round t₂)) = -round z := by ring326  rw [hz', abs_neg]; omega327328end conjecture329330section lie331332/-! ### 1:E7, 1:E8 — the Lie-algebra layer: the axis group, the window count, the heights and the read-back -/333334open QuadraticAlgebra335336variable (p : ℕ) [Fact p.Prime]337338/-- The axis algebra of a pure quaternion `v` with `N(v) = d`: the pairs `a + t v`, with `v² = −d`. -/339abbrev AxisAlg (d : ZMod p) := QuadraticAlgebra (ZMod p) (-d) 0340341/-- The scalars inside the axis group. -/342noncomputable def scalars (d : ZMod p) : Subgroup (AxisAlg p d)ˣ :=343  (Units.map (algebraMap (ZMod p) (AxisAlg p d) : ZMod p →* AxisAlg p d)).range344345instance (d : ZMod p) : Finite (AxisAlg p d) := Finite.of_equiv _ (QuadraticAlgebra.equivProd (-d) 0).symm346347theorem card_axisAlg (d : ZMod p) : Nat.card (AxisAlg p d) = p * p := by348  rw [Nat.card_congr (QuadraticAlgebra.equivProd (-d) 0), Nat.card_prod, Nat.card_zmod]349350theorem card_scalars (d : ZMod p) : Nat.card (scalars p d) = p - 1 := by351  unfold scalars352  rw [MonoidHom.range_eq_map, Subgroup.card_map_of_injective, Subgroup.card_top, Nat.card_eq_fintype_card, ZMod.card_units]353  intro x y h354  apply Units.ext355  have := congrArg Units.val h356  simpa using (algebraMap (ZMod p) (AxisAlg p d)).injective this357358/-- 1:E7, the axis group when `−d` is not a square: cyclic of order `p + 1`. -/359theorem axis_field (d : ZMod p) [Fact (¬ IsSquare (-d))] :360    IsCyclic ((AxisAlg p d)ˣ ⧸ scalars p d) ∧ Nat.card ((AxisAlg p d)ˣ ⧸ scalars p d) = p + 1 := by361  refine ⟨isCyclic_of_surjective (QuotientGroup.mk' _) (QuotientGroup.mk'_surjective _), ?_⟩362  have hU : Nat.card (AxisAlg p d)ˣ = p * p - 1 := by363    rw [Nat.card_units, card_axisAlg]364  have hL := Subgroup.card_eq_card_quotient_mul_card_subgroup (scalars p d)365  rw [hU, card_scalars] at hL366  have h2 : 2 ≤ p := (Fact.out : p.Prime).two_le367  have : p * p - 1 = (p + 1) * (p - 1) := by368    have := Nat.mul_self_sub_mul_self_eq p 1369    simpa using this370  rw [this] at hL371  exact (Nat.eq_of_mul_eq_mul_right (by omega) hL).symm372373/-- The reading of the axis algebra at a square root `r` of `−d`: `a + t v ↦ a + r t`, a ring map. -/374def psiK {K : Type*} [Field K] (d r : K) (hr : r * r = -d) : QuadraticAlgebra K (-d) 0 →+* K where375  toFun z := z.re + r * z.im376  map_one' := by simp377  map_mul' x y := by378    simp only [QuadraticAlgebra.re_mul, QuadraticAlgebra.im_mul]379    linear_combination (-(x.im * y.im)) * hr380  map_zero' := by simp381  map_add' x y := by simp; ring382383theorem psiK_apply {K : Type*} [Field K] (d r : K) (hr : r * r = -d) (z : QuadraticAlgebra K (-d) 0) :384    psiK d r hr z = z.re + r * z.im := rfl385386/-- 1:E7, the axis group when `−d = r²` with `r ≠ 0` (characteristic not two): the units modulo the scalars are387isomorphic to `Kˣ`. -/388theorem axis_split_equiv {K : Type*} [Field K] (h2 : (2 : K) ≠ 0) (d r : K) (hr : r * r = -d) (hr0 : r ≠ 0) :389    Nonempty ((QuadraticAlgebra K (-d) 0)ˣ ⧸390      (Units.map (algebraMap K (QuadraticAlgebra K (-d) 0) : K →* QuadraticAlgebra K (-d) 0)).range ≃* Kˣ) := by391  have hr' : (-r) * (-r) = -d := by linear_combination hr392  let f₁ : (QuadraticAlgebra K (-d) 0)ˣ →* Kˣ := Units.map (psiK d r hr : QuadraticAlgebra K (-d) 0 →* K)393  let f₂ : (QuadraticAlgebra K (-d) 0)ˣ →* Kˣ := Units.map (psiK d (-r) hr' : QuadraticAlgebra K (-d) 0 →* K)394  let φ : (QuadraticAlgebra K (-d) 0)ˣ →* Kˣ := f₁ * f₂⁻¹395  have h2r : (2 * r) ≠ 0 := mul_ne_zero h2 hr0396  have hdet : ∀ x y : QuadraticAlgebra K (-d) 0, psiK d r hr x = psiK d r hr y → psiK d (-r) hr' x = psiK d (-r) hr' y → x = y := by397    intro x y h1 h2'398    rw [psiK_apply, psiK_apply] at h1 h2'399    have him : x.im = y.im := by400      have : (2 * r) * (x.im - y.im) = 0 := by linear_combination h1 - h2'401      rcases mul_eq_zero.mp this with h | h402      · exact absurd h h2r403      · exact sub_eq_zero.mp h404    have hre : x.re = y.re := by rw [him] at h1; linear_combination h1405    exact QuadraticAlgebra.ext hre him406  have hker : φ.ker = (Units.map (algebraMap K (QuadraticAlgebra K (-d) 0) : K →* QuadraticAlgebra K (-d) 0)).range := by407    ext z408    rw [MonoidHom.mem_ker, MonoidHom.mem_range]409    constructor410    · intro h411      have h' : f₁ z = f₂ z := by412        have := congrArg (· * f₂ z) h413        simpa [φ] using this414      have hv := congrArg Units.val h'415      simp only [f₁, f₂, Units.coe_map, MonoidHom.coe_ofClass, psiK_apply] at hv416      have him : (z : QuadraticAlgebra K (-d) 0).im = 0 := by417        have : (2 * r) * (z : QuadraticAlgebra K (-d) 0).im = 0 := by linear_combination hv418        rcases mul_eq_zero.mp this with h | h419        · exact absurd h h2r420        · exact h421      have hre0 : (z : QuadraticAlgebra K (-d) 0).re ≠ 0 := by422        intro h0423        exact z.ne_zero (QuadraticAlgebra.ext (by simpa using h0) (by simpa using him))424      refine ⟨Units.mk0 _ hre0, ?_⟩425      apply Units.ext426      exact QuadraticAlgebra.ext (by simp) (by simp [him])427    · rintro ⟨c, rfl⟩428      apply Units.ext429      simp [φ, f₁, f₂, psiK_apply]430  have hsurj : Function.Surjective φ := by431    intro y432    let zf : Kˣ → QuadraticAlgebra K (-d) 0 := fun y => ⟨((y : K) + 1) / 2, ((y : K) - 1) / (2 * r)⟩433    have e1 : ∀ y : Kˣ, psiK d r hr (zf y) = y := by434      intro y; rw [psiK_apply]; show ((y : K) + 1) / 2 + r * (((y : K) - 1) / (2 * r)) = y; field_simp; ring435    have e2 : ∀ y : Kˣ, psiK d (-r) hr' (zf y) = 1 := by436      intro y; rw [psiK_apply]; show ((y : K) + 1) / 2 + -r * (((y : K) - 1) / (2 * r)) = 1; field_simp; ring437    have hmul : zf y * zf y⁻¹ = 1 :=438      hdet _ _ (by rw [map_mul, map_one, e1, e1]; simp) (by rw [map_mul, map_one, e2, e2, mul_one])439    have hmul' : zf y⁻¹ * zf y = 1 := by rw [mul_comm]; exact hmul440    let u : (QuadraticAlgebra K (-d) 0)ˣ := ⟨zf y, zf y⁻¹, hmul, hmul'⟩441    have hu1 : f₁ u = y := Units.ext (e1 y)442    have hu2 : f₂ u = 1 := Units.ext (e2 y)443    exact ⟨u, by simp [φ, hu1, hu2]⟩444  exact ⟨(QuotientGroup.quotientMulEquivOfEq hker.symm).trans (QuotientGroup.quotientKerEquivOfSurjective φ hsurj)⟩445446/-- 1:E7, the axis group on the shell when `−d = r²`, `r ≠ 0`: cyclic of order `p − 1`. -/447theorem axis_split (hp2 : p ≠ 2) (d r : ZMod p) (hr : r * r = -d) (hr0 : r ≠ 0) :448    IsCyclic ((AxisAlg p d)ˣ ⧸ scalars p d) ∧ Nat.card ((AxisAlg p d)ˣ ⧸ scalars p d) = p - 1 := by449  have h2 : (2 : ZMod p) ≠ 0 := Ring.two_ne_zero (by rw [ZMod.ringChar_zmod_n]; exact hp2)450  obtain ⟨e⟩ := axis_split_equiv h2 d r hr hr0451  refine ⟨isCyclic_of_surjective e.symm.toMonoidHom e.symm.surjective, ?_⟩452  exact (Nat.card_congr e.toEquiv).trans (by rw [Nat.card_eq_fintype_card, ZMod.card_units])453454/-- 1:E7, the rotation group of an axis `v` on a shell `p ≡ 1 (mod 4)`, `N(v) = N ≢ 0`: the pairs `a + t v` modulo455the scalars form a cyclic group of order `p − (N|p)`. -/456theorem axis_group (hp4 : p % 4 = 1) (N : ℤ) (hN : (N : ZMod p) ≠ 0) :457    IsCyclic ((AxisAlg p N)ˣ ⧸ scalars p N) ∧ (Nat.card ((AxisAlg p N)ˣ ⧸ scalars p N) : ℤ) = p - legendreSym p N := by458  have hp2 : p ≠ 2 := by omega459  have hneg : legendreSym p (-N) = legendreSym p N := by460    rw [show -N = (-1) * N by ring, legendreSym.mul, legendreSym.at_neg_one hp2, ZMod.χ₄_nat_one_mod_four hp4, one_mul]461  have hNn : ((-N : ℤ) : ZMod p) ≠ 0 := by push_cast; exact neg_ne_zero.mpr hN462  by_cases hs : IsSquare (-(N : ZMod p))463  · obtain ⟨r, hr⟩ := hs464    have hr0 : r ≠ 0 := by rintro rfl; exact hN (neg_eq_zero.mp (hr.trans (mul_zero 0)))465    obtain ⟨hc, hcard⟩ := axis_split p hp2 (N : ZMod p) r hr.symm hr0466    refine ⟨hc, ?_⟩467    have h1 : legendreSym p (-N) = 1 := (legendreSym.eq_one_iff p hNn).mpr (by push_cast; exact ⟨r, hr⟩)468    rw [hcard, ← hneg, h1]469    have := (Fact.out : p.Prime).two_le470    omega471  · have : Fact (¬ IsSquare (-(N : ZMod p))) := ⟨hs⟩472    obtain ⟨hc, hcard⟩ := axis_field p (N : ZMod p)473    refine ⟨hc, ?_⟩474    have h1 : legendreSym p (-N) = -1 := (legendreSym.eq_neg_one_iff p).mpr (by push_cast; exact hs)475    rw [hcard, ← hneg, h1]476    push_cast; ring477478/-- The window pairs `(a, t)`, `|a|, |t| ≤ H`, not both zero. -/479def winPairs (H : ℕ) : Finset (ℤ × ℤ) := ((Finset.Icc (-(H : ℤ)) H) ×ˢ (Finset.Icc (-(H : ℤ)) H)).erase 0480481/-- One pair of each sign class `±(a, t)`: `t > 0`, or `t = 0` and `a > 0`. -/482def halfPairs (H : ℕ) : Finset (ℤ × ℤ) :=483  ((Finset.Icc (-(H : ℤ)) H) ×ˢ (Finset.Icc (1 : ℤ) H)) ∪ ((Finset.Icc (1 : ℤ) H) ×ˢ {0})484485theorem card_halfPairs (H : ℕ) : (halfPairs H).card = 2 * H * H + 2 * H := by486  unfold halfPairs487  rw [Finset.card_union_of_disjoint]488  · simp only [Finset.card_product, Int.card_Icc, Finset.card_singleton]489    have h1 : ((H : ℤ) + 1 - -(H : ℤ)).toNat = 2 * H + 1 := by omega490    have h2 : ((H : ℤ) + 1 - 1).toNat = H := by omega491    rw [h1, h2]; ring492  · rw [Finset.disjoint_left]493    rintro ⟨a, t⟩ h1 h2494    simp only [Finset.mem_product, Finset.mem_Icc, Finset.mem_singleton] at h1 h2495    omega496497/-- 1:E7, the window count: a map of the window pairs that takes `x` and `−x` to the same value (the rotation498`ρ_{a + t v₀}`: `ρ_{−q} = ρ_q`) takes at most `2H² + 2H` values. -/499theorem card_image_le_of_neg {β : Type*} [DecidableEq β] (H : ℕ) (f : ℤ × ℤ → β) (hf : ∀ x, f (-x) = f x) :500    ((winPairs H).image f).card ≤ 2 * H * H + 2 * H := by501  rw [← card_halfPairs H]502  refine le_trans (Finset.card_le_card (t := (halfPairs H).image f) ?_) Finset.card_image_le503  intro y hy504  simp only [Finset.mem_image, winPairs, Finset.mem_erase, Finset.mem_product, Finset.mem_Icc] at hy ⊢505  obtain ⟨⟨a, t⟩, ⟨hne, ⟨ha1, ha2⟩, ⟨ht1, ht2⟩⟩, rfl⟩ := hy506  by_cases hpos : 0 < t ∨ (t = 0 ∧ 0 < a)507  · refine ⟨(a, t), ?_, rfl⟩508    simp only [halfPairs, Finset.mem_union, Finset.mem_product, Finset.mem_Icc, Finset.mem_singleton]509    omega510  · refine ⟨(-a, -t), ?_, ?_⟩511    · have hne' : (a, t) ≠ (0, 0) := hne512      simp only [halfPairs, Finset.mem_union, Finset.mem_product, Finset.mem_Icc, Finset.mem_singleton]513      have : ¬ (a = 0 ∧ t = 0) := fun h => hne' (by rw [h.1, h.2])514      omega515    · exact hf (a, t)516517section heights518519open Quaternion520521/-- 1:E8, the height law: a window quaternion `q` (integer coordinates of size at most `H`) has every coordinate522of `q^m` of size at most `(2H)^m` — the norm is multiplicative and at most `4H²` on the window. -/523theorem quat_pow_height (H : ℤ) (q : ℍ[ℤ]) (hr : |q.re| ≤ H) (hi : |q.imI| ≤ H) (hj : |q.imJ| ≤ H) (hk : |q.imK| ≤ H) (m : ℕ) :524    |(q ^ m).re| ≤ (2 * H) ^ m ∧ |(q ^ m).imI| ≤ (2 * H) ^ m ∧ |(q ^ m).imJ| ≤ (2 * H) ^ m ∧ |(q ^ m).imK| ≤ (2 * H) ^ m := by525  have hH : 0 ≤ H := le_trans (abs_nonneg _) hr526  have hn : normSq q ≤ (2 * H) ^ 2 := by527    rw [normSq_def']528    have h1 := sq_le_sq' (abs_le.mp hr).1 (abs_le.mp hr).2529    have h2 := sq_le_sq' (abs_le.mp hi).1 (abs_le.mp hi).2530    have h3 := sq_le_sq' (abs_le.mp hj).1 (abs_le.mp hj).2531    have h4 := sq_le_sq' (abs_le.mp hk).1 (abs_le.mp hk).2532    nlinarith533  have hpow : normSq (q ^ m) ≤ ((2 * H) ^ m) ^ 2 := by534    rw [map_pow, ← pow_mul, mul_comm m 2, pow_mul]535    exact pow_le_pow_left₀ (normSq_nonneg) hn m536  have hb : 0 ≤ (2 * H) ^ m := pow_nonneg (by linarith) m537  have key : ∀ c : ℤ, c ^ 2 ≤ normSq (q ^ m) → |c| ≤ (2 * H) ^ m := fun c hc =>538    abs_le_of_sq_le_sq' (le_trans hc hpow) hb |> fun h => abs_le.mpr h539  rw [normSq_def'] at hpow540  refine ⟨key _ ?_, key _ ?_, key _ ?_, key _ ?_⟩ <;> rw [normSq_def'] <;> nlinarith [sq_nonneg (q ^ m).re, sq_nonneg (q ^ m).imI, sq_nonneg (q ^ m).imJ, sq_nonneg (q ^ m).imK]541542/-- 1:E8, read-back (the window law D2 coordinate by coordinate): an integer `c` is the signed reading of its residue543on the shell `p` (odd) exactly when `2|c| < p`. -/544theorem readback_iff (p : ℕ) [Fact p.Prime] (hp : p ≠ 2) (c : ℤ) : ((c : ZMod p).valMinAbs = c) ↔ 2 * |c| < p := by545  rw [ZMod.valMinAbs_spec]546  have hodd : (p : ℤ) % 2 = 1 := by547    have := (Fact.out : p.Prime).eq_one_or_self_of_dvd 2548    omega549  constructor550  · rintro ⟨_, h1, h2⟩551    rcases abs_cases c with ⟨h, _⟩ | ⟨h, _⟩ <;> rw [h] <;> omega552  · intro h553    refine ⟨rfl, ?_, ?_⟩ <;> rcases abs_cases c with ⟨h', _⟩ | ⟨h', _⟩ <;> rw [h'] at h <;> omega554555end heights556557end lie558559-- Ledger predicates of 1-algebra (generated by make_predicates.py from docs/1-algebra/1-algebra-ledger.json; edit the ledger, not this section)560/-- 1:B2 (p01004) — Symmetry completeness (Thm.~\ref{thm:symmetric-completeness}): the fourth roots of unity form the unique order-four subgroup $Q_4=\{1,\im,-1,-\im\}$; under the Klein four-group $\langle x\mapsto-x,\,x\mapsto x^{-1}\rangle$, $Q_4$ is the union of the two size-two orbits $\{\pm1\}$, $\{\pm\im\}$, and $\Fpx\setminus Q_4$ splits into exactly $\kap-1$ orbits of size four. For $\p\equiv3\pmod4$ no $\im$ exists. -/561theorem p01004 : (∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → ∃ u, u ^ (2 : ℕ) = (-1 : F)) ∧ (∀ {F : Type u_2} [Field F], (2 : F) ≠ (0 : F) → ∀ (x : F), x ≠ (0 : F) → x ^ (2 : ℕ) ≠ (1 : F) → x ^ (2 : ℕ) ≠ (-1 : F) → x ≠ -x ∧ x ≠ x⁻¹ ∧ x ≠ -x⁻¹ ∧ -x ≠ x⁻¹ ∧ -x ≠ -x⁻¹ ∧ x⁻¹ ≠ -x⁻¹) ∧ ∀ {F : Type u_3} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → Nat.card ↥(rootsOfUnity (4 : ℕ) F) = (4 : ℕ) :=562  And.intro @FRC.Algebra.quarter_turn_exists (And.intro @FRC.Algebra.klein_orbit_four (@FRC.Algebra.card_fourth_roots))563/-- 1:B3 (p01005) — The oriented quarter-turn: $\im=-\gen^{\kap}$ satisfies $\im^{2}=-1$ for every primitive root $\gen$; the two square roots of $-1$ are $\{-\gen^{\kap},\gen^{\kap}\}$, so the drive fixes which is $\im$. On $\F_{13}$, $\gen=2$: $\im=5$. -/564theorem p01005 : (∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → (-g ^ κ) ^ (2 : ℕ) = (-1 : F) ∧ g ^ ((2 : ℕ) * κ) = (-1 : F)) ∧ -(2 : ZMod (13 : ℕ)) ^ (3 : ℕ) = (5 : ZMod (13 : ℕ)) ∧ (5 : ZMod (13 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (13 : ℕ)) :=565  And.intro @FRC.Algebra.quarter_turn (@FRC.Algebra.s13_quarter_turn)566/-- 1:B4 (p01006) — Affine reframing (Def.~\ref{def:framed-field}, Lemma~\ref{lem:affine-invariance}): $\varphi_{a,b}(x)=a+bx$, $b\neq0$, is a ring isomorphism $(\Fp,+,\cdot)\to(\Fp,\oplus,\otimes)$ with origin $a$ and unit $a+b$; every polynomial identity is frame-covariant. -/567theorem p01006 : ∀ {F : Type u_1} [Field F] (a b : F), b ≠ (0 : F) → have φ := fun x => a + b * x; have oplus := fun x y => a + b * ((x - a) / b + (y - a) / b); have otimes := fun x y => a + b * ((x - a) / b * ((y - a) / b)); (∀ (x y : F), φ (x + y) = oplus (φ x) (φ y)) ∧ (∀ (x y : F), φ (x * y) = otimes (φ x) (φ y)) ∧ Function.Bijective φ ∧ (∀ (y : F), otimes (a + b) y = y) ∧ (a ≠ (0 : F) → otimes b (a + b) ≠ a + b) :=568  @FRC.Algebra.affine_frame569/-- 1:C4 (p01011) — Involutions and counts (Def.~\ref{def:orbit-sphere}\,(a)--(c)): $M_n(a)=M_{n+2\kap}(-a)$ and $L_a(m)=L_{-a}(m+2\kap)$ since $\gen^{2\kap}=-1$; $\p-1$ distinct meridian lists in $2\kap$ great circles; $2\kap$ latitude pairs; one-sided vertex count $(\p-1)^{2}/2+1$, the double cover $(\p-1)^{2}$ (00:B11). -/570theorem p01011 : ∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → ∀ (a : F) (n : ℕ), -a * g ^ (n + (2 : ℕ) * κ) = a * g ^ n :=571  @FRC.Algebra.meridian_involution572/-- 1:D2 (p01013) — The window law: $z\mapsto z\bmod\p$ is injective on $W_H$ when $2H<\p$; for $x,y\in W_H$ the residue of $x\pm y$ reads back the integer when $4H<\p$, and that of $xy$ when $2H^{2}<\p$ (the same injectivity on the windows $2H$ and $H^{2}$). -/573theorem p01013 : ∀ (p : Nat) [@NeZero Nat (@MulZeroClass.toZero Nat Nat.instMulZeroClass) p] (H : Nat), @LT.lt Nat instLTNat (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) H) p → ∀ (x y : Int), @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup x) (@Nat.cast Int instNatCastInt H) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup y) (@Nat.cast Int instNatCastInt H) → @Eq (ZMod p) (@Int.cast (ZMod p) (@AddGroupWithOne.toIntCast (ZMod p) (@Ring.toAddGroupWithOne (ZMod p) (@CommRing.toRing (ZMod p) (ZMod.commRing p)))) x) (@Int.cast (ZMod p) (@AddGroupWithOne.toIntCast (ZMod p) (@Ring.toAddGroupWithOne (ZMod p) (@CommRing.toRing (ZMod p) (ZMod.commRing p)))) y) → @Eq Int x y :=574  @FRC.Algebra.framed_integer_window575/-- 1:D4 (p01015) — Scale-periodicity (Lemma~\ref{thm:scale-periodicity}, in the field): $S_n(x)=x\gen^{-n}$ satisfies $S_{n+(\p-1)}=S_n$; the grids $G_n$ are $(\p-1)$-periodic as ordered lists; the zoom $[x,n]\mapsto[x,n+1]$ has order $\p-1$. As lists of rationals $x/\gen^{n}$ ($\gen$ lifted to $\Z$) the grids are not periodic: the periodicity is a relation of the field. -/576theorem p01015 : ∀ {F : Type u_1} [Field F] [Fintype F] (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → ∀ (n : ℕ) (x : F), x * (g ^ (n + (Fintype.card F - (1 : ℕ))))⁻¹ = x * (g ^ n)⁻¹ :=577  @FRC.Algebra.scale_periodic578/-- 1:D7 (p01027) — Limit-like approximation (second clause), across the tower: for every real $r$ and $\varepsilon>0$ some shell $\p=4\kap+1$ carries a framed rational $x/2^{n}$, $|x|\le2\kap$, within $\varepsilon$ of $r$ (primes $\equiv1\pmod4$ beyond every bound). One shell trades range for resolution; the limit is the tower, not a completion. -/579theorem p01027 : ∀ (r ε : ℝ), (0 : ℝ) < ε → ∃ p κ n x, Nat.Prime p ∧ p = (4 : ℕ) * κ + (1 : ℕ) ∧ |x| ≤ (2 : ℤ) * ↑κ ∧ |r - ↑x / (2 : ℝ) ^ n| < ε :=580  @FRC.Algebra.tower_density581/-- 1:E2 (p01019) — The extension by $X^{2}+1$ is trivial (Prop.~\ref{prop:Cp-field} reversed): on the shell $\Fp[X]/(X^{2}+1)\cong\Fp\times\Fp$ has zero divisors, $(X+\im)(X-\im)=0$, so it is not a field; $\Fp[X]/(X^{2}+1)$ is a field exactly when $\p\equiv3\pmod4$; the quadratic extension of the shell is $\Fp[\eta]$, $\eta^{2}=\nu$ a non-square (8-dirac B6). -/582theorem p01019 : ∀ {F : Type u_1} [Field F] (u : F), u ^ (2 : ℕ) = (-1 : F) → let R := AdjoinRoot (Polynomial.X ^ (2 : ℕ) + (1 : Polynomial F)); ∃ α β, α ≠ (0 : R) ∧ β ≠ (0 : R) ∧ α * β = (0 : R) :=583  @FRC.Algebra.complex_chart_zero_divisor584/-- 1:E3 (p01026) — Solving in the substrate (first clause): $f\in\Fp[X]$ has a root in $\Fp$ iff $f$ and $X^{\p}-X=\prod_{a}(X-a)$ are not coprime; the gcd counts the distinct roots and Cantor--Zassenhaus splitting finds them, exactly. An equation without a root in $\Fp$ is recognised, not extended (E2). -/585theorem p01026 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (f : Polynomial (ZMod p)), (∃ a, Polynomial.eval a f = (0 : ZMod p)) ↔ ¬IsCoprime f (Polynomial.X ^ p - Polynomial.X) :=586  @FRC.Algebra.root_iff_not_coprime587/-- 1:E4 (p01028) — Continuous symmetry, the abelian case (third clause): $\Fpx\simeq C_{\p-1}\simeq SO(2,\Fp)$ (6:E2) is a $\pi/(\p-1)$-net of $U(1)$ under $k\mapsto e^{2\pi\im k/(\p-1)}$; the rounding $k(\theta)=\lfloor(\p-1)\theta/2\pi+\tfrac12\rfloor$ has angle and chord error $\le\pi/(\p-1)$ and group-law defect at most one step. -/588theorem p01028 : (∀ (N : ℕ), (0 : ℕ) < N → ∀ (θ : ℝ), |θ - (2 : ℝ) * Real.pi * ↑(round (↑N * θ / ((2 : ℝ) * Real.pi))) / ↑N| ≤ Real.pi / ↑N) ∧ ∀ (N : ℕ) (θ₁ θ₂ : ℝ), |round (↑N * θ₁ / ((2 : ℝ) * Real.pi)) + round (↑N * θ₂ / ((2 : ℝ) * Real.pi)) - round (↑N * (θ₁ + θ₂) / ((2 : ℝ) * Real.pi))| ≤ (1 : ℤ) :=589  And.intro @FRC.Algebra.circle_net (@FRC.Algebra.group_law_defect)590/-- 1:E7 (p01032) — The Lie-algebra layer, one axis: on a shell $\p>8H^{2}$, for $q=a+v\in W_H^{4}$ with $v\ne0$, the rotation $\rho_q\colon x\mapsto qxq^{-1}$ is the Cayley step (8:C3) of the self-adjoint $\eta S_v$ (E2's $\eta$, $S_vx=v\times x$, $N(v)=v\cdot v$) at $\alpha=\eta/(\nu a)$, and the half-turn $U_\infty=I+2N(v)^{-1}S_v^{2}$ at $a=0$. With $U_\infty$ these steps form a cyclic group of order $\p-\bigl(\tfrac{N(v)}{\p}\bigr)$ containing every iterate; at most $2H^{2}+2H$ of its elements are window rotations. -/591theorem p01032 : (∀ (p : ℕ) [Fact (Nat.Prime p)], p % (4 : ℕ) = (1 : ℕ) → ∀ (N : ℤ), ↑N ≠ (0 : ZMod p) → IsCyclic ((FRC.Algebra.AxisAlg p ↑N)ˣ ⧸ FRC.Algebra.scalars p ↑N) ∧ ↑(Nat.card ((FRC.Algebra.AxisAlg p ↑N)ˣ ⧸ FRC.Algebra.scalars p ↑N)) = ↑p - legendreSym p N) ∧ ∀ {β : Type u_1} [DecidableEq β] (H : ℕ) (f : ℤ × ℤ → β), (∀ (x : ℤ × ℤ), f (-x) = f x) → (Finset.image f (FRC.Algebra.winPairs H)).card ≤ (2 : ℕ) * H * H + (2 : ℕ) * H :=592  And.intro @FRC.Algebra.axis_group (@FRC.Algebra.card_image_le_of_neg)593set_option linter.defProp false in594/-- 1:E8 (p01033) — The Lie-algebra layer, two axes and range: for pure quaternions $u,w$ with $1+N(u)$, $1+N(w)$ and $1-u\cdot w$ nonzero, $\rho_{1+u}\rho_{1+w}=\rho_{1+u\circ w}$ with $u\circ w=(u+w+u\times w)/(1-u\cdot w)$, the bracket being $[u,w]=2u\times w$; at $u\cdot w=1$ the product is the half-turn about $u+w+u\times w$. The entries of $q^{m}$, $q\in W_H^{4}$, are at most $(2H)^{m}$, and $q^{m}$ reads back from the shell iff $2\|q^{m}\|_\infty<\p$ (D2). -/595def p01033 := And.intro @FRC.Algebra.quat_pow_height (@FRC.Algebra.readback_iff)596/-- 1:Z1 (p01020) — No element of additive order two (Thm.~\ref{thm:no-south-pole}): $2s=0$ forces $s=0$; the antipode of the origin on the additive cycle is not a residue; it sits between $2\kap=(\p-1)/2$ and $2\kap+1=(\p+1)/2=2^{-1}$ (20-rh B8). -/597theorem p01020 : ∀ {F : Type u_1} [Field F], (2 : F) ≠ (0 : F) → ∀ (s : F), (2 : F) * s = (0 : F) → s = (0 : F) :=598  @FRC.Algebra.no_south_pole599-- end ledger predicates600601end FRC.Algebra602