Theme/Framed.lean — FrcCore

1import FrcCore.Frame2import FrcCore.Orbit3import FrcCore.Ring4import FrcCore.Theme.Field5import FrcCore.Theme.Foundation67/-!8# FrcCore.Theme.Framed — framed integers and framed rationals on the window (the algebra theme)910The algebra theme holds 1-algebra's exact content above the frame and the foundation (6 November 2026). This file:1112* the signed window integers `SInt` (a pair `(u, v)` read as `u − v`; no `Int`), their reading `sread`, the window13  bound `SBound`, and the signed window law `sread_inj` — moved here from the paper module `FrcCore/Quaternion.lean`,14  every name unchanged;15* the window law for framed rationals (1:D8): fractions `a/b` with `|a| ≤ N`, `1 ≤ b ≤ D` and `2ND < p` that read as16  the same residue are the same fraction (`frac_window`, `frac_window_inv`), so the products and the sums of window17  fractions read back on the windows `(H², H²)` and `(2H², H²)` (`frac_mul_readback`, `frac_add_readback`);18* the scale grid covers the shell (1:D9): every residue is `t · B⁻¹` for exactly one `t` with `|t| ≤ 2κ`19  (`signed_rep`, `signed_rep_unique`, `grid_cover`, `grid_unique`), and the nonzero residues form `2κ` sign pairs20  (`sign_pair`; 1:C4 with `vertex_count`);21* the complex chart is a field exactly off the shells (1:E2): on a prime `p ≡ 3 (mod 4)` every nonzero pair of22  `F_p[X]/(X² + 1)` is invertible (`complex_chart_field`);23* scale-periodicity made exact (1:D4): the grid `x · g^{−n}` returns to a nonzero point exactly when the scales24  agree modulo `p − 1`, the zoom has order exactly `p − 1`, and every grid lists the whole shell once;25* the circle in counts (1:E4): the rounding of a framed turn `u/v` to the cycle of `N` steps is within half a step,26  and the rounding's group-law defect is `−1`, `0` or `1` (`round_bounds`, `round_defect`).2728No axioms.29-/3031namespace FRC32namespace Shell33namespace Frame3435variable {p : Nat} [Pos p]3637/-- A signed window integer: `(u, v)` stands for `u − v`. -/38abbrev SInt := Nat × Nat3940def sread (x : SInt) : Shell p := ofNat x.1 + -(ofNat x.2)41def sadd (x y : SInt) : SInt := (x.1 + y.1, x.2 + y.2)42def sneg (x : SInt) : SInt := (x.2, x.1)43def smul (x y : SInt) : SInt := (x.1 * y.1 + x.2 * y.2, x.1 * y.2 + x.2 * y.1)44/-- The canonical pair of the same value: one component zero. -/45def snorm (x : SInt) : SInt := (x.1 - x.2, x.2 - x.1)4647theorem prod_ext {x y : SInt} (h1 : x.1 = y.1) (h2 : x.2 = y.2) : x = y :=48  match x, y, h1, h2 with49  | (_, _), (_, _), h1, h2 => by cases h1; cases h2; rfl5051theorem sread_add (x y : SInt) : (sread (sadd x y) : Shell p) = sread x + sread y := by52  unfold sread sadd53  show ofNat (x.1 + y.1) + -(ofNat (x.2 + y.2)) = ofNat x.1 + -(ofNat x.2) + (ofNat y.1 + -(ofNat y.2))54  rw [← ofNat_add, ← ofNat_add, neg_add_rev, add_assoc, add_assoc, ← add_assoc (-(ofNat x.2)),55    add_comm (-(ofNat x.2)) (ofNat y.1), add_assoc]5657theorem sread_neg (x : SInt) : (sread (sneg x) : Shell p) = -(sread x) := by58  unfold sread sneg59  show ofNat x.2 + -(ofNat x.1) = -(ofNat x.1 + -(ofNat x.2))60  rw [neg_add_rev, neg_neg, add_comm]6162theorem sread_mul (x y : SInt) : (sread (smul x y) : Shell p) = sread x * sread y := by63  unfold sread smul64  show ofNat (x.1 * y.1 + x.2 * y.2) + -(ofNat (x.1 * y.2 + x.2 * y.1)) =65    (ofNat x.1 + -(ofNat x.2)) * (ofNat y.1 + -(ofNat y.2))66  rw [right_distrib, left_distrib, left_distrib, ← mul_neg, ← neg_mul, neg_mul_neg, ← ofNat_add, ← ofNat_add,67    ← ofNat_mul, ← ofNat_mul, ← ofNat_mul, ← ofNat_mul, neg_add_rev]68  -- a + d + (-b + -c) = a + -b + (-c + d)69  rw [add_assoc, add_assoc]70  refine congrArg (ofNat x.1 * ofNat y.1 + ·) ?_71  rw [← add_assoc, add_comm (ofNat x.2 * ofNat y.2), add_assoc, add_comm (ofNat x.2 * ofNat y.2)]7273theorem sread_norm (x : SInt) : (sread (snorm x) : Shell p) = sread x := by74  unfold sread snorm75  match Nat.decLe x.2 x.1 with76  | .isTrue h =>77    have e : x.2 - x.1 = 0 := FRC.Nat.sub_eq_zero_of_le h78    show ofNat (x.1 - x.2) + -(ofNat (x.2 - x.1)) = ofNat x.1 + -(ofNat x.2)79    rw [e]80    have e0 : (ofNat 0 : Shell p) = 0 := rfl81    rw [e0, neg_zero, add_zero]82    have e1 : x.1 = (x.1 - x.2) + x.2 := (FRC.Nat.sub_add_cancel h).symm83    calc ofNat (x.1 - x.2) = ofNat (x.1 - x.2) + 0 := (add_zero _).symm84      _ = ofNat (x.1 - x.2) + (ofNat x.2 + -(ofNat x.2)) := by rw [add_neg]85      _ = ofNat (x.1 - x.2 + x.2) + -(ofNat x.2) := by rw [← add_assoc, ofNat_add]86      _ = ofNat x.1 + -(ofNat x.2) := by rw [← e1]87  | .isFalse h =>88    have h' : x.1 ≤ x.2 := Nat.le_of_lt (Nat.lt_of_not_le h)89    have e : x.1 - x.2 = 0 := FRC.Nat.sub_eq_zero_of_le h'90    show ofNat (x.1 - x.2) + -(ofNat (x.2 - x.1)) = ofNat x.1 + -(ofNat x.2)91    rw [e]92    have e0 : (ofNat 0 : Shell p) = 0 := rfl93    rw [e0, zero_add]94    have e1 : x.2 = (x.2 - x.1) + x.1 := (FRC.Nat.sub_add_cancel h').symm95    calc (-(ofNat (x.2 - x.1)) : Shell p) = (0 : Shell p) + -(ofNat (x.2 - x.1)) := (zero_add _).symm96      _ = (ofNat x.1 + -(ofNat x.1)) + -(ofNat (x.2 - x.1)) := by rw [add_neg]97      _ = ofNat x.1 + -((ofNat (x.2 - x.1) : Shell p) + ofNat x.1) := by98          rw [add_assoc, neg_add_rev, add_comm (-(ofNat x.1))]99      _ = ofNat x.1 + -(ofNat x.2) := by rw [ofNat_add, ← e1]100101/-- The window bound: both components at most `H`, one of them zero. -/102def SBound (H : Nat) (x : SInt) : Prop := x.1 ≤ H ∧ x.2 ≤ H ∧ (x.1 = 0 ∨ x.2 = 0)103104theorem sneg_bound {H : Nat} {x : SInt} (h : SBound H x) : SBound H (sneg x) :=105  ⟨h.2.1, h.1, match h.2.2 with | Or.inl e => Or.inr e | Or.inr e => Or.inl e⟩106107theorem smul_bound {H : Nat} {x y : SInt} (hx : SBound H x) (hy : SBound H y) : SBound (H * H) (smul x y) := by108  unfold smul109  have b11 := Nat.mul_le_mul hx.1 hy.1110  have b22 := Nat.mul_le_mul hx.2.1 hy.2.1111  have b12 := Nat.mul_le_mul hx.1 hy.2.1112  have b21 := Nat.mul_le_mul hx.2.1 hy.1113  match hx.2.2, hy.2.2 with114  | Or.inl e, Or.inl f =>115    refine ⟨?_, ?_, Or.inr ?_⟩116    · show x.1 * y.1 + x.2 * y.2 ≤ H * H117      rw [e, Nat.zero_mul, Nat.zero_add]; exact b22118    · show x.1 * y.2 + x.2 * y.1 ≤ H * H119      rw [e, f, Nat.zero_mul, Nat.mul_zero]; exact Nat.zero_le _120    · show x.1 * y.2 + x.2 * y.1 = 0121      rw [e, f, Nat.zero_mul, Nat.mul_zero]122  | Or.inl e, Or.inr f =>123    refine ⟨?_, ?_, Or.inl ?_⟩124    · show x.1 * y.1 + x.2 * y.2 ≤ H * H125      rw [e, f, Nat.zero_mul, Nat.mul_zero]; exact Nat.zero_le _126    · show x.1 * y.2 + x.2 * y.1 ≤ H * H127      rw [e, Nat.zero_mul, Nat.zero_add]; exact b21128    · show x.1 * y.1 + x.2 * y.2 = 0129      rw [e, f, Nat.zero_mul, Nat.mul_zero]130  | Or.inr e, Or.inl f =>131    refine ⟨?_, ?_, Or.inl ?_⟩132    · show x.1 * y.1 + x.2 * y.2 ≤ H * H133      rw [e, f, Nat.mul_zero, Nat.zero_mul]; exact Nat.zero_le _134    · show x.1 * y.2 + x.2 * y.1 ≤ H * H135      rw [e, Nat.zero_mul, Nat.add_zero]; exact b12136    · show x.1 * y.1 + x.2 * y.2 = 0137      rw [e, f, Nat.mul_zero, Nat.zero_mul]138  | Or.inr e, Or.inr f =>139    refine ⟨?_, ?_, Or.inr ?_⟩140    · show x.1 * y.1 + x.2 * y.2 ≤ H * H141      rw [e, Nat.zero_mul, Nat.add_zero]; exact b11142    · show x.1 * y.2 + x.2 * y.1 ≤ H * H143      rw [e, f, Nat.mul_zero, Nat.zero_mul]; exact Nat.zero_le _144    · show x.1 * y.2 + x.2 * y.1 = 0145      rw [e, f, Nat.mul_zero, Nat.zero_mul]146147/-- Four window terms of size `M` add to a pair with both components at most `4M`. -/148theorem sum4_bound {M : Nat} {t1 t2 t3 t4 : SInt} (h1 : SBound M t1) (h2 : SBound M t2) (h3 : SBound M t3)149    (h4 : SBound M t4) :150    (sadd (sadd t1 t2) (sadd t3 t4)).1 ≤ 4 * M ∧ (sadd (sadd t1 t2) (sadd t3 t4)).2 ≤ 4 * M := by151  unfold sadd152  rw [four_mul_eq, Nat.add_assoc (M + M) M M]153  exact ⟨Nat.add_le_add (Nat.add_le_add h1.1 h2.1) (Nat.add_le_add h3.1 h4.1),154    Nat.add_le_add (Nat.add_le_add h1.2.1 h2.2.1) (Nat.add_le_add h3.2.1 h4.2.1)⟩155156theorem snorm_bound {M : Nat} {x : SInt} (h1 : x.1 ≤ M) (h2 : x.2 ≤ M) : SBound M (snorm x) := by157  unfold snorm158  refine ⟨Nat.le_trans (Nat.sub_le _ _) h1, Nat.le_trans (Nat.sub_le _ _) h2, ?_⟩159  match Nat.decLe x.2 x.1 with160  | .isTrue h => exact Or.inr (FRC.Nat.sub_eq_zero_of_le h)161  | .isFalse h => exact Or.inl (FRC.Nat.sub_eq_zero_of_le (Nat.le_of_lt (Nat.lt_of_not_le h)))162163/-- The signed window law: two canonical pairs of size `M`, `2M < p`, with the same reading are equal. -/164theorem sread_inj {M : Nat} (hM : 2 * M < p) {x y : SInt} (hx : SBound M x) (hy : SBound M y)165    (h : (sread x : Shell p) = sread y) : x = y := by166  unfold sread at h167  have h' : (ofNat (x.1 + y.2) : Shell p) = ofNat (y.1 + x.2) := by168    rw [← ofNat_add, ← ofNat_add]169    calc ofNat x.1 + ofNat y.2 = ofNat x.1 + -(ofNat x.2) + (ofNat x.2 + ofNat y.2) := by170          rw [add_assoc, ← add_assoc (-(ofNat x.2)), neg_add, zero_add]171      _ = ofNat y.1 + -(ofNat y.2) + (ofNat x.2 + ofNat y.2) := by rw [h]172      _ = ofNat y.1 + ofNat x.2 := by173          rw [add_assoc, add_comm (ofNat x.2), ← add_assoc (-(ofNat y.2)), neg_add, zero_add]174  have hv := val_injective h'175  rw [val_ofNat, val_ofNat] at hv176  have l1 : x.1 + y.2 < p := Nat.lt_of_le_of_lt (Nat.add_le_add hx.1 hy.2.1) (Nat.two_mul M ▸ hM)177  have l2 : y.1 + x.2 < p := Nat.lt_of_le_of_lt (Nat.add_le_add hy.1 hx.2.1) (Nat.two_mul M ▸ hM)178  rw [FRC.Nat.mod_eq_of_lt l1, FRC.Nat.mod_eq_of_lt l2] at hv179  -- hv : x.1 + y.2 = y.1 + x.2180  match hx.2.2, hy.2.2 with181  | Or.inl e, Or.inl f =>182    rw [e, f, Nat.zero_add, Nat.zero_add] at hv183    exact prod_ext (e.trans f.symm) hv.symm184  | Or.inl e, Or.inr f =>185    rw [e, f, Nat.zero_add] at hv186    -- hv : 0 = y.1 + x.2187    have hy1 : y.1 = 0 := Nat.eq_zero_of_add_eq_zero_right hv.symm188    have hx2 : x.2 = 0 := Nat.eq_zero_of_add_eq_zero_left hv.symm189    exact prod_ext (e.trans hy1.symm) (hx2.trans f.symm)190  | Or.inr e, Or.inl f =>191    rw [e, f, Nat.zero_add] at hv192    -- hv : x.1 + y.2 = 0193    have hx1 : x.1 = 0 := Nat.eq_zero_of_add_eq_zero_right hv194    have hy2 : y.2 = 0 := Nat.eq_zero_of_add_eq_zero_left hv195    exact prod_ext (hx1.trans f.symm) (e.trans hy2.symm)196  | Or.inr e, Or.inr f =>197    rw [e, f, Nat.add_zero, Nat.add_zero] at hv198    exact prod_ext hv (e.trans f.symm)199200201/-! ## Framed rationals: the window law (1:D8) -/202203/-- A natural number as a signed window integer reads as itself. -/204theorem sread_nat (b : Nat) : (sread (b, 0) : Shell p) = ofNat b := by205  unfold sread206  show ofNat b + -(ofNat 0 : Shell p) = ofNat b207  have e0 : (ofNat 0 : Shell p) = 0 := rfl208  rw [e0, neg_zero, add_zero]209210theorem nat_bound {D b : Nat} (hb : b ≤ D) : SBound D (b, 0) := ⟨hb, Nat.zero_le D, Or.inr rfl⟩211212/-- The product of window integers of sizes `N` and `D` is a window integer of size `N·D`. -/213theorem smul_bound2 {N D : Nat} {x y : SInt} (hx : SBound N x) (hy : SBound D y) : SBound (N * D) (smul x y) := by214  unfold smul215  have b11 := Nat.mul_le_mul hx.1 hy.1216  have b22 := Nat.mul_le_mul hx.2.1 hy.2.1217  have b12 := Nat.mul_le_mul hx.1 hy.2.1218  have b21 := Nat.mul_le_mul hx.2.1 hy.1219  match hx.2.2, hy.2.2 with220  | Or.inl e, Or.inl f =>221    refine ⟨?_, ?_, Or.inr ?_⟩222    · show x.1 * y.1 + x.2 * y.2 ≤ N * D223      rw [e, Nat.zero_mul, Nat.zero_add]; exact b22224    · show x.1 * y.2 + x.2 * y.1 ≤ N * D225      rw [e, f, Nat.zero_mul, Nat.mul_zero]; exact Nat.zero_le _226    · show x.1 * y.2 + x.2 * y.1 = 0227      rw [e, f, Nat.zero_mul, Nat.mul_zero]228  | Or.inl e, Or.inr f =>229    refine ⟨?_, ?_, Or.inl ?_⟩230    · show x.1 * y.1 + x.2 * y.2 ≤ N * D231      rw [e, f, Nat.zero_mul, Nat.mul_zero]; exact Nat.zero_le _232    · show x.1 * y.2 + x.2 * y.1 ≤ N * D233      rw [e, Nat.zero_mul, Nat.zero_add]; exact b21234    · show x.1 * y.1 + x.2 * y.2 = 0235      rw [e, f, Nat.zero_mul, Nat.mul_zero]236  | Or.inr e, Or.inl f =>237    refine ⟨?_, ?_, Or.inl ?_⟩238    · show x.1 * y.1 + x.2 * y.2 ≤ N * D239      rw [e, f, Nat.mul_zero, Nat.zero_mul]; exact Nat.zero_le _240    · show x.1 * y.2 + x.2 * y.1 ≤ N * D241      rw [e, Nat.zero_mul, Nat.add_zero]; exact b12242    · show x.1 * y.1 + x.2 * y.2 = 0243      rw [e, f, Nat.mul_zero, Nat.zero_mul]244  | Or.inr e, Or.inr f =>245    refine ⟨?_, ?_, Or.inr ?_⟩246    · show x.1 * y.1 + x.2 * y.2 ≤ N * D247      rw [e, Nat.zero_mul, Nat.add_zero]; exact b11248    · show x.1 * y.2 + x.2 * y.1 ≤ N * D249      rw [e, f, Nat.mul_zero, Nat.zero_mul]; exact Nat.zero_le _250    · show x.1 * y.2 + x.2 * y.1 = 0251      rw [e, f, Nat.mul_zero, Nat.zero_mul]252253/-- 1:D8, the window law for framed rationals — two fractions `a₁/b₁`, `a₂/b₂` with `|aᵢ| ≤ N`, `bᵢ ≤ D` and254`2ND < p` whose cross-products agree on the shell, `a₁ b₂ ≡ a₂ b₁`, are the same fraction: `a₁ b₂ = a₂ b₁` as255integers. -/256theorem frac_window {N D : Nat} (hND : 2 * (N * D) < p) {a₁ a₂ : SInt} {b₁ b₂ : Nat}257    (ha₁ : SBound N a₁) (ha₂ : SBound N a₂) (hb₁ : b₁ ≤ D) (hb₂ : b₂ ≤ D)258    (h : (sread a₁ : Shell p) * ofNat b₂ = sread a₂ * ofNat b₁) :259    smul a₁ (b₂, 0) = smul a₂ (b₁, 0) := by260  apply sread_inj hND (smul_bound2 ha₁ (nat_bound hb₂)) (smul_bound2 ha₂ (nat_bound hb₁))261  rw [sread_mul, sread_mul, sread_nat, sread_nat]; exact h262263/-- 1:D8, in the residues of the fractions — `a₁ · b₁⁻¹ = a₂ · b₂⁻¹` on the shell, with the window bounds and264`2ND < p`, forces `a₁ b₂ = a₂ b₁`: distinct window fractions take distinct residues. -/265theorem frac_window_inv {N D : Nat} (hND : 2 * (N * D) < p) {a₁ a₂ : SInt} {b₁ b₂ : Nat} {y₁ y₂ : Shell p}266    (ha₁ : SBound N a₁) (ha₂ : SBound N a₂) (hb₁ : b₁ ≤ D) (hb₂ : b₂ ≤ D)267    (hy₁ : (ofNat b₁ : Shell p) * y₁ = 1) (hy₂ : (ofNat b₂ : Shell p) * y₂ = 1)268    (h : (sread a₁ : Shell p) * y₁ = sread a₂ * y₂) :269    smul a₁ (b₂, 0) = smul a₂ (b₁, 0) := by270  apply frac_window hND ha₁ ha₂ hb₁ hb₂271  calc (sread a₁ : Shell p) * ofNat b₂ = sread a₁ * (ofNat b₁ * y₁) * ofNat b₂ := by rw [hy₁, mul_one]272    _ = (sread a₁ * y₁) * (ofNat b₁ * ofNat b₂) :=273        RE.sound (look [sread a₁, ofNat b₁, y₁, ofNat b₂]) (.mul (.mul (.var 0) (.mul (.var 1) (.var 2))) (.var 3))274          (.mul (.mul (.var 0) (.var 2)) (.mul (.var 1) (.var 3))) (by decide +kernel)275    _ = (sread a₂ * y₂) * (ofNat b₁ * ofNat b₂) := by rw [h]276    _ = (sread a₂ * ofNat b₁) * (ofNat b₂ * y₂) :=277        RE.sound (look [sread a₂, y₂, ofNat b₁, ofNat b₂]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))278          (.mul (.mul (.var 0) (.var 2)) (.mul (.var 3) (.var 1))) (by decide +kernel)279    _ = sread a₂ * ofNat b₁ := by rw [hy₂, mul_one]280281/-- 1:D8, products read back — for window fractions `a/b`, `c/d` (`|a|, |c|, b, d ≤ H`) the product `ac/bd` lies282in the window `(H², H²)`; when `2H⁴ < p` the residue of the product determines it among that window's fractions283`e/f`. -/284theorem frac_mul_readback {H : Nat} (hH : 2 * ((H * H) * (H * H)) < p) {a c e : SInt} {b d f : Nat}285    {yb yd yf : Shell p} (ha : SBound H a) (hc : SBound H c) (hb : b ≤ H) (hd : d ≤ H)286    (he : SBound (H * H) e) (hf : f ≤ H * H)287    (hyb : (ofNat b : Shell p) * yb = 1) (hyd : (ofNat d : Shell p) * yd = 1) (hyf : (ofNat f : Shell p) * yf = 1)288    (h : (sread a * yb) * (sread c * yd) = (sread e : Shell p) * yf) :289    smul (smul a c) (f, 0) = smul e (b * d, 0) := by290  have hbd : (ofNat (b * d) : Shell p) * (yb * yd) = 1 := by291    rw [← ofNat_mul]292    calc (ofNat b : Shell p) * ofNat d * (yb * yd) = (ofNat b * yb) * (ofNat d * yd) :=293          RE.sound (look [ofNat b, ofNat d, yb, yd]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))294            (.mul (.mul (.var 0) (.var 2)) (.mul (.var 1) (.var 3))) (by decide +kernel)295      _ = 1 := by rw [hyb, hyd, mul_one]296  apply frac_window_inv hH (smul_bound ha hc) he (Nat.mul_le_mul hb hd) hf hbd hyf297  rw [sread_mul]298  rw [← h]299  exact RE.sound (look [sread a, sread c, yb, yd]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))300    (.mul (.mul (.var 0) (.var 2)) (.mul (.var 1) (.var 3))) (by decide +kernel)301302/-- 1:D8, sums read back — for window fractions `a/b`, `c/d` the sum `(ad + cb)/bd` lies in the window303`(2H², H²)`; when `4H⁴ < p` its residue determines it among that window's fractions `e/f`. -/304theorem frac_add_readback {H : Nat} (hH : 2 * ((H * H + H * H) * (H * H)) < p) {a c e : SInt} {b d f : Nat}305    {yb yd yf : Shell p} (ha : SBound H a) (hc : SBound H c) (hb : b ≤ H) (hd : d ≤ H)306    (he : SBound (H * H + H * H) e) (hf : f ≤ H * H)307    (hyb : (ofNat b : Shell p) * yb = 1) (hyd : (ofNat d : Shell p) * yd = 1) (hyf : (ofNat f : Shell p) * yf = 1)308    (h : sread a * yb + sread c * yd = (sread e : Shell p) * yf) :309    smul (snorm (sadd (smul a (d, 0)) (smul c (b, 0)))) (f, 0) = smul e (b * d, 0) := by310  have hbd : (ofNat (b * d) : Shell p) * (yb * yd) = 1 := by311    rw [← ofNat_mul]312    calc (ofNat b : Shell p) * ofNat d * (yb * yd) = (ofNat b * yb) * (ofNat d * yd) :=313          RE.sound (look [ofNat b, ofNat d, yb, yd]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))314            (.mul (.mul (.var 0) (.var 2)) (.mul (.var 1) (.var 3))) (by decide +kernel)315      _ = 1 := by rw [hyb, hyd, mul_one]316  have h1 := smul_bound2 ha (nat_bound hd)317  have h2 := smul_bound2 hc (nat_bound hb)318  have hs : SBound (H * H + H * H) (snorm (sadd (smul a (d, 0)) (smul c (b, 0)))) :=319    snorm_bound (Nat.add_le_add h1.1 h2.1) (Nat.add_le_add h1.2.1 h2.2.1)320  apply frac_window_inv hH hs he (Nat.mul_le_mul hb hd) hf hbd hyf321  rw [sread_norm, sread_add, sread_mul, sread_mul, sread_nat, sread_nat, ← h]322  -- (a d + c b) · (yb yd) = a yb (d yd) + c yd (b yb)323  calc (sread a * ofNat d + sread c * ofNat b) * (yb * yd)324        = sread a * yb * (ofNat d * yd) + sread c * yd * (ofNat b * yb) :=325          RE.sound (look [sread a, ofNat d, sread c, ofNat b, yb, yd])326            (.mul (.add (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3))) (.mul (.var 4) (.var 5)))327            (.add (.mul (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 5))) (.mul (.mul (.var 2) (.var 5)) (.mul (.var 3) (.var 4))))328            (by decide +kernel)329    _ = sread a * yb + sread c * yd := by rw [hyd, hyb, mul_one, mul_one]330331/-! ## The scale grid covers the shell (1:D9) and the sign pairs (1:C4) -/332333theorem four_eq_two_two (κ : Nat) : 4 * κ = 2 * κ + 2 * κ := by334  rw [four_mul_eq, Nat.two_mul, Nat.add_assoc (κ + κ) κ κ]335336omit [Pos p] in337theorem two_two_lt {κ : Nat} (hcap : p = 4 * κ + 1) : 2 * (2 * κ) < p := by338  rw [hcap, Nat.two_mul (2 * κ), ← four_eq_two_two]; exact Nat.lt_succ_self _339340/-- 1:D9 — every residue of the shell `p = 4κ + 1` is the reading of exactly one signed window integer of size `2κ`341(existence here, uniqueness `signed_rep_unique`). -/342theorem signed_rep {κ : Nat} (hcap : p = 4 * κ + 1) (x : Shell p) : ∃ t : SInt, SBound (2 * κ) t ∧ (sread t : Shell p) = x := by343  match Nat.decLe x.val (2 * κ) with344  | .isTrue h => exact ⟨(x.val, 0), nat_bound h, by rw [sread_nat, ofNat_val]⟩345  | .isFalse h =>346    have hlt : 2 * κ < x.val := Nat.lt_of_not_le h347    have hxp : x.val ≤ p := Nat.le_of_lt x.lt348    refine ⟨(0, p - x.val), ⟨Nat.zero_le _, ?_, Or.inl rfl⟩, ?_⟩349    · apply FRC.Nat.sub_le_of_le_add350      -- p ≤ 2κ + x.val351      have e : p = 2 * κ + (2 * κ + 1) := by rw [hcap, four_eq_two_two, Nat.add_assoc]352      calc p = 2 * κ + (2 * κ + 1) := e353        _ ≤ 2 * κ + x.val := Nat.add_le_add_left (Nat.succ_le_of_lt hlt) (2 * κ)354    · unfold sread355      show ofNat 0 + -(ofNat (p - x.val)) = x356      have e0 : (ofNat 0 : Shell p) = 0 := rfl357      rw [e0, zero_add]358      have hs : (ofNat (p - x.val) : Shell p) + ofNat x.val = 0 := by359        rw [ofNat_add, FRC.Nat.sub_add_cancel hxp, ofNat_self]360      rw [neg_eq_of_add_eq_zero hs, ofNat_val]361362/-- 1:D9, uniqueness — two signed window integers of size `2κ` with the same reading are equal. -/363theorem signed_rep_unique {κ : Nat} (hcap : p = 4 * κ + 1) {t t' : SInt} (ht : SBound (2 * κ) t) (ht' : SBound (2 * κ) t')364    (h : (sread t : Shell p) = sread t') : t = t' :=365  sread_inj (two_two_lt hcap) ht ht' h366367/-- 1:D9 — for every unit `B` (`B · y = 1`) the scale grid `t · B⁻¹`, `|t| ≤ 2κ`, covers the shell. -/368theorem grid_cover {κ : Nat} (hcap : p = 4 * κ + 1) {B y : Shell p} (hBy : B * y = 1) (x : Shell p) :369    ∃ t : SInt, SBound (2 * κ) t ∧ (sread t : Shell p) * y = x := by370  obtain ⟨t, ht, hr⟩ := signed_rep hcap (x * B)371  exact ⟨t, ht, by rw [hr, mul_assoc, hBy, mul_one]⟩372373/-- 1:D9 — and each residue sits on the grid once: `t · B⁻¹ = t' · B⁻¹` with `|t|, |t'| ≤ 2κ` forces `t = t'`. -/374theorem grid_unique {κ : Nat} (hcap : p = 4 * κ + 1) {B y : Shell p} (hBy : B * y = 1) {t t' : SInt}375    (ht : SBound (2 * κ) t) (ht' : SBound (2 * κ) t') (h : (sread t : Shell p) * y = sread t' * y) : t = t' := by376  apply signed_rep_unique hcap ht ht'377  calc (sread t : Shell p) = sread t * (B * y) := by rw [hBy, mul_one]378    _ = sread t * y * B := by rw [mul_comm B y, mul_assoc]379    _ = sread t' * y * B := by rw [h]380    _ = sread t' := by rw [mul_assoc, mul_comm y B, hBy, mul_one]381382/-- 1:C4 — the nonzero residues form `2κ` sign pairs: every `x ≠ 0` is `a` or `−a` for some `1 ≤ a ≤ 2κ`383(the pair is unique by `window_injective` and `window_signed` at `H = 2κ`). -/384theorem sign_pair {κ : Nat} (hcap : p = 4 * κ + 1) {x : Shell p} (hx : x ≠ 0) :385    ∃ a, 0 < a ∧ a ≤ 2 * κ ∧ (x = ofNat a ∨ x = -(ofNat a)) := by386  obtain ⟨t, ht, hr⟩ := signed_rep hcap x387  have e0 : (ofNat 0 : Shell p) = 0 := rfl388  match ht.2.2 with389  | Or.inr e =>390    have hx' : x = ofNat t.1 := by391      rw [← hr]; unfold sread; rw [e, e0, neg_zero, add_zero]392    refine ⟨t.1, Nat.pos_of_ne_zero (fun h0 => hx (by rw [hx', h0]; rfl)), ht.1, Or.inl hx'⟩393  | Or.inl e =>394    have hx' : x = -(ofNat t.2) := by395      rw [← hr]; unfold sread; rw [e, e0, zero_add]396    refine ⟨t.2, Nat.pos_of_ne_zero (fun h0 => hx (by rw [hx', h0, e0, neg_zero])), ht.2.1, Or.inr hx'⟩397398/-- 1:C4 — the one-sided vertex count: `(p − 1)² = 2 · (2κ · (p − 1))`, with `p − 1 = 4κ`; the orbital complex has399`2κ(p − 1) + 1` vertices, half its double cover plus the origin. -/400theorem vertex_count (κ : Nat) : (4 * κ) * (4 * κ) = 2 * ((2 * κ) * (4 * κ)) := by401  rw [← FRC.Nat.mul_assoc 2 (2 * κ) (4 * κ), ← FRC.Nat.mul_assoc 2 2 κ]402403/-! ## The complex chart off the shells (1:E2) -/404405/-- Inverses on a prime shell (Fermat; as `Theme/Hopf.lean`'s `exists_inv`, restated in the algebra theme). -/406theorem inv_of_prime (hp : FRC.Nat.isPrime p) {x : Shell p} (hx : x ≠ 0) : ∃ y, x * y = 1 := by407  refine ⟨x ^ (p - 2), ?_⟩408  have e : p - 1 = (p - 2) + 1 := by409    have h2 : 2 ≤ p := Prime.two_le hp410    have : p = (p - 2) + 2 := (FRC.Nat.sub_add_cancel h2).symm411    rw [this, FRC.Nat.add_sub_cancel]; rfl412  rw [mul_comm, ← pow_succ, ← e]; exact Prime.fermat hp hx413414/-- 1:E2, the converse — on a prime `p ≡ 3 (mod 4)` the chart `F_p[X]/(X² + 1)` is a field: every nonzero pair415`(a, b)` has the inverse `(a, −b)/(a² + b²)`, since `a² + b² = 0` with `b ≠ 0` would make `a/b` a square root of `−1`. -/416theorem complex_chart_field (hp : FRC.Nat.isPrime p) (h3 : p % 4 = 3) {x : Shell p × Shell p} (hx : x ≠ (0, 0)) :417    ∃ y, cmul x y = (1, 0) := by418  have h2 : 2 < p := by419    match Nat.lt_or_ge 2 p with420    | Or.inl h => exact h421    | Or.inr h =>422      have hp2 : p = 2 := Nat.le_antisymm h (Prime.two_le hp)423      rw [hp2] at h3; exact absurd h3 (by decide)424  have hn : x.1 * x.1 + x.2 * x.2 ≠ 0 := by425    intro hn426    match decEq x.2 0 with427    | isTrue hb =>428      rw [hb, mul_zero, add_zero] at hn429      have ha : x.1 = 0 := match Prime.mul_eq_zero hp hn with | Or.inl h => h | Or.inr h => h430      exact hx (Prod.ext ha hb)431    | isFalse hb =>432      obtain ⟨yb, hyb⟩ := inv_of_prime hp hb433      have hsq : (x.1 * yb) * (x.1 * yb) = -1 := by434        have ha : x.1 * x.1 = -(x.2 * x.2) := eq_neg_of_add_eq_zero hn435        calc (x.1 * yb) * (x.1 * yb) = (x.1 * x.1) * (yb * yb) :=436              RE.sound (look [x.1, yb]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1)))437                (.mul (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1))) (by decide +kernel)438          _ = -((x.2 * yb) * (x.2 * yb)) := by439              rw [ha]440              exact RE.sound (look [x.2, yb]) (.mul (.neg (.mul (.var 0) (.var 0))) (.mul (.var 1) (.var 1)))441                (.neg (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1)))) (by decide +kernel)442          _ = -1 := by rw [hyb, mul_one]443      have h1 : p % 4 = 1 := (FRC.Shell.Prime.quarter_turn_iff hp h2).1 ⟨_, hsq⟩444      rw [h1] at h3; exact absurd h3 (by decide)445  obtain ⟨m, hm⟩ := inv_of_prime hp hn446  refine ⟨(x.1 * m, -(x.2 * m)), ?_⟩447  unfold cmul448  show (x.1 * (x.1 * m) + -(x.2 * -(x.2 * m)), x.1 * -(x.2 * m) + x.2 * (x.1 * m)) = (1, 0)449  have e1 : x.1 * (x.1 * m) + -(x.2 * -(x.2 * m)) = (x.1 * x.1 + x.2 * x.2) * m :=450    RE.sound (look [x.1, x.2, m]) (.add (.mul (.var 0) (.mul (.var 0) (.var 2))) (.neg (.mul (.var 1) (.neg (.mul (.var 1) (.var 2))))))451      (.mul (.add (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1))) (.var 2)) (by decide +kernel)452  have e2 : x.1 * -(x.2 * m) + x.2 * (x.1 * m) = 0 :=453    RE.sound (look [x.1, x.2, m]) (.add (.mul (.var 0) (.neg (.mul (.var 1) (.var 2)))) (.mul (.var 1) (.mul (.var 0) (.var 2))))454      .zero (by decide +kernel)455  rw [e1, e2, hm]456457/-! ## Scale-periodicity, exact (1:D4)458459The grid at scale `n` is `G_n = (x · g^{−n})_x`, written with the inverse `y` of the drive (`g · y = 1`), so that460`x · y^n = x g^{−n}`. The frame theme's `scale_periodic` gives the period `p − 1`; the theorems below make it exact:461two scales give the same grid point of a nonzero `x` exactly when they agree modulo `p − 1`, the zoom `y` has order462exactly `p − 1`, and every grid is the whole shell, each residue once. -/463464/-- The inverse drive's powers invert the drive's: `g^k · y^k = 1` when `g · y = 1`. -/465theorem inv_pow {g y : Shell p} (hy : g * y = 1) (k : Nat) : g ^ k * y ^ k = 1 := by466  rw [← mul_pow, hy, one_pow]467468/-- Cancellation by a nonzero residue on a framed shell: `x · a = x · b` with `x ≠ 0` forces `a = b`. -/469theorem mul_cancel {κ : Nat} {g : Shell p} (F : Frame p κ g) {x a b : Shell p} (hx : x ≠ 0) (h : x * a = x * b) :470    a = b := by471  obtain ⟨z, hz⟩ := F.exists_inv hx472  calc a = z * x * a := by rw [mul_comm z x, hz, one_mul]473    _ = z * (x * b) := by rw [mul_assoc, h]474    _ = b := by rw [← mul_assoc, mul_comm z x, hz, one_mul]475476/-- 1:D4 — the grid of scale `n` is periodic in `n` with period `p − 1`: `x · y^{n+(p−1)} = x · y^n`. -/477theorem scale_inv_periodic {κ : Nat} {g y : Shell p} (F : Frame p κ g) (hy : g * y = 1) (x : Shell p) (n : Nat) :478    x * y ^ (n + (p - 1)) = x * y ^ n := by479  have h1 : y ^ (p - 1) = 1 := by480    calc y ^ (p - 1) = g ^ (p - 1) * y ^ (p - 1) := by rw [F.pow_n, one_mul]481      _ = 1 := inv_pow hy _482  rw [pow_add, h1, mul_one]483484/-- The drive's powers agree exactly when their exponents agree modulo `p − 1`. -/485theorem pow_eq_iff {κ : Nat} {g : Shell p} (F : Frame p κ g) (m n : Nat) :486    g ^ m = g ^ n ↔ m % (p - 1) = n % (p - 1) := by487  constructor488  · intro h489    rw [F.pow_mod m, F.pow_mod n] at h490    exact F.pow_inj (Nat.mod_lt m F.n_pos) (Nat.mod_lt n F.n_pos) h491  · intro h; rw [F.pow_mod m, F.pow_mod n, h]492493/-- 1:D4, the period is exact — for a nonzero `x` the grid points `x · y^m` and `x · y^n` coincide exactly when494`m ≡ n (mod p − 1)`: no smaller shift of scale returns a nonzero point to its place. -/495theorem scale_exact {κ : Nat} {g y : Shell p} (F : Frame p κ g) (hy : g * y = 1) {x : Shell p} (hx : x ≠ 0)496    (m n : Nat) : x * y ^ m = x * y ^ n ↔ m % (p - 1) = n % (p - 1) := by497  constructor498  · intro h499    have e : y ^ m = y ^ n := mul_cancel F hx h500    have hg : g ^ m = g ^ n := by501      calc g ^ m = g ^ m * (g ^ n * y ^ n) := by rw [inv_pow hy n, mul_one]502        _ = g ^ n * (g ^ m * y ^ n) := mul_left_comm _ _ _503        _ = g ^ n * (g ^ m * y ^ m) := by rw [e]504        _ = g ^ n := by rw [inv_pow hy m, mul_one]505    exact (pow_eq_iff F m n).1 hg506  · intro h507    have e : g ^ m = g ^ n := (pow_eq_iff F m n).2 h508    have ey : y ^ m = y ^ n := by509      calc y ^ m = y ^ m * (g ^ n * y ^ n) := by rw [inv_pow hy n, mul_one]510        _ = y ^ m * (g ^ m * y ^ n) := by rw [e]511        _ = (g ^ m * y ^ m) * y ^ n := by rw [← mul_assoc, mul_comm (y ^ m) (g ^ m)]512        _ = y ^ n := by rw [inv_pow hy m, one_mul]513    rw [ey]514515/-- 1:D4, the zoom has order `p − 1` — the zoom by `k` steps fixes every grid point, `x · y^k = x` for all `x`,516exactly when `(p − 1) ∣ k`. -/517theorem zoom_order {κ : Nat} {g y : Shell p} (F : Frame p κ g) (hy : g * y = 1) (k : Nat) :518    (∀ x : Shell p, x * y ^ k = x) ↔ k % (p - 1) = 0 := by519  have h0 : k % (p - 1) = 0 % (p - 1) ↔ k % (p - 1) = 0 := by520    rw [FRC.Nat.mod_eq_of_lt F.n_pos]521  constructor522  · intro h523    have e := h 1524    rw [one_mul] at e525    have e' : (1 : Shell p) * y ^ k = 1 * y ^ 0 := by rw [one_mul, e, pow_zero, one_mul]526    exact h0.1 ((scale_exact F hy F.one_ne_zero k 0).1 e')527  · intro h x528    have e := (scale_exact F hy F.one_ne_zero k 0).2 (h0.2 h)529    rw [one_mul, one_mul, pow_zero] at e530    rw [e, mul_one]531532/-- 1:D4, every grid is the whole shell — the scale map `x ↦ x · y^n` is onto (`z = (z g^n) y^n`) and one-to-one,533so each grid `G_n` lists every residue once, and `G_m`, `G_n` are equal as ordered lists exactly when534`m ≡ n (mod p − 1)` (`scale_exact` at `x = 1`, `scale_inv_periodic`). -/535theorem scale_bijective {κ : Nat} {g y : Shell p} (F : Frame p κ g) (hy : g * y = 1) (n : Nat) :536    (∀ z : Shell p, (z * g ^ n) * y ^ n = z) ∧ (∀ x x' : Shell p, x * y ^ n = x' * y ^ n → x = x') := by537  refine ⟨fun z => by rw [mul_assoc, inv_pow hy n, mul_one], fun x x' h => ?_⟩538  have hyn : y ^ n ≠ 0 := fun h0 => F.one_ne_zero (by rw [← inv_pow hy n, h0, mul_zero])539  rw [mul_comm x, mul_comm x'] at h540  exact mul_cancel F hyn h541542/-! ## The circle in counts (1:E4) -/543544/-- `k` rounds the framed turn `u/v` to the cycle of `N` steps: `2vk ≤ 2Nu + v < 2vk + 2v`, that is545`k = ⌊Nu/v + 1/2⌋` and `|k/N − u/v| ≤ 1/(2N)`. -/546def IsRound (N u v k : Nat) : Prop := 2 * v * k ≤ 2 * N * u + v ∧ 2 * N * u + v < 2 * v * k + 2 * v547548theorem two_v_pos {v : Nat} (hv : 0 < v) : 0 < 2 * v := Nat.mul_pos (Nat.zero_lt_succ 1) hv549550/-- 1:E4, 2:E2, 2:E4 — every framed turn has its rounding (the division with remainder by `2v`). -/551theorem round_exists (N u v : Nat) (hv : 0 < v) : ∃ k, IsRound N u v k := by552  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec (2 * v) (two_v_pos hv) (2 * N * u + v)553  have hr := Nat.mod_lt (2 * N * u + v) (two_v_pos hv)554  refine ⟨q, ?_, ?_⟩555  · calc 2 * v * q ≤ 2 * v * q + (2 * N * u + v) % (2 * v) := Nat.le_add_right _ _556      _ = 2 * N * u + v := hq.symm557  · calc 2 * N * u + v = 2 * v * q + (2 * N * u + v) % (2 * v) := hq558      _ < 2 * v * q + 2 * v := Nat.add_lt_add_left hr _559560theorem lt_of_mul_lt {c a b : Nat} (h : c * a < c * b) : a < b :=561  match Nat.lt_or_ge a b with562  | Or.inl hab => hab563  | Or.inr hba => absurd (Nat.lt_of_lt_of_le h (Nat.mul_le_mul_left c hba)) (Nat.lt_irrefl _)564565theorem shuffle (A B v : Nat) : (A + v) + (B + v) = (A + B + v) + v := by566  rw [Nat.add_assoc A v, Nat.add_comm v (B + v), Nat.add_assoc B v v, ← Nat.add_assoc A B (v + v), Nat.add_assoc (A + B) v v]567568theorem round_step (v k : Nat) : 2 * v * k + 2 * v = 2 * v * (k + 1) := (Nat.mul_succ (2 * v) k).symm569570/-- 1:E4 — the rounding's group-law defect is `−1`, `0` or `1`: `k(u) + k(u′)` and `k(u + u′)` differ by at most one571step of the cycle. -/572theorem round_defect {N u u' v k₁ k₂ k₃ : Nat} (hv : 0 < v) (h₁ : IsRound N u v k₁) (h₂ : IsRound N u' v k₂)573    (h₃ : IsRound N (u + u') v k₃) : k₁ + k₂ ≤ k₃ + 1 ∧ k₃ ≤ k₁ + k₂ + 1 := by574  have hX : 2 * N * (u + u') = 2 * N * u + 2 * N * u' := Nat.left_distrib _ _ _575  have hvv : v < 2 * v := by576    rw [Nat.two_mul]; exact Nat.lt_add_of_pos_right hv577  refine ⟨Nat.le_of_lt_succ (lt_of_mul_lt (c := 2 * v) ?_), Nat.le_of_lt_succ (lt_of_mul_lt (c := 2 * v) ?_)⟩578  · -- 2v(k₁ + k₂) ≤ (2Nu + v) + (2Nu′ + v) = 2N(u + u′) + v + v < 2v k₃ + 2v + v < 2v(k₃ + 2)579    calc 2 * v * (k₁ + k₂) = 2 * v * k₁ + 2 * v * k₂ := Nat.left_distrib _ _ _580      _ ≤ (2 * N * u + v) + (2 * N * u' + v) := Nat.add_le_add h₁.1 h₂.1581      _ = (2 * N * (u + u') + v) + v := by rw [hX]; exact shuffle _ _ _582      _ < (2 * v * k₃ + 2 * v) + v := Nat.add_lt_add_right h₃.2 v583      _ < (2 * v * k₃ + 2 * v) + 2 * v := Nat.add_lt_add_left hvv _584      _ = 2 * v * (k₃ + 1 + 1) := by rw [round_step, round_step]585  · -- 2v k₃ ≤ 2N(u + u′) + v < (2Nu + v) + (2Nu′ + v) < (2v k₁ + 2v) + (2v k₂ + 2v) = 2v(k₁ + k₂ + 2)586    calc 2 * v * k₃ ≤ 2 * N * (u + u') + v := h₃.1587      _ < (2 * N * (u + u') + v) + v := Nat.lt_add_of_pos_right hv588      _ = (2 * N * u + v) + (2 * N * u' + v) := by rw [hX]; exact (shuffle _ _ _).symm589      _ < (2 * v * k₁ + 2 * v) + (2 * v * k₂ + 2 * v) := Nat.add_lt_add h₁.2 h₂.2590      _ = 2 * v * (k₁ + k₂ + 1 + 1) := by591          rw [round_step, round_step, ← Nat.left_distrib, Nat.add_assoc k₁ 1 (k₂ + 1), Nat.add_comm 1 (k₂ + 1),592            ← Nat.add_assoc, ← Nat.add_assoc]593594end Frame595end Shell596end FRC597