The core module lean/FrcCore/Orbit.lean — the substrate from first principles, no Mathlib, no axioms (the modules in order: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Projective, Theme/Fourier, Theme/Fractional, Theme/Lifts, Theme/Dichotomy, Theme/Rotations, Theme/Heisenberg, Theme/Spectra, Theme/Exclusivity, Theme/Quadratic, Theme/Extension, Theme/Tally, Theme/Numbers, Theme/Logic, Theme/SecondOrder, Theme/Formation, Theme/Field, Theme/Foundation, Theme/Drive, Theme/Carrier, Theme/Subject, Theme/Pair, Theme/Hopf, Theme/Symbol, Theme/Gravity, Theme/Quantum, Theme/Unitary, Theme/Interactions, Theme/Horizon, Theme/Shift, Theme/Lattice, Theme/Drift, Theme/Observation, Theme/Interference, Theme/Composite, Theme/Ladder, Meridian, Fourier, Algebra, Epi, Dimensions, Poly, Quaternion, Causality, Representation, Reductio, Godel, Finitism, Geometry, Complex, Instances, Rh, Entropy, Dirac, Gravity, S13, Qm, Pnp, Keys/Frame, Keys/Extension, Keys/Projective, Keys/Fourier, Keys/Numbers, Keys/Logic, Keys/Foundation, Keys/Carrier, Keys/Subject, Keys/Gravity, Keys/Quantum, Keys/Interactions, Keys/Horizon): 32 theorems (2 definitions): 32 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Frame2import FrcCore.Parity34/-!5# FrcCore.Orbit — the generators form one orbit (2:B3; 1-algebra's torsor of primitive roots)67`Coprime u n` is taken in its invertible form — some `a < n` has `a·u ≡ 1 (mod n)` — which is decidable by8search and, for `n ≥ 1`, the same as `gcd(u, n) = 1` (Bezout); it is what every proof uses. Theorem:9`h` is primitive of order `n = p − 1` exactly when `h = g^u` with `u < n` coprime to `n`. No axioms.1011Since the ledger migration (task LM17) it also holds the Klein orbits off the fourth roots of unity (from 1-algebra),12the octant character of `2` (from 14-entropy: `2` is a square exactly on the frames of even capacity) and the parity of13the drive (from 8-dirac: `g^m` is a square exactly when `m` is even); the parity is `Parity.lean` since task LM24.14-/1516namespace FRC17namespace Shell1819/-- `u` is invertible mod `n`: some `a < n` has `a·u % n = 1`. -/20
def Coprime (u n : Nat) : Prop := ∃ a, a < n ∧ (a * u) % n = 12122instance (u n : Nat) : Decidable (Coprime u n) := decExistsLT (fun a => (a * u) % n = 1) n2324namespace Frame25variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}2627/-- A power of the drive with an invertible exponent is again primitive. -/28
theorem primitive_pow_of_coprime (F : Frame p κ g) {u : Nat} (hu : Coprime u (p - 1)) :29 IsPrimitive (g ^ u) (p - 1) := by30 have hn := F.n_pos31 match hu with32 | ⟨a, _, ha⟩ =>33 refine ⟨by rw [pow_mul_comm, F.pow_n, one_pow], ?_⟩34 intro l hl hl0 hpow35 -- (g^u)^l = 1 gives (u·l) % n = 0; with a·u = n·q + 1, g^l = g^{l·a·u} = ((g^u)^l)^a = 136 have h1 : (u * l) % (p - 1) = 0 := F.mod_eq_zero_of_pow_eq_one (by rw [pow_mul]; exact hpow)37 match FRC.Nat.mod_spec (p - 1) hn (a * u) with38 | ⟨q, hq⟩ =>39 rw [ha] at hq40 have e : l * (a * u) = (p - 1) * (q * l) + l := by41 rw [hq, Nat.left_distrib, Nat.mul_one, FRC.Nat.mul_left_comm, Nat.mul_comm l q]42 have h2 : g ^ (l * (a * u)) = 1 := by43 rw [show l * (a * u) = (u * l) * a by rw [Nat.mul_comm u l, FRC.Nat.mul_assoc, Nat.mul_comm a u]]44 rw [pow_mul, F.pow_eq_one_of_mod h1, one_pow]45 rw [e, pow_add, pow_mul, F.pow_n, one_pow, one_mul] at h246 have := F.mod_eq_zero_of_pow_eq_one h247 rw [FRC.Nat.mod_eq_of_lt hl] at this48 exact Nat.lt_irrefl 0 (this ▸ hl0)4950/-- The frame of another primitive drive on the same shell. -/51theorem of_primitive (F : Frame p κ g) {h : Shell p} (hh : IsPrimitive h (p - 1)) : Frame p κ h :=52 ⟨F.cap, F.cap_pos, hh⟩5354/-- 2:B3 (Props. 2.7, 4.5), 1-algebra's torsor — the primitive generators form one orbit: `h` is primitive55of order `p − 1` exactly when `h = g^u` for some `u < p − 1` coprime to `p − 1`. -/56theorem generator_orbit (F : Frame p κ g) (h : Shell p) :57 IsPrimitive h (p - 1) ↔ ∃ u, u < p - 1 ∧ Coprime u (p - 1) ∧ h = g ^ u := by58 have hn := F.n_pos59 constructor60 · intro hh61 have Fh : Frame p κ h := F.of_primitive hh62 have hh0 : h ≠ 0 := Fh.g_ne_zero63 match F.eq_pow_of_ne_zero hh0 with64 | ⟨u, hu, e⟩ =>65 refine ⟨u, hu, ?_, e.symm⟩66 -- g is a power of h: g = h^v; then g^{u v} = g, so u·v ≡ 1 (mod n)67 match Fh.eq_pow_of_ne_zero F.g_ne_zero with68 | ⟨v, hv, ev⟩ =>69 refine ⟨v, hv, ?_⟩70 have e1 : g ^ (v * u) = g ^ 1 := by71 rw [pow_one, Nat.mul_comm v u, pow_mul, e, ev]72 have h1n : 1 < p - 1 := by73 rw [F.n_eq]; exact Nat.lt_of_lt_of_le (by decide : 1 < 4 * 1) (Nat.mul_le_mul_left 4 F.cap_pos)74 have := F.pow_inj (Nat.mod_lt _ hn) h1n (by rw [← F.pow_mod, e1])75 exact this76 · intro ⟨u, _, hu, e⟩77 rw [e]; exact F.primitive_pow_of_coprime hu7879/-- 1:E3, the finitary core (Fermat): every residue satisfies `x^p = x` — the polynomial `X^p − X` vanishes on80the whole shell, which is what the root test of 1:E3 rests on. -/81theorem fermat (F : Frame p κ g) (x : Shell p) : x ^ p = x := by82 have hp1 : x ^ p = x ^ (p - 1) * x :=83 congrArg (fun k => x ^ k) (FRC.Nat.sub_add_cancel Pos.pos).symm84 rw [hp1]85 exact match Shell.instDecidableEq x 0 with86 | isTrue e => by rw [e, mul_zero]87 | isFalse e => by88 match F.eq_pow_of_ne_zero e with89 | ⟨m, _, em⟩ => rw [← em, pow_mul_comm, F.pow_n, one_pow, one_mul]9091/-! ## The Klein orbits off the fourth roots of unity (moved from 1-algebra, task LM17) -/9293/-- 1:B2 (Theorem 1 of 1-algebra), 2:D7 — off the fourth roots of unity, `x`, `−x`, `x⁻¹`, `−x⁻¹` are four94distinct residues (`y` stands for the inverse: `x·y = 1`). -/95theorem klein_orbit_four (F : Frame p κ g) {x y : Shell p} (hxy : x * y = 1) (h4 : x ^ 4 ≠ 1) :96 x ≠ -x ∧ x ≠ y ∧ x ≠ -y ∧ -x ≠ y ∧ -x ≠ -y ∧ y ≠ -y := by97 have hx0 : x ≠ 0 := fun h => F.one_ne_zero (by rw [← hxy, h, zero_mul])98 have hy0 : y ≠ 0 := fun h => F.one_ne_zero (by rw [← hxy, h, mul_zero])99 have h4' : x ^ 4 = (x * x) * (x * x) := by100 rw [show (4 : Nat) = 2 * 2 from rfl, pow_mul, pow_two, pow_two]101 have hsq : x * x ≠ 1 := fun h => h4 (by rw [h4', h, one_mul])102 have hsqn : x * x ≠ -1 := fun h => h4 (by rw [h4', h, neg_mul_neg, one_mul])103 have hxy' : x = y → False := fun e => hsq (by rw [← hxy, e])104 have hxny : x = -y → False := fun e => hsqn (by105 have : x * x = x * -y := by rw [← e]106 rw [this, ← mul_neg, hxy])107 refine ⟨fun h => hx0 (F.eq_zero_of_eq_neg h), hxy', hxny, ?_, ?_, ?_⟩108 · intro h; exact hxny (by rw [← neg_neg x, h])109 · intro h; exact hxy' (by rw [← neg_neg x, h, neg_neg])110 · intro h; exact hy0 (F.eq_zero_of_eq_neg h)111112/-! ### 1:B2, the count: the Klein orbits off `Q₄` are exactly `κ − 1`, represented by `g^r`, `1 ≤ r < κ` -/113114/-- `y` lies in the Klein orbit of `x`: `y ∈ {x, −x, x⁻¹, −x⁻¹}` (the inverse written as `x·y = 1`). -/115def InOrbit (x y : Shell p) : Prop := y = x ∨ y = -x ∨ x * y = 1 ∨ x * -y = 1116117theorem two_mul_eq (κ : Nat) : 2 * κ = κ + κ := Nat.two_mul κ118theorem three_mul_eq (κ : Nat) : 3 * κ = κ + κ + κ := by rw [Nat.succ_mul, Nat.two_mul]119theorem four_mul_eq (κ : Nat) : 4 * κ = κ + κ + κ + κ := by rw [Nat.succ_mul, three_mul_eq]120121/-- The exponent `m` of `x = g^m` reduced to its orbit representative in `[1, κ)`. -/122theorem orbit_rep_of_exp (F : Frame p κ g) {m : Nat} (hm : m < p - 1) (h0 : m ≠ 0) (h1 : m ≠ κ)123 (h2 : m ≠ 2 * κ) (h3 : m ≠ 3 * κ) :124 ∃ r, 1 ≤ r ∧ r < κ ∧ InOrbit (g ^ r) (g ^ m) := by125 have hn := F.n_eq126 have hπ := F.half_period127 rw [hn, four_mul_eq] at hm128 rw [two_mul_eq] at h2 hπ129 rw [three_mul_eq] at h3130 match Nat.lt_or_ge m κ with131 | Or.inl hlt => exact ⟨m, Nat.pos_of_ne_zero h0, hlt, Or.inl rfl⟩132 | Or.inr hge1 => match Nat.lt_or_ge m (κ + κ) with133 | Or.inl hlt =>134 -- κ < m < 2κ: r = 2κ − m, and g^m · (−g^r) = −g^{2κ} = 1135 have hgt : κ < m := Nat.lt_of_le_of_ne hge1 (fun e => h1 e.symm)136 refine ⟨κ + κ - m, ?_, ?_, Or.inr (Or.inr (Or.inr ?_))⟩137 · refine Nat.lt_of_add_lt_add_right (n := m) ?_138 rw [Nat.zero_add, FRC.Nat.sub_add_cancel (Nat.le_of_lt hlt)]; exact hlt139 · refine Nat.lt_of_add_lt_add_right (n := m) ?_140 rw [FRC.Nat.sub_add_cancel (Nat.le_of_lt hlt)]; exact Nat.add_lt_add_left hgt κ141 · rw [← mul_neg, ← pow_add, FRC.Nat.sub_add_cancel (Nat.le_of_lt hlt), hπ, neg_neg]142 | Or.inr hge2 => match Nat.lt_or_ge m (κ + κ + κ) with143 | Or.inl hlt =>144 -- 2κ < m < 3κ: r = m − 2κ, and g^m = −g^r145 have hgt : κ + κ < m := Nat.lt_of_le_of_ne hge2 (fun e => h2 e.symm)146 refine ⟨m - (κ + κ), ?_, ?_, Or.inr (Or.inl ?_)⟩147 · refine Nat.lt_of_add_lt_add_right (n := κ + κ) ?_148 rw [Nat.zero_add, FRC.Nat.sub_add_cancel hge2]; exact hgt149 · refine Nat.lt_of_add_lt_add_right (n := κ + κ) ?_150 rw [FRC.Nat.sub_add_cancel hge2, Nat.add_comm κ (κ + κ)]; exact hlt151 · have : m = κ + κ + (m - (κ + κ)) := (FRC.Nat.add_sub_of_le hge2).symm152 rw [this, pow_add, hπ, neg_one_mul, FRC.Nat.add_sub_cancel_left]153 | Or.inr hge3 =>154 -- 3κ < m < 4κ: r = 4κ − m, and g^m · g^r = g^{4κ} = 1155 have hgt : κ + κ + κ < m := Nat.lt_of_le_of_ne hge3 (fun e => h3 e.symm)156 refine ⟨κ + κ + κ + κ - m, ?_, ?_, Or.inr (Or.inr (Or.inl ?_))⟩157 · refine Nat.lt_of_add_lt_add_right (n := m) ?_158 rw [Nat.zero_add, FRC.Nat.sub_add_cancel (Nat.le_of_lt hm)]; exact hm159 · refine Nat.lt_of_add_lt_add_right (n := m) ?_160 rw [FRC.Nat.sub_add_cancel (Nat.le_of_lt hm), Nat.add_comm κ m]161 exact Nat.add_lt_add_right hgt κ162 · rw [← pow_add, FRC.Nat.sub_add_cancel (Nat.le_of_lt hm), ← four_mul_eq, ← hn, F.pow_n]163164/-- Off the fourth roots of unity, `x = g^m` has `m ∉ {0, κ, 2κ, 3κ}`. -/165theorem exp_not_fourth (F : Frame p κ g) {m : Nat} (h4 : (g ^ m) ^ 4 ≠ 1) :166 m ≠ 0 ∧ m ≠ κ ∧ m ≠ 2 * κ ∧ m ≠ 3 * κ := by167 have hi := (F.quarter_turn_order).2168 refine ⟨fun e => h4 (by rw [e, pow_zero, one_pow]), fun e => h4 (by rw [e, hi]), fun e => h4 ?_, fun e => h4 ?_⟩169 · rw [e, Nat.mul_comm 2 κ, pow_mul, ← pow_mul, show (2 : Nat) * 4 = 4 * 2 from rfl, pow_mul, hi, one_pow]170 · rw [e, Nat.mul_comm 3 κ, pow_mul, ← pow_mul, show (3 : Nat) * 4 = 4 * 3 from rfl, pow_mul, hi, one_pow]171172/-- 1:B2 (Theorem 1, the count, existence), 2:D7 — every residue off `Q₄` lies in the Klein orbit of some `g^r`173with `1 ≤ r < κ`. -/174theorem orbit_rep (F : Frame p κ g) {x : Shell p} (hx : x ≠ 0) (h4 : x ^ 4 ≠ 1) :175 ∃ r, 1 ≤ r ∧ r < κ ∧ InOrbit (g ^ r) x := by176 match F.eq_pow_of_ne_zero hx with177 | ⟨m, hm, e⟩ =>178 rw [← e] at h4 ⊢179 match F.exp_not_fourth h4 with180 | ⟨h0, h1, h2, h3⟩ => exact F.orbit_rep_of_exp hm h0 h1 h2 h3181182theorem neg_mul_of_mul_neg {a b : Shell p} (e : a * -b = 1) : -a * b = 1 := by183 rw [← neg_mul, mul_neg]; exact e184185/-- The orbit relation is symmetric. -/186theorem inOrbit_symm {a b : Shell p} (h : InOrbit a b) : InOrbit b a :=187 match h with188 | Or.inl e => Or.inl e.symm189 | Or.inr (Or.inl e) => Or.inr (Or.inl (by rw [e, neg_neg]))190 | Or.inr (Or.inr (Or.inl e)) => Or.inr (Or.inr (Or.inl (by rw [mul_comm]; exact e)))191 | Or.inr (Or.inr (Or.inr e)) => Or.inr (Or.inr (Or.inr (by rw [← mul_neg, mul_comm, mul_neg]; exact e)))192193theorem neg_eq_neg {a b : Shell p} (h : -a = -b) : a = b := by rw [← neg_neg a, h, neg_neg]194195/-- The orbit relation is transitive. -/196theorem inOrbit_trans {a b c : Shell p} (h1 : InOrbit a b) (h2 : InOrbit b c) : InOrbit a c := by197 have hab : b = a ∨ b = -a ∨ a * b = 1 ∨ a * -b = 1 := h1198 have hbc : c = b ∨ c = -b ∨ b * c = 1 ∨ b * -c = 1 := h2199 unfold InOrbit200 match hab, hbc with201 | Or.inl e, h => exact e ▸ h202 | Or.inr (Or.inl e), Or.inl e' => exact Or.inr (Or.inl (e' ▸ e))203 | Or.inr (Or.inl e), Or.inr (Or.inl e') => exact Or.inl (by rw [e', e, neg_neg])204 | Or.inr (Or.inl e), Or.inr (Or.inr (Or.inl e')) => exact Or.inr (Or.inr (Or.inr (by rw [← mul_neg, neg_mul, ← e]; exact e')))205 | Or.inr (Or.inl e), Or.inr (Or.inr (Or.inr e')) => exact Or.inr (Or.inr (Or.inl (by rw [← neg_mul_neg, ← e]; exact e')))206 | Or.inr (Or.inr (Or.inl e)), Or.inl e' => exact Or.inr (Or.inr (Or.inl (e' ▸ e)))207 | Or.inr (Or.inr (Or.inl e)), Or.inr (Or.inl e') => exact Or.inr (Or.inr (Or.inr (by rw [e', neg_neg]; exact e)))208 | Or.inr (Or.inr (Or.inl e)), Or.inr (Or.inr (Or.inl e')) =>209 exact Or.inl (inv_unique (x := c) (x' := a) (y := b) (by rw [mul_comm]; exact e') e)210 | Or.inr (Or.inr (Or.inl e)), Or.inr (Or.inr (Or.inr e')) =>211 exact Or.inr (Or.inl (by212 have := inv_unique (x := -c) (x' := a) (y := b) (by rw [mul_comm]; exact e') e213 rw [← this, neg_neg]))214 | Or.inr (Or.inr (Or.inr e)), Or.inl e' => exact Or.inr (Or.inr (Or.inr (e' ▸ e)))215 | Or.inr (Or.inr (Or.inr e)), Or.inr (Or.inl e') => exact Or.inr (Or.inr (Or.inl (by rw [e']; exact e)))216 | Or.inr (Or.inr (Or.inr e)), Or.inr (Or.inr (Or.inl e')) =>217 exact Or.inr (Or.inl (inv_unique (x := -a) (x' := c) (y := b) (neg_mul_of_mul_neg e) (by rw [mul_comm]; exact e')).symm)218 | Or.inr (Or.inr (Or.inr e)), Or.inr (Or.inr (Or.inr e')) =>219 exact Or.inl (neg_eq_neg (inv_unique (x := -a) (x' := -c) (y := b) (neg_mul_of_mul_neg e) (by rw [mul_comm]; exact e'))).symm220221/-- The exponents of the orbit of `g^r`: `g^s ∈ orbit(g^r)`, `s < n`, forces `s ∈ {r, r + 2κ, 4κ − r, 2κ − r}`222(for `1 ≤ r < κ`). -/223theorem orbit_exponent (F : Frame p κ g) {r s : Nat} (hr1 : 1 ≤ r) (hrκ : r < κ) (hs : s < p - 1)224 (h : InOrbit (g ^ r) (g ^ s)) : s = r ∨ s = r + (κ + κ) ∨ s = κ + κ + κ + κ - r ∨ s = κ + κ - r := by225 have hn := F.n_eq226 have hπ := F.half_period227 rw [two_mul_eq] at hπ228 rw [hn, four_mul_eq] at hs229 have hr2 : r < κ + κ := Nat.lt_of_lt_of_le hrκ (Nat.le_add_right κ κ)230 have hr4 : r < κ + κ + κ + κ := Nat.lt_of_lt_of_le hr2 (Nat.le_trans (Nat.le_add_right _ κ) (Nat.le_add_right _ κ))231 have hpow_inj : ∀ {i j : Nat}, i < κ + κ + κ + κ → j < κ + κ + κ + κ → g ^ i = g ^ j → i = j :=232 fun hi hj e => F.pow_inj (by rw [hn, four_mul_eq]; exact hi) (by rw [hn, four_mul_eq]; exact hj) e233 have hpn : g ^ (κ + κ + κ + κ) = 1 := by rw [← four_mul_eq, ← hn]; exact F.pow_n234 match h with235 | Or.inl e => exact Or.inl (hpow_inj hs hr4 e)236 | Or.inr (Or.inl e) =>237 have e' : g ^ s = g ^ (r + (κ + κ)) := by rw [e, pow_add, hπ, mul_comm, neg_one_mul]238 have hlt : r + (κ + κ) < κ + κ + κ + κ := by239 rw [show κ + κ + κ + κ = (κ + κ) + (κ + κ) by rw [Nat.add_assoc]]240 exact Nat.add_lt_add_right hr2 _241 exact Or.inr (Or.inl (hpow_inj hs hlt e'))242 | Or.inr (Or.inr (Or.inl e)) =>243 have hlt : κ + κ + κ + κ - r < κ + κ + κ + κ := Nat.sub_lt (Nat.lt_of_lt_of_le (Nat.zero_lt_succ 0) (Nat.le_trans hr1 (Nat.le_of_lt hr4))) hr1244 have e2 : g ^ r * g ^ (κ + κ + κ + κ - r) = 1 := by rw [← pow_add, FRC.Nat.add_sub_of_le (Nat.le_of_lt hr4), hpn]245 have e' : g ^ s = g ^ (κ + κ + κ + κ - r) := F.mul_left_cancel (F.pow_ne_zero r) (e.trans e2.symm)246 exact Or.inr (Or.inr (Or.inl (hpow_inj hs hlt e')))247 | Or.inr (Or.inr (Or.inr e)) =>248 have hlt : κ + κ - r < κ + κ + κ + κ := Nat.lt_of_le_of_lt (Nat.sub_le _ _)249 (Nat.lt_of_lt_of_le (Nat.lt_add_of_pos_right F.cap_pos) (Nat.le_add_right _ κ))250 have e2 : g ^ r * -(g ^ (κ + κ - r)) = 1 := by251 rw [← mul_neg, ← pow_add, FRC.Nat.add_sub_of_le (Nat.le_of_lt hr2), hπ, neg_neg]252 have e' : -(g ^ s) = -(g ^ (κ + κ - r)) := F.mul_left_cancel (F.pow_ne_zero r) (e.trans e2.symm)253 exact Or.inr (Or.inr (Or.inr (hpow_inj hs hlt (neg_eq_neg e'))))254255/-- 1:B2 (Theorem 1, the count, uniqueness), 2:D7 — two representatives `g^r`, `g^{r'}` with `1 ≤ r, r' < κ` whose256orbits meet are the same: the Klein orbits off `Q₄` are exactly `κ − 1`, one for each `r ∈ [1, κ)`. -/257theorem orbit_rep_unique (F : Frame p κ g) {r r' : Nat} (hr1 : 1 ≤ r) (hrκ : r < κ) (_hr1' : 1 ≤ r')258 (hrκ' : r' < κ) {x : Shell p} (hx : InOrbit (g ^ r) x) (hx' : InOrbit (g ^ r') x) : r = r' := by259 have hn := F.n_eq260 have hr' : r' < p - 1 := by261 rw [hn, four_mul_eq]262 exact Nat.lt_of_lt_of_le hrκ' (Nat.le_trans (Nat.le_add_right κ κ) (Nat.le_trans (Nat.le_add_right _ κ) (Nat.le_add_right _ κ)))263 have h := inOrbit_trans hx (inOrbit_symm hx')264 match F.orbit_exponent hr1 hrκ hr' h with265 | Or.inl e => exact e.symm266 | Or.inr (Or.inl e) =>267 exact absurd hrκ' (Nat.not_lt_of_le (by rw [e]; exact Nat.le_trans (Nat.le_add_right κ κ) (Nat.le_add_left _ r)))268 | Or.inr (Or.inr (Or.inl e)) =>269 -- 4κ − r > κ since r < κ270 have : κ ≤ κ + κ + κ + κ - r := by271 apply FRC.Nat.le_sub_of_add_le272 rw [Nat.add_assoc, Nat.add_assoc]273 exact Nat.add_le_add_left (Nat.le_trans (Nat.le_of_lt hrκ) (Nat.le_add_right κ _)) κ274 exact absurd hrκ' (Nat.not_lt_of_le (e ▸ this))275 | Or.inr (Or.inr (Or.inr e)) =>276 -- 2κ − r > κ since r < κ277 have : κ ≤ κ + κ - r := by278 apply FRC.Nat.le_sub_of_add_le279 exact Nat.add_le_add_left (Nat.le_of_lt hrκ) κ280 exact absurd hrκ' (Nat.not_lt_of_le (e ▸ this))281282/-! ## The octant character of `2` (moved from 14-entropy, task LM17) -/283284/-! ## The octant character on every framed shell of even capacity (14:C6, X4) -/285286287/-- Literals multiply as their values: `a · b = ab` on every shell. -/288theorem lit_mul (a b : Nat) : (OfNat.ofNat a : Shell p) * OfNat.ofNat b = (OfNat.ofNat (a * b) : Shell p) :=289 Shell.ext (by290 show (a % p * (b % p)) % p = (a * b) % p291 exact (FRC.Nat.mul_mod a b p Pos.pos).symm)292293/-- `a + 1 + (1 − a) = 2` on every shell. -/294theorem add_one_add_one_neg (a : Shell p) : a + 1 + (1 + -a) = 2 := by295 rw [Shell.add_assoc, ← Shell.add_assoc 1 1 (-a), Shell.add_comm (1 + 1) (-a),296 ← Shell.add_assoc a (-a) (1 + 1), Shell.add_neg a, Shell.zero_add]297 exact Frame.two_eq_one_add_one.symm298299/-- On a frame of capacity `κ = 2m`: `g^{4m} = −1` (the half-period) and `g^{8m} = 1`. -/300theorem even_capacity_powers (F : Frame p κ g) (m : Nat) (hm : κ = 2 * m) :301 g ^ (4 * m) = -1 ∧ g ^ (8 * m) = 1 := by302 have h4 : 4 * m = 2 * κ := by rw [hm, ← FRC.Nat.mul_assoc]303 have h8 : 8 * m = p - 1 := by rw [F.n_eq, hm, ← FRC.Nat.mul_assoc]304 exact ⟨by rw [h4]; exact F.half_period, by rw [h8]; exact F.pow_n⟩305306/-- 14:C6 — the octant character: on every frame `(τ; 0, 1, g)` of even capacity `κ = 2m`, `ζ = g^m` has307`ζ⁴ = −1` and `ζ⁸ = 1` — the sector `C₈ ⊂ C_{4κ}` is realised and `ζ` is its residue `ζ₈`. -/308theorem octant_residue (F : Frame p κ g) (m : Nat) (hm : κ = 2 * m) :309 (g ^ m) ^ 4 = -1 ∧ (g ^ m) ^ 8 = 1 := by310 obtain ⟨h4, h8⟩ := even_capacity_powers F m hm311 constructor312 · rw [← Shell.pow_mul, Nat.mul_comm m 4]; exact h4313 · rw [← Shell.pow_mul, Nat.mul_comm m 8]; exact h8314315/-- 14:C6, 14:X4 — the Tsirelson square: with `ζ = g^m` and `ζ' = g^{7m}` its inverse (`ζζ' = 1`),316`(ζ + ζ')² = 2` and `(2(ζ + ζ'))² = 8` on every frame of capacity `κ = 2m`; hence `2` is a square on every317such shell — the direction "octant ⇒ c-square" of X4's second face (the converse is318`even_capacity_of_two_square` below; the equivalence `two_is_square_iff`). -/319theorem tsirelson_square (F : Frame p κ g) (m : Nat) (hm : κ = 2 * m) :320 g ^ m * g ^ (7 * m) = 1 ∧ (g ^ m + g ^ (7 * m)) ^ 2 = 2 ∧321 (2 * (g ^ m + g ^ (7 * m))) ^ 2 = 8 := by322 obtain ⟨h4, h8⟩ := even_capacity_powers F m hm323 have hz : g ^ m * g ^ (7 * m) = 1 := by324 rw [← Shell.pow_add, show m + 7 * m = 8 * m by325 rw [Nat.mul_comm 8 m, Nat.mul_succ, Nat.mul_comm m 7, Nat.add_comm]]326 exact h8327 -- `ζ'² = −ζ²`: `g^{14m} = g^{8m} g^{4m} g^{2m} = (−1) g^{2m}`328 have h14 : 7 * m + 7 * m = 8 * m + (4 * m + (m + m)) := by329 calc 7 * m + 7 * m = (7 + 7) * m := (FRC.Nat.add_mul 7 7 m).symm330 _ = (8 + (4 + (1 + 1))) * m := rfl331 _ = 8 * m + (4 * m + (1 * m + 1 * m)) := by332 rw [FRC.Nat.add_mul, FRC.Nat.add_mul, FRC.Nat.add_mul]333 _ = 8 * m + (4 * m + (m + m)) := by rw [Nat.one_mul]334 have hz' : g ^ (7 * m) * g ^ (7 * m) = -(g ^ m * g ^ m) := by335 rw [← Shell.pow_add, h14, Shell.pow_add, Shell.pow_add, Shell.pow_add, h8, h4, Shell.one_mul,336 Shell.neg_one_mul]337 -- `(ζ + ζ')² = ζ² + ζζ' + ζ'ζ + ζ'² = ζ² + 1 + (1 − ζ²) = 2`338 have hsq : (g ^ m + g ^ (7 * m)) ^ 2 = 2 := by339 rw [Shell.pow_two, Shell.left_distrib, Shell.right_distrib, Shell.right_distrib, hz,340 Shell.mul_comm (g ^ (7 * m)) (g ^ m), hz, hz']341 exact add_one_add_one_neg _342 refine ⟨hz, hsq, ?_⟩343 rw [Shell.mul_pow, hsq, Shell.pow_two, lit_mul 2 2, lit_mul 4 2]344345/-- 14:X4 — the direction "even capacity ⇒ `2` a square" at tier 0: on every frame of even capacity `2` is a346square, `(ζ + ζ⁻¹)² = 2`; the converse is `even_capacity_of_two_square`, the equivalence `two_is_square_iff`. -/347theorem two_is_square (F : Frame p κ g) (m : Nat) (hm : κ = 2 * m) : ∃ r : Shell p, r * r = 2 :=348 ⟨g ^ m + g ^ (7 * m), by rw [← Shell.pow_two]; exact (tsirelson_square F m hm).2.1⟩349350351/-! ## The converse: `2` a square ⇒ even capacity, on every frame (14:X4) -/352353354/-- Literals add as their values: `a + b = (a + b)` on every shell. -/355theorem lit_add (a b : Nat) : (OfNat.ofNat a : Shell p) + OfNat.ofNat b = (OfNat.ofNat (a + b) : Shell p) :=356 Shell.ext (by357 show (a % p + b % p) % p = (a + b) % p358 exact (FRC.Nat.add_mod a b p Pos.pos).symm)359360/-- `−1 ≠ 1` on every frame (`2 ≠ 0`). -/361theorem neg_one_ne_one (F : Frame p κ g) : (-1 : Shell p) ≠ 1 := fun h => by362 have h2 : (1 : Shell p) + 1 = 0 := by363 have := Shell.neg_add (1 : Shell p); rw [h] at this; exact this364 exact F.two_ne_zero (by rw [Frame.two_eq_one_add_one]; exact h2)365366/-- `−1 ≠ 0` on every frame. -/367theorem neg_one_ne_zero (F : Frame p κ g) : (-1 : Shell p) ≠ 0 := fun h => by368 have : (1 : Shell p) = 0 := by369 have h' : -(-1 : Shell p) = -0 := congrArg Neg.neg h370 rw [Shell.neg_neg, Shell.neg_zero] at h'371 exact h'372 exact F.one_ne_zero this373374/-- A square root of `2` gives a square root of the quarter-turn: with `i² = −1`, `2h = 1` and `r² = 2`,375`ζ = (r + i r) h` has `ζ² = i`, hence `ζ⁴ = −1` and `ζ⁸ = 1` — an element of order eight wherever `−1 ≠ 1`,376that is on every frame. -/377theorem octant_of_two_square {r i h : Shell p} (hr : r * r = 2) (hi : i * i = -1)378 (hh : 2 * h = 1) :379 ∃ ζ : Shell p, ζ * ζ = i ∧ ζ ^ 4 = -1 ∧ ζ ^ 8 = 1 := by380 -- `(r + i r)² = 4 i`381 have hA : (r + i * r) * (r + i * r) = i * 4 := by382 rw [Shell.left_distrib, Shell.right_distrib, Shell.right_distrib, hr,383 Shell.mul_assoc i r r, hr, Shell.mul_left_comm r i r, hr,384 Shell.mul_assoc i r (i * r), Shell.mul_left_comm r i r, ← Shell.mul_assoc i i (r * r), hi, hr,385 Shell.neg_one_mul, Shell.add_comm 2 (i * 2), Shell.add_assoc, Shell.add_comm 2 (i * 2 + -2),386 Shell.add_assoc, Shell.neg_add, Shell.add_zero, ← Shell.left_distrib, lit_add 2 2]387 -- `4 h² = (2h)² = 1`388 have h4 : (4 : Shell p) * (h * h) = 1 := by389 rw [← lit_mul 2 2, ← mul_mul_mul_comm, hh, Shell.one_mul]390 have hz : ((r + i * r) * h) * ((r + i * r) * h) = i := by391 rw [mul_mul_mul_comm, hA, Shell.mul_assoc, h4, Shell.mul_one]392 refine ⟨(r + i * r) * h, hz, ?_, ?_⟩393 · rw [show (4 : Nat) = 2 * 2 from rfl, Shell.pow_mul, Shell.pow_two, Shell.pow_two, hz, hi]394 · rw [show (8 : Nat) = 2 * 2 * 2 from rfl, Shell.pow_mul, Shell.pow_mul, Shell.pow_two, Shell.pow_two,395 Shell.pow_two, hz, hi, Shell.neg_mul_neg, Shell.one_mul]396397/-- The arithmetic of the order: `(k · 8) % 4κ = 0` and `(k · 4) % 4κ ≠ 0` force `κ` even (a divisor `4κ` of398`8k` that misses `4k` cannot be `4 · odd`; `0 < κ` is only what `mod_spec` needs). -/399theorem even_of_order_eight {κ k : Nat} (hκ : 0 < κ) (h8 : (k * 8) % (4 * κ) = 0)400 (h4 : (k * 4) % (4 * κ) ≠ 0) : ∃ m, κ = 2 * m := by401 have h4κ : 0 < 4 * κ := Nat.mul_pos (Nat.zero_lt_succ 3) hκ402 obtain ⟨q, hq⟩ := FRC.Nat.mod_spec (4 * κ) h4κ (k * 8)403 rw [h8, Nat.add_zero] at hq404 -- `2k = κ q`405 have h2k : 2 * k = κ * q := by406 apply Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ 3)407 rw [← FRC.Nat.mul_assoc, ← FRC.Nat.mul_assoc, Nat.mul_comm 4 2, Nat.mul_comm (2 * 4) k, ← hq]408 have h2 : 0 < 2 := Nat.zero_lt_succ 1409 obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 2 h2 κ410 have hlt : κ % 2 < 2 := FRC.Nat.mod_lt' κ h2411 match hκ2 : κ % 2 with412 | 0 => rw [hκ2, Nat.add_zero] at hm; exact ⟨m, hm⟩413 | 1 =>414 -- `κ` odd: `q` is even, `k = κ q'`, so `4κ ∣ 4k`, contradicting `h4`415 have hq2 : q % 2 = 0 := by416 have e1 : (κ * q) % 2 = q % 2 := by417 rw [FRC.Nat.mul_mod κ q 2 h2, hκ2, Nat.one_mul, FRC.Nat.mod_mod q 2 h2]418 have e2 : (2 * k) % 2 = 0 := by419 rw [Nat.mul_comm 2 k]420 exact (FRC.Nat.mod_unique (Nat.zero_lt_succ 1) (by rw [Nat.add_zero, Nat.mul_comm k 2]) : (k * 2) % 2 = 0)421 rw [← e1, ← h2k]; exact e2422 obtain ⟨q', hq'⟩ := FRC.Nat.mod_spec 2 h2 q423 rw [hq2, Nat.add_zero] at hq'424 have hk : k = κ * q' := by425 apply Nat.eq_of_mul_eq_mul_left h2426 rw [h2k, hq', Nat.mul_left_comm κ 2 q']427 exact absurd (FRC.Nat.mod_unique h4κ428 (by rw [hk, Nat.add_zero, Nat.mul_comm (κ * q') 4, ← FRC.Nat.mul_assoc])) h4429 | n + 2 => exact absurd hlt (by rw [hκ2]; exact Nat.not_lt_of_ge (Nat.le_add_left 2 n))430431/-- 14:C6 — the octant forces even capacity: on every frame, an element `ζ` with `ζ⁴ = −1` and `ζ⁸ = 1` (an432element of order eight) gives `8 ∣ 4κ`, so the capacity is even. -/433theorem even_capacity_of_octant (F : Frame p κ g) {ζ : Shell p} (hz4 : ζ ^ 4 = -1) (hz8 : ζ ^ 8 = 1) :434 ∃ m, κ = 2 * m := by435 have hζ0 : ζ ≠ 0 := fun h0 => by436 rw [h0, show (4 : Nat) = 3 + 1 from rfl, Shell.pow_succ, Shell.mul_zero] at hz4437 exact neg_one_ne_zero F hz4.symm438 obtain ⟨k, hk, hgk⟩ := F.eq_pow_of_ne_zero hζ0439 have e8 : (k * 8) % (p - 1) = 0 :=440 F.mod_eq_zero_of_pow_eq_one (by rw [Shell.pow_mul, hgk]; exact hz8)441 have e4 : (k * 4) % (p - 1) ≠ 0 := fun e => by442 have := F.pow_eq_one_of_mod e443 rw [Shell.pow_mul, hgk, hz4] at this444 exact neg_one_ne_one F this445 rw [F.n_eq] at e8 e4446 exact even_of_order_eight F.cap_pos e8 e4447448/-- 14:C6 — the octant sector at tier 0, as an equivalence: on every frame, an element with `ζ⁴ = −1` and449`ζ⁸ = 1` exists exactly when the capacity is even. -/450theorem octant_iff (F : Frame p κ g) : (∃ ζ : Shell p, ζ ^ 4 = -1 ∧ ζ ^ 8 = 1) ↔ ∃ m, κ = 2 * m :=451 ⟨fun ⟨_, h4, h8⟩ => even_capacity_of_octant F h4 h8,452 fun ⟨m, hm⟩ => ⟨g ^ m, octant_residue F m hm⟩⟩453454/-- 14:X4 — the converse of the second face at tier 0: on every frame, a square root of `2` forces the455capacity even — `ζ = (r + i r)/2` has `ζ² = i`, so an element of order eight exists and `8 ∣ 4κ`. -/456theorem even_capacity_of_two_square (F : Frame p κ g) {r : Shell p} (hr : r * r = 2) :457 ∃ m, κ = 2 * m := by458 obtain ⟨h, hh⟩ := F.exists_inv F.two_ne_zero459 obtain ⟨ζ, _, hz4, hz8⟩ := octant_of_two_square hr F.quarter_turn_sq hh460 exact even_capacity_of_octant F hz4 hz8461462/-- 14:X4 — the second face as an equivalence at tier 0: on every frame `(τ; 0, 1, g)`, `2` is a square463exactly when the capacity is even — the c-square congruence and the octant sector are one condition. -/464theorem two_is_square_iff (F : Frame p κ g) : (∃ r : Shell p, r * r = 2) ↔ ∃ m, κ = 2 * m :=465 ⟨fun ⟨_, hr⟩ => even_capacity_of_two_square F hr, fun ⟨m, hm⟩ => two_is_square F m hm⟩466467468end Frame469end Shell470end FRC471