FrameCore.lean — FrcCore

1import FrcCore.Shell2import FrcCore.Pigeonhole3import FrcCore.Series45/-!6# FrcCore.FrameCore — the frame `(τ; 0, 1, g)` and the Euclidean datum, from first principles (the frame theme)78The shell of capacity `κ` has modulus `p = 4κ + 1`; its frame carries the drive `g` (00:A6, 00:A12, 00:C1; labels as of 9 October 2026).9One decidable predicate states what the frame's generator is: `IsPrimitive g n` (`g^n = 1`, no positive10power below `n` is `1`). That `g` then *generates* — every nonzero residue is a power of `g`11(`Generates g n`, also decidable) — is proved by the pigeonhole (`FrcCore.Pigeonhole`): the `n` powers are12distinct nonzero residues and there are `n` of those. Primality of `p` is neither assumed nor used here; the13classical equivalence (a frame on `p = 4κ + 1` exists iff `p` is prime) is `FrcBridge/Foundation.lean`'s14`frame_iff_isPrime` (task LM23).1516From primitivity alone: inverses (`exists_inv`), no zero divisors (`mul_eq_zero`), the square roots17of one (`sq_eq_one`), the half-period `g^{2κ} = −1` (2:D1, 00:C1), the quarter-turn `i = −g^κ` with18`i² = −1` (1:B3, 2:D2), its orientation classes under `g ↦ g^u` (2:D5), the Euler identity19`(g^i)^{i·2κ} = (−1)^i` (2:D6, 00:C14), `2π ≡ −1`, and `2 ≠ 0` with `2s = 0 ⇒ s = 0` (1:Z1). No axioms.2021Split from `Frame.lean` by the ledger migration (task LM24), every name unchanged, so that a theme needing the frame22alone does not carry the frame's arithmetic; `Frame.lean` imports this file and keeps the rest.23-/2425namespace FRC26namespace Shell2728variable {p : Nat} [Pos p]2930/-- 00:A12 — the drive generator is primitive of order `n`: `g^n = 1` and `g^l ≠ 1` for `0 < l < n`. -/31def IsPrimitive (g : Shell p) (n : Nat) : Prop :=32  g ^ n = 1 ∧ ∀ l, l < n → 0 < l → g ^ l ≠ 13334instance (g : Shell p) (n : Nat) : Decidable (IsPrimitive g n) := by35  unfold IsPrimitive; exact inferInstance3637/-- 00:A12 — the drive generates the shell: every nonzero residue `v < p` is `g^m` for some `m < n`. -/38def Generates (g : Shell p) (n : Nat) : Prop :=39  ∀ v, v < p → 0 < v → ∃ m, m < n ∧ (g ^ m).val = v4041instance (g : Shell p) (n : Nat) : Decidable (Generates g n) := by42  unfold Generates43  have : ∀ v, Decidable (∃ m, m < n ∧ (g ^ m).val = v) := fun v => decExistsLT (fun m => (g ^ m).val = v) n44  exact inferInstance4546/-- 00:C1 — the frame `(τ; 0, 1, g)` on the shell of capacity `κ`: `p = 4κ + 1`, `κ` positive, and the47drive `g` a primitive generator of the `p − 1` nonzero residues. -/48structure Frame (p : Nat) [Pos p] (κ : Nat) (g : Shell p) : Prop where49  cap : p = 4 * κ + 150  cap_pos : 0 < κ51  prim : IsPrimitive g (p - 1)5253instance instDecForallLT (P : Nat → Prop) [DecidablePred P] (n : Nat) : Decidable (∀ m, m < n → P m) :=54  decForallLT P n5556/-- `∀ x : Shell p, P x`, decided through the representatives. -/57instance instDecForallShell {p : Nat} [Pos p] (P : Shell p → Prop) [DecidablePred P] :58    Decidable (∀ x, P x) :=59  match decForallLT (fun v => P (ofNat v)) p with60  | isTrue h => isTrue (fun x => ofNat_val x ▸ h x.val x.lt)61  | isFalse h => isFalse (fun hall => h (fun v _ => hall (ofNat v)))6263namespace Frame64variable {κ : Nat} {g : Shell p}6566/-- A residue has at most one inverse (moved here from `Orbit.lean` by task LM25, name unchanged). -/67theorem inv_unique {x x' y : Shell p} (h : x * y = 1) (h' : x' * y = 1) : x = x' := by68  calc x = x * (x' * y) := by rw [h', mul_one]69    _ = x' * (x * y) := mul_left_comm _ _ _70    _ = x' := by rw [h, mul_one]717273theorem n_eq (F : Frame p κ g) : p - 1 = 4 * κ := by rw [F.cap]; rfl7475theorem n_pos (F : Frame p κ g) : 0 < p - 1 := by76  rw [F.n_eq]; exact Nat.mul_pos (Nat.zero_lt_succ 3) F.cap_pos7778theorem one_lt_p (F : Frame p κ g) : 1 < p := by79  rw [F.cap]; exact Nat.succ_lt_succ (Nat.mul_pos (Nat.zero_lt_succ 3) F.cap_pos)8081theorem one_ne_zero (F : Frame p κ g) : (1 : Shell p) ≠ 0 := fun h => by82  have := val_injective h83  rw [val_one, val_zero, FRC.Nat.mod_eq_of_lt F.one_lt_p] at this84  exact Nat.noConfusion this8586theorem pow_n (F : Frame p κ g) : g ^ (p - 1) = 1 := F.prim.18788/-- 26:G2 — powers of the drive are periodic with period `p − 1`. -/89theorem pow_mod (F : Frame p κ g) (l : Nat) : g ^ l = g ^ (l % (p - 1)) := by90  match FRC.Nat.mod_spec (p - 1) F.n_pos l with91  | ⟨q, hq⟩ =>92    calc g ^ l = g ^ ((p - 1) * q + l % (p - 1)) := by rw [← hq]93      _ = (g ^ (p - 1)) ^ q * g ^ (l % (p - 1)) := by rw [pow_add, pow_mul]94      _ = g ^ (l % (p - 1)) := by rw [F.pow_n, one_pow, one_mul]9596theorem pow_eq_one_of_mod (F : Frame p κ g) {l : Nat} (h : l % (p - 1) = 0) : g ^ l = 1 := by97  rw [F.pow_mod, h, pow_zero]9899theorem mod_eq_zero_of_pow_eq_one (F : Frame p κ g) {l : Nat} (h : g ^ l = 1) : l % (p - 1) = 0 := by100  rw [F.pow_mod] at h101  exact match Nat.decEq (l % (p - 1)) 0 with102    | .isTrue h0 => h0103    | .isFalse h0 => absurd h (F.prim.2 _ (Nat.mod_lt l F.n_pos) (Nat.pos_of_ne_zero h0))104105/-- 26:B3 — the powers `g⁰, …, g^{n−1}` of the drive are distinct: `g^i = g^j` with `i, j < n` forces `i = j`. -/106theorem pow_inj (F : Frame p κ g) {i j : Nat} (hi : i < p - 1) (hj : j < p - 1) (h : g ^ i = g ^ j) :107    i = j := by108  have key : ∀ {i j : Nat}, i ≤ j → j < p - 1 → g ^ i = g ^ j → i = j := by109    intro i j hij hj h110    have hji : j - i < p - 1 := Nat.lt_of_le_of_lt (Nat.sub_le j i) hj111    have e : g ^ j = g ^ i * g ^ (j - i) := by rw [← pow_add, FRC.Nat.add_sub_of_le hij]112    have hinv : g ^ i * g ^ (p - 1 - i) = 1 := by113      rw [← pow_add, FRC.Nat.add_sub_of_le (Nat.le_of_lt (Nat.lt_of_le_of_lt hij hj)), F.pow_n]114    have h1 : g ^ (j - i) = 1 := by115      calc g ^ (j - i) = 1 * g ^ (j - i) := (one_mul _).symm116        _ = g ^ (p - 1 - i) * g ^ i * g ^ (j - i) := by rw [mul_comm (g ^ (p - 1 - i)), hinv]117        _ = g ^ (p - 1 - i) * g ^ j := by rw [mul_assoc, ← e]118        _ = g ^ (p - 1 - i) * g ^ i := by rw [h]119        _ = 1 := by rw [mul_comm, hinv]120    have h2 := F.mod_eq_zero_of_pow_eq_one h1121    rw [FRC.Nat.mod_eq_of_lt hji] at h2122    have : j = i + (j - i) := (FRC.Nat.add_sub_of_le hij).symm123    rw [h2, Nat.add_zero] at this124    exact this.symm125  exact match Nat.lt_or_ge i j with126    | .inl hlt => key (Nat.le_of_lt hlt) hj h127    | .inr hge => (key hge hi h.symm).symm128129theorem g_ne_zero (F : Frame p κ g) : g ≠ 0 := fun h0 => by130  have hn := F.pow_n131  have : p - 1 = (p - 2) + 1 := by132    have := F.one_lt_p133    match p, this with134    | k + 2, _ => rfl135  rw [this, pow_succ, h0, mul_zero] at hn136  exact F.one_ne_zero hn.symm137138/-- No power of the drive is zero: `g^m · g^{(n−1)m} = g^{nm} = 1`. -/139theorem pow_ne_zero (F : Frame p κ g) (m : Nat) : g ^ m ≠ 0 := fun h0 => by140  have hn := F.n_pos141  have e : m + (p - 1 - 1) * m = (p - 1) * m := by142    calc m + (p - 1 - 1) * m = 1 * m + (p - 1 - 1) * m := by rw [Nat.one_mul]143      _ = (1 + (p - 1 - 1)) * m := (FRC.Nat.add_mul _ _ _).symm144      _ = (p - 1) * m := by rw [FRC.Nat.add_sub_of_le hn]145  have : g ^ m * g ^ ((p - 1 - 1) * m) = 1 := by146    rw [← pow_add, e, pow_mul, F.pow_n, one_pow]147  rw [h0, zero_mul] at this148  exact F.one_ne_zero this.symm149150/-- The representatives of `g^0, …, g^{n−1}`, as a list (latest first). -/151def powList (g : Shell p) : Nat → List Nat152  | 0 => []153  | m + 1 => (g ^ m).val :: powList g m154155theorem powList_length (g : Shell p) (n : Nat) : (powList g n).length = n := by156  induction n with157  | zero => rfl158  | succ n ih => show (powList g n).length + 1 = n + 1; rw [ih]159160theorem mem_powList {g : Shell p} {v : Nat} : ∀ {n : Nat}, Pigeonhole.mem v (powList g n) → ∃ m, m < n ∧ (g ^ m).val = v161  | 0, h => absurd h id162  | n + 1, h => match h with163    | Or.inl e => ⟨n, Nat.lt_succ_self n, e.symm⟩164    | Or.inr h' => match mem_powList h' with165      | ⟨m, hm, e⟩ => ⟨m, Nat.lt_succ_of_lt hm, e⟩166167theorem powList_nodup (F : Frame p κ g) : ∀ {n : Nat}, n ≤ p - 1 → Pigeonhole.NoDup (powList g n)168  | 0, _ => trivial169  | n + 1, hn => ⟨fun h => match mem_powList h with170      | ⟨m, hm, e⟩ =>171        have : m = n := F.pow_inj (Nat.lt_trans hm hn) hn (ext e)172        Nat.lt_irrefl n (this ▸ hm),173    powList_nodup F (Nat.le_of_lt hn)⟩174175/-- 00:A12, 26:E10, 26:F10 — the drive generates: every nonzero residue is a power `g^m`, `m < p − 1` (the pigeonhole). -/176theorem generates (F : Frame p κ g) : Generates g (p - 1) := by177  intro v hv hv0178  have hb : ∀ e, Pigeonhole.mem e (powList g (p - 1)) → 1 ≤ e ∧ e ≤ p - 1 := fun e he =>179    match mem_powList he with180    | ⟨m, _, hm⟩ =>181      ⟨Nat.pos_of_ne_zero (fun h0 => F.pow_ne_zero m (ext (by rw [hm, h0]; rfl))),182       by rw [← hm]; exact Nat.le_of_lt_succ (Nat.lt_of_lt_of_le (g ^ m).lt (Nat.le_of_eq (FRC.Nat.sub_add_cancel Pos.pos).symm))⟩183  exact mem_powList (Pigeonhole.mem_of_nodup_of_length (p - 1) (powList g (p - 1)) (F.powList_nodup (Nat.le_refl _))184    hb (powList_length g (p - 1)) v hv0 (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hv (Nat.le_of_eq (FRC.Nat.sub_add_cancel Pos.pos).symm))))185186/-- Every nonzero residue is a power of the drive, on residues. -/187theorem eq_pow_of_ne_zero (F : Frame p κ g) {x : Shell p} (hx : x ≠ 0) :188    ∃ m, m < p - 1 ∧ g ^ m = x := by189  have hv : 0 < x.val := Nat.pos_of_ne_zero (fun h => hx (ext h))190  match F.generates x.val x.lt hv with191  | ⟨m, hm, e⟩ => exact ⟨m, hm, ext e⟩192193theorem exists_inv (F : Frame p κ g) {x : Shell p} (hx : x ≠ 0) : ∃ y, x * y = 1 := by194  match F.eq_pow_of_ne_zero hx with195  | ⟨m, hm, e⟩ =>196    refine ⟨g ^ (p - 1 - m), ?_⟩197    rw [← e, ← pow_add, FRC.Nat.add_sub_of_le (Nat.le_of_lt hm), F.pow_n]198199theorem mul_eq_zero (F : Frame p κ g) {a b : Shell p} (h : a * b = 0) : a = 0 ∨ b = 0 :=200  match Shell.instDecidableEq a 0 with201  | .isTrue ha => .inl ha202  | .isFalse ha => .inr (by203      match F.exists_inv ha with204      | ⟨y, hy⟩ =>205        calc b = 1 * b := (one_mul b).symm206          _ = y * a * b := by rw [mul_comm y a, hy]207          _ = y * (a * b) := mul_assoc _ _ _208          _ = 0 := by rw [h, mul_zero])209210theorem mul_ne_zero (F : Frame p κ g) {a b : Shell p} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=211  fun h => match F.mul_eq_zero h with212    | .inl e => ha e213    | .inr e => hb e214215/-- Cancellation: `a * b = a * c` with `a ≠ 0` gives `b = c`. -/216theorem mul_left_cancel (F : Frame p κ g) {a b c : Shell p} (ha : a ≠ 0) (h : a * b = a * c) : b = c := by217  have : a * (b + -c) = 0 := by rw [left_distrib, ← mul_neg, h, add_neg]218  match F.mul_eq_zero this with219  | .inl e => exact absurd e ha220  | .inr e =>221    calc b = b + 0 := (add_zero b).symm222      _ = b + (-c + c) := by rw [neg_add]223      _ = (b + -c) + c := (add_assoc _ _ _).symm224      _ = c := by rw [e, zero_add]225226/-- The square roots of one are `±1`. -/227theorem sq_eq_one (F : Frame p κ g) {x : Shell p} (h : x * x = 1) : x = 1 ∨ x = -1 := by228  have e : (x + -1) * (x + 1) = 0 := by229    rw [right_distrib, left_distrib, left_distrib, h, mul_one, neg_one_mul, neg_one_mul]230    rw [add_assoc, ← add_assoc x (-x), add_neg, zero_add, add_neg]231  match F.mul_eq_zero e with232  | .inl e1 => exact .inl (by233      calc x = x + 0 := (add_zero x).symm234        _ = x + (-1 + 1) := by rw [neg_add]235        _ = (x + -1) + 1 := (add_assoc _ _ _).symm236        _ = 1 := by rw [e1, zero_add])237  | .inr e2 => exact .inr (eq_neg_of_add_eq_zero e2)238239/-! ### The Euclidean datum (00:C1) -/240241/-- The half-period `π = 2κ`. -/242def halfPeriod (κ : Nat) : Nat := 2 * κ243244/-- The oriented quarter-turn `i = −g^κ` (00:C7). -/245def quarterTurn (g : Shell p) (κ : Nat) : Shell p := -(g ^ κ)246247theorem two_kappa_lt (F : Frame p κ g) : 2 * κ < p - 1 := by248  rw [F.n_eq]; exact FRC.Nat.mul_lt_mul_of_lt_of_pos (Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.zero_lt_succ 1))) F.cap_pos249250theorem two_kappa_pos (F : Frame p κ g) : 0 < 2 * κ := Nat.mul_pos (Nat.zero_lt_succ 1) F.cap_pos251252theorem four_kappa (F : Frame p κ g) : 2 * κ + 2 * κ = p - 1 := by253  rw [F.n_eq]254  show 2 * κ + 2 * κ = 2 * 2 * κ255  rw [FRC.Nat.mul_assoc, ← Nat.two_mul (2 * κ)]256257/-- 2:D1, 13:H2, 00:C1 — the half-period: `g^{2κ} = −1` for the drive of every frame (the half-turn tautology258behind `χ(−1) = e^{iπ}`). -/259theorem half_period (F : Frame p κ g) : g ^ (2 * κ) = -1 := by260  have hsq : g ^ (2 * κ) * g ^ (2 * κ) = 1 := by rw [← pow_add, F.four_kappa, F.pow_n]261  match F.sq_eq_one hsq with262  | .inr e => exact e263  | .inl e => exact absurd e (F.prim.2 (2 * κ) F.two_kappa_lt F.two_kappa_pos)264265/-- 1:B3, 2:D2, 13:J2 — the quarter-turn `i = −g^κ` squares to `−1` (the pinning relation `i² + 1 ≡ 0`). -/266theorem quarter_turn_sq (F : Frame p κ g) : quarterTurn g κ * quarterTurn g κ = -1 := by267  unfold quarterTurn268  rw [neg_mul_neg, ← pow_add, ← Nat.two_mul, F.half_period]269270/-- 2:D2 — `g^κ` has order four: `(g^κ)^2 = −1` and `(g^κ)^4 = 1`. -/271theorem quarter_turn_order (F : Frame p κ g) : (g ^ κ) ^ 2 = -1 ∧ (g ^ κ) ^ 4 = 1 := by272  have h2 : (g ^ κ) ^ 2 = -1 := by rw [← pow_mul, Nat.mul_comm, F.half_period]273  refine ⟨h2, ?_⟩274  show (g ^ κ) ^ (2 * 2) = 1275  rw [pow_mul, h2, neg_pow_two, one_pow]276277/-- 2:D5, 6:B3, 13:B2 — the orientation classes: for `g' = g^u`, the quarter-turn `−g'^κ` is `−g^κ` when278`u ≡ 1 (mod 4)` and `−(−g^κ)` when `u ≡ 3 (mod 4)`. -/279theorem orientation_class (F : Frame p κ g) (u : Nat) :280    (u % 4 = 1 → -((g ^ u) ^ κ) = -(g ^ κ)) ∧ (u % 4 = 3 → -((g ^ u) ^ κ) = -(-(g ^ κ))) := by281  have h4 : (g ^ κ) ^ 4 = 1 := (F.quarter_turn_order).2282  have h2 : (g ^ κ) ^ 2 = -1 := (F.quarter_turn_order).1283  have key : (g ^ u) ^ κ = (g ^ κ) ^ u := pow_mul_comm g u κ284  have hu : (g ^ κ) ^ u = (g ^ κ) ^ (u % 4) := by285    match FRC.Nat.mod_spec 4 (Nat.zero_lt_succ 3) u with286    | ⟨q, hq⟩ =>287      calc (g ^ κ) ^ u = (g ^ κ) ^ (4 * q + u % 4) := by rw [← hq]288        _ = ((g ^ κ) ^ 4) ^ q * (g ^ κ) ^ (u % 4) := by rw [pow_add, pow_mul]289        _ = (g ^ κ) ^ (u % 4) := by rw [h4, one_pow, one_mul]290  constructor291  · intro h1; rw [key, hu, h1, pow_one]292  · intro h3293    rw [key, hu, h3]294    show -((g ^ κ) ^ (2 + 1)) = -(-(g ^ κ))295    rw [pow_add, h2, pow_one, neg_one_mul]296297theorem sq_mod_two (i : Nat) : (i * i) % 2 = i % 2 := by298  rw [FRC.Nat.mul_mod i i 2 (Nat.zero_lt_succ 1)]299  have := Nat.mod_lt i (Nat.zero_lt_succ 1)300  match i % 2, this with301  | 0, _ => rfl302  | 1, _ => rfl303  | k + 2, hk => exact absurd hk (Nat.not_lt_of_le (Nat.le_add_left 2 k))304305/-- 2:D6, 6:B2, 00:C14 — the Euler identity on the shell: with `e = g^i` and `π = 2κ`,306`(g^i)^{i·2κ} = (−1)^i` for every natural reading `i` of the quarter-turn — `−1` exactly when `i` is odd. -/307theorem euler_identity (F : Frame p κ g) (i : Nat) :308    (g ^ i) ^ (i * (2 * κ)) = if i % 2 = 0 then 1 else -1 := by309  have e1 : (g ^ i) ^ (i * (2 * κ)) = (g ^ (2 * κ)) ^ (i * i) := by310    rw [← pow_mul, ← pow_mul]311    show g ^ (i * (i * (2 * κ))) = g ^ (2 * κ * (i * i))312    rw [← FRC.Nat.mul_assoc, Nat.mul_comm (i * i)]313  rw [e1, F.half_period, neg_one_pow, sq_mod_two]314315/-- 00:C1, 13:J2, 13:I4 — the web closes: `2π ≡ −1` on every shell (`4κ = p − 1`): the height-two pinning316`2π_A + 1 ≡ 0`, which holds in every fibre of a composite lift. -/317theorem two_pi (F : Frame p κ g) : (ofNat (2 * halfPeriod κ) : Shell p) = -1 := by318  apply ext319  rw [val_ofNat, val_neg, val_one, FRC.Nat.mod_eq_of_lt F.one_lt_p]320  unfold halfPeriod321  rw [← FRC.Nat.mul_assoc]322  show (4 * κ) % p = (p - 1) % p323  rw [F.n_eq]324325/-! ### Two is invertible on every shell -/326327theorem two_lt_p (F : Frame p κ g) : 2 < p := by328  rw [F.cap]329  have h : 4 * 1 ≤ 4 * κ := Nat.mul_le_mul_left 4 F.cap_pos330  exact Nat.lt_of_lt_of_le (by decide : 2 < 4 * 1 + 1) (Nat.succ_le_succ h)331332theorem two_ne_zero (F : Frame p κ g) : (2 : Shell p) ≠ 0 := fun h => by333  have := val_injective h334  rw [val_lit, val_zero, FRC.Nat.mod_eq_of_lt F.two_lt_p] at this335  exact Nat.noConfusion this336337theorem two_eq_one_add_one : (2 : Shell p) = 1 + 1 :=338  ext (by rw [val_add, val_one, val_lit, FRC.Nat.mod_add_mod _ _ _ hp, FRC.Nat.add_mod_mod _ _ _ hp])339340theorem two_mul' (x : Shell p) : (2 : Shell p) * x = x + x := by341  rw [two_eq_one_add_one, right_distrib, one_mul]342343theorem eq_zero_of_eq_neg (F : Frame p κ g) {x : Shell p} (h : x = -x) : x = 0 := by344  have h2 : (2 : Shell p) * x = 0 := by345    rw [two_mul']346    calc x + x = x + -x := by rw [← h]347      _ = 0 := add_neg x348  match F.mul_eq_zero h2 with349  | .inl e => exact absurd e F.two_ne_zero350  | .inr e => exact e351352/-- 1:Z1 (Theorem 3) — `2s = 0 ⇒ s = 0`: the additive cycle has no element of order two; the antipode of353the origin is not a residue. -/354theorem no_south_pole (F : Frame p κ g) (s : Shell p) (h : (2 : Shell p) * s = 0) : s = 0 :=355  match F.mul_eq_zero h with356  | .inl e => absurd e F.two_ne_zero357  | .inr e => e358359end Frame360end Shell361end FRC362