Frame.lean — FrcCore

1import FrcCore.FrameCore23/-!4# FrcCore.Frame — the frame's arithmetic (the frame theme)56The frame itself, `IsPrimitive`, `Generates`, `Frame`, the half-period, the quarter-turn, the orientation classes and7the Euler identity, is `FrameCore.lean` (split off by task LM24, every name unchanged); this file imports it, so a module8that imports `Frame` sees both.910Since the ledger migration (task LM17) it holds the frame's arithmetic from 1-algebra (scale periodicity, the affine11frame, the window law and its read-backs, `ofNat_add`, `ofNat_mul`, the quarter-turn and the fourth roots, the meridian12involution, the complex chart, Theorem approx, `natCount`), `ofNat_self` and `ofNat_add_self` (from 13-epi), the root pair13(from 10-dimensions) and the counting lemmas of 20-rh, all under their old names in `FRC.Shell` and `FRC.Shell.Frame`.14The bounded quantifiers' deciders (from 10-dimensions and 20-rh) are in `Series.lean` since task LM22. No axioms.15-/1617namespace FRC18namespace Shell1920variable {p : Nat} [Pos p]2122namespace Frame23variable {κ : Nat} {g : Shell p}2425/-! ## The frame's arithmetic (moved from 1-algebra by the ledger migration, task LM17) -/2627/-- 1:D4 (Lemma 2 of 1-algebra, scale periodicity) — the residue grid repeats with the period `p − 1`28of the drive: `g^{n + (p−1)} = g^n`, hence `x·g^{n + (p−1)} = x·g^n` for every `x`. -/29theorem scale_periodic (F : Frame p κ g) (x : Shell p) (n : Nat) :30    x * g ^ (n + (p - 1)) = x * g ^ n := by31  rw [pow_add, F.pow_n, mul_one]3233/-- The affine frame `(a, b)` of 1-algebra (Definition 2): the transported product34`x ⊗ z := a + b·((x − a)/b)·((z − a)/b)`, written with `y` the inverse of `b`. -/35def affineMul (a b y x z : Shell p) : Shell p := a + b * ((x + -a) * y) * ((z + -a) * y)3637/-- 1:B4 (Definition 2 of 1-algebra) — in the affine frame `(a, b)` the multiplicative unit38is `a + b`, not `b`: `(a + b) ⊗ z = z` for every `z`. -/39theorem affine_frame_unit {a b y : Shell p} (hby : b * y = 1) (z : Shell p) :40    affineMul a b y (a + b) z = z := by41  unfold affineMul42  have e1 : a + b + -a = b := by rw [add_comm a b, add_assoc, add_neg, add_zero]43  rw [e1, hby, mul_one, mul_left_comm b, hby, mul_one, add_comm z (-a), ← add_assoc, add_neg, zero_add]4445/-- 1:D2 (the window law, injectivity) — two window integers `x, y ≤ H` with `2H < p` that read as the same46residue are equal: `ofNat x = ofNat y → x = y`. (Both are below `p`, so the residues are the integers.) -/47theorem window_injective {H x y : Nat} (hH : 2 * H < p) (hx : x ≤ H) (hy : y ≤ H)48    (h : (ofNat x : Shell p) = ofNat y) : x = y := by49  have hxp : x < p := Nat.lt_of_le_of_lt hx (Nat.lt_of_le_of_lt (Nat.le_add_left H H) (Nat.two_mul H ▸ hH))50  have hyp : y < p := Nat.lt_of_le_of_lt hy (Nat.lt_of_le_of_lt (Nat.le_add_left H H) (Nat.two_mul H ▸ hH))51  have := val_injective h52  rw [val_ofNat, val_ofNat, FRC.Nat.mod_eq_of_lt hxp, FRC.Nat.mod_eq_of_lt hyp] at this53  exact this5455theorem ofNat_add (x y : Nat) : (ofNat x : Shell p) + ofNat y = ofNat (x + y) :=56  ext (by rw [val_add, val_ofNat, val_ofNat, val_ofNat, FRC.Nat.mod_add_mod _ _ _ hp, FRC.Nat.add_mod_mod _ _ _ hp])5758theorem ofNat_mul (x y : Nat) : (ofNat x : Shell p) * ofNat y = ofNat (x * y) :=59  ext (by rw [val_mul, val_ofNat, val_ofNat, val_ofNat, FRC.Nat.mod_mul_mod _ _ _ hp, FRC.Nat.mul_mod_mod _ _ _ hp])6061/-- `p ≡ 0` on the shell. -/62theorem ofNat_self : (ofNat p : Shell p) = 0 := by63  apply ext; show p % p = 0; exact FRC.Nat.mod_self p Pos.pos6465theorem ofNat_add_self (n : Nat) : (ofNat (n + p) : Shell p) = ofNat n := by66  rw [← ofNat_add, ofNat_self, add_zero]6768/-- 1:D2, the read-back of sums: for `x, y ≤ H` and `4H < p`, the residue of `x + y` determines the integer69`x + y` among the integers `z ≤ 2H`. -/70theorem window_add_readback {H x y z : Nat} (hH : 2 * (2 * H) < p) (hx : x ≤ H) (hy : y ≤ H) (hz : z ≤ 2 * H)71    (h : (ofNat x : Shell p) + ofNat y = ofNat z) : x + y = z := by72  rw [ofNat_add] at h73  exact window_injective hH (by rw [Nat.two_mul]; exact Nat.add_le_add hx hy) hz h7475/-- 1:D2, the read-back of products: for `x, y ≤ H` and `2H² < p`, the residue of `x·y` determines the integer76`x·y` among the integers `z ≤ H²`. -/77theorem window_mul_readback {H x y z : Nat} (hH : 2 * (H * H) < p) (hx : x ≤ H) (hy : y ≤ H) (hz : z ≤ H * H)78    (h : (ofNat x : Shell p) * ofNat y = ofNat z) : x * y = z := by79  rw [ofNat_mul] at h80  exact window_injective hH (Nat.mul_le_mul hx hy) hz h8182/-- 1:D2, the signed window: `x` and `−y` (`x, y ≤ H`, `2H < p`) read as the same residue only when both83are zero — the window's positive and negative halves do not overlap. -/84theorem window_signed {H x y : Nat} (hH : 2 * H < p) (hx : x ≤ H) (hy : y ≤ H)85    (h : (ofNat x : Shell p) = -(ofNat y)) : x = 0 ∧ y = 0 := by86  have hxp : x < p := Nat.lt_of_le_of_lt hx (Nat.lt_of_le_of_lt (Nat.le_add_left H H) (Nat.two_mul H ▸ hH))87  have hyp : y < p := Nat.lt_of_le_of_lt hy (Nat.lt_of_le_of_lt (Nat.le_add_left H H) (Nat.two_mul H ▸ hH))88  have hv := val_injective h89  rw [val_ofNat, val_neg, val_ofNat, FRC.Nat.mod_eq_of_lt hxp, FRC.Nat.mod_eq_of_lt hyp] at hv90  -- hv : x = (p - y) % p91  match Nat.decEq y 0 with92  | .isTrue hy0 =>93    rw [hy0, Nat.sub_zero, FRC.Nat.mod_self p hp] at hv94    exact ⟨hv, hy0⟩95  | .isFalse hy0 =>96    have hpy : p - y < p := Nat.sub_lt hp (Nat.pos_of_ne_zero hy0)97    rw [FRC.Nat.mod_eq_of_lt hpy] at hv98    -- x = p − y with x ≤ H, y ≤ H gives p = x + y ≤ 2H < p99    have : p = x + y := by rw [hv, FRC.Nat.sub_add_cancel (Nat.le_of_lt hyp)]100    have hle : x + y ≤ 2 * H := by rw [Nat.two_mul]; exact Nat.add_le_add hx hy101    exact absurd (Nat.lt_of_le_of_lt (this ▸ hle) hH) (Nat.lt_irrefl p)102103/-- 1:B2 (Theorem 1, existence clause) — a quarter-turn `u` with `u² = −1` exists on every shell. -/104theorem quarter_turn_exists (F : Frame p κ g) : ∃ u : Shell p, u * u = -1 :=105  ⟨quarterTurn g κ, F.quarter_turn_sq⟩106107/-- 1:B2 (Theorem 1, the structural set) — the fourth roots of unity are exactly `1, −1, i, −i`. -/108theorem fourth_roots (F : Frame p κ g) (x : Shell p) :109    x ^ 4 = 1 ↔ x = 1 ∨ x = -1 ∨ x = quarterTurn g κ ∨ x = -(quarterTurn g κ) := by110  have h4 : x ^ 4 = (x * x) * (x * x) := by111    rw [show (4 : Nat) = 2 * 2 from rfl, pow_mul, pow_two, pow_two]112  have hi := F.quarter_turn_sq113  constructor114  · intro h115    rw [h4] at h116    match F.sq_eq_one h with117    | .inl e => match F.sq_eq_one e with118      | .inl e1 => exact .inl e1119      | .inr e1 => exact .inr (.inl e1)120    | .inr e =>121      -- x² = −1 = i²: (x + −i)(x + i) = 0122      have e2 : (x + -(quarterTurn g κ)) * (x + quarterTurn g κ) = 0 := by123        rw [right_distrib, left_distrib, left_distrib, e, ← neg_mul, ← neg_mul, hi, neg_neg, mul_comm (quarterTurn g κ) x]124        rw [add_assoc, ← add_assoc (x * quarterTurn g κ), add_neg, zero_add, neg_add]125      match F.mul_eq_zero e2 with126      | .inl e3 => exact .inr (.inr (.inl (by127          calc x = x + 0 := (add_zero x).symm128            _ = x + (-(quarterTurn g κ) + quarterTurn g κ) := by rw [neg_add]129            _ = (x + -(quarterTurn g κ)) + quarterTurn g κ := (add_assoc _ _ _).symm130            _ = quarterTurn g κ := by rw [e3, zero_add])))131      | .inr e3 => exact .inr (.inr (.inr (eq_neg_of_add_eq_zero e3)))132  · intro h133    match h with134    | .inl e => rw [e, one_pow]135    | .inr (.inl e) => rw [h4, e, neg_mul_neg, one_mul, one_mul]136    | .inr (.inr (.inl e)) => rw [h4, e, hi, neg_mul_neg, one_mul]137    | .inr (.inr (.inr e)) => rw [h4, e, neg_mul_neg, hi, neg_mul_neg, one_mul]138139/-- 1:C4 (Definition 5 (a)) — the meridian involution: `(−a)·g^{n + 2κ} = a·g^n`. -/140theorem meridian_involution (F : Frame p κ g) (a : Shell p) (n : Nat) :141    -a * g ^ (n + 2 * κ) = a * g ^ n := by142  rw [pow_add, F.half_period, mul_comm (g ^ n), ← mul_assoc, neg_mul_neg, mul_one]143144/-- The complex chart: pairs `(a, b)` read as `a + b·X` with `X² = −1`, multiplied as145`(a, b)(c, d) = (ac − bd, ad + bc)`. -/146def cmul (x y : Shell p × Shell p) : Shell p × Shell p :=147  (x.1 * y.1 + -(x.2 * y.2), x.1 * y.2 + x.2 * y.1)148149/-- 1:E2 (Proposition 5 reversed) — on a shell that already has a square root of `−1` the complex chart is150not a field: `(i, 1)·(−i, 1) = (0, 0)` with both factors nonzero (`X + i` and `X − i` are zero divisors). -/151theorem complex_chart_zero_divisor (F : Frame p κ g) :152    cmul (quarterTurn g κ, (1 : Shell p)) (-(quarterTurn g κ), 1) = (0, 0) ∧153    (quarterTurn g κ, (1 : Shell p)) ≠ (0, 0) ∧ (-(quarterTurn g κ), (1 : Shell p)) ≠ (0, 0) := by154  refine ⟨?_, fun h => F.one_ne_zero (congrArg Prod.snd h), fun h => F.one_ne_zero (congrArg Prod.snd h)⟩155  unfold cmul156  show (quarterTurn g κ * -(quarterTurn g κ) + -(1 * 1), quarterTurn g κ * 1 + 1 * -(quarterTurn g κ)) = (0, 0)157  rw [← mul_neg, F.quarter_turn_sq, neg_neg, one_mul, add_neg, mul_one, one_mul, add_neg]158159/-- 1:D6 (Theorem approx, the range at `p = 13`, `g = 2`): every grid point160`x / 2^n` with `x < 13` and `n ≥ 3` is at most `3/2` — as the integer statement `2x ≤ 3·2^n`. -/161theorem approx_obstruction (n x : Nat) (hn : 3 ≤ n) (hx : x < 13) : 2 * x ≤ 3 * 2 ^ n := by162  have h8 : 2 ^ 3 ≤ 2 ^ n := Nat.pow_le_pow_right (Nat.zero_lt_succ 1) hn163  have h1 : 2 * x ≤ 2 * 12 := Nat.mul_le_mul_left 2 (Nat.le_of_lt_succ hx)164  have h2 : 3 * 2 ^ 3 ≤ 3 * 2 ^ n := Nat.mul_le_mul_left 3 h8165  exact Nat.le_trans h1 h2166167/-- The number of `x < n` with `P x`, as a sum of `0`s and `1`s. -/168def natCount (P : Nat → Prop) [DecidablePred P] : Nat → Nat169  | 0 => 0170  | n + 1 => natCount P n + if P n then 1 else 0171172theorem natCount_ne_zero (n : Nat) : natCount (fun x => x ≠ 0) (n + 1) = n := by173  induction n with174  | zero => rfl175  | succ n ih =>176    show natCount (fun x => x ≠ 0) (n + 1) + (if n + 1 ≠ 0 then 1 else 0) = n + 1177    rw [ih, ite_eq_left (Nat.succ_ne_zero n)]178179/-- 10:E4, 10:P2 — the root pair: if `x² = a` with `x ≠ 0` then `y² = a` iff `y = x` or `y = −x`, and `−x ≠ x`;180each quadratic defining congruence has exactly two roots on a framed Carrier. -/181theorem root_pair (F : Frame p κ g) (a x : Shell p) (hx : x * x = a) (hx0 : x ≠ 0) :182    (∀ y : Shell p, y * y = a ↔ (y = x ∨ y = -x)) ∧ -x ≠ x := by183  refine ⟨fun y => ⟨fun hy => ?_, fun hy => ?_⟩, fun h => hx0 (F.eq_zero_of_eq_neg h.symm)⟩184  · have h0 : (y + -x) * (y + x) = 0 := by185      rw [Shell.right_distrib, Shell.left_distrib, Shell.left_distrib, ← Shell.neg_mul, ← Shell.neg_mul,186        Shell.mul_comm y x, Shell.add_assoc, ← Shell.add_assoc (x * y), Shell.add_neg, Shell.zero_add,187        hy, hx, Shell.add_neg]188    rcases F.mul_eq_zero h0 with h | h189    · left; exact (Shell.eq_neg_of_add_eq_zero h).trans (Shell.neg_neg x)190    · right; exact Shell.eq_neg_of_add_eq_zero h191  · rcases hy with rfl | rfl192    · exact hx193    · rw [Shell.neg_mul_neg]; exact hx194195/-- Counting where nothing satisfies the predicate. -/196theorem natCount_eq_zero (P : Nat → Prop) [DecidablePred P] : ∀ n, (∀ x, x < n → ¬ P x) → natCount P n = 0197  | 0, _ => rfl198  | n + 1, h => by199    show natCount P n + (if P n then 1 else 0) = 0200    rw [natCount_eq_zero P n (fun x hx => h x (Nat.lt_succ_of_lt hx)), ite_eq_right (h n (Nat.lt_succ_self n))]201202/-- Counting through an equivalent predicate. -/203theorem natCount_congr (P Q : Nat → Prop) [DecidablePred P] [DecidablePred Q] :204    ∀ n, (∀ x, x < n → (P x ↔ Q x)) → natCount P n = natCount Q n205  | 0, _ => rfl206  | n + 1, h => by207    show natCount P n + (if P n then 1 else 0) = natCount Q n + (if Q n then 1 else 0)208    rw [natCount_congr P Q n (fun x hx => h x (Nat.lt_succ_of_lt hx))]209    have e := h n (Nat.lt_succ_self n)210    match (inferInstance : Decidable (Q n)) with211    | isTrue hq => rw [ite_eq_left hq, ite_eq_left (e.2 hq)]212    | isFalse hq => rw [ite_eq_right hq, ite_eq_right (fun hp => hq (e.1 hp))]213214end Frame215end Shell216end FRC217