Theme/Quantum.lean — FrcCore

1import FrcCore.Theme.Field2import FrcCore.Theme.Logic3import FrcCore.Theme.Drive45/-!6# FrcCore.Theme.Quantum — the quantum theme: the unequal-cycle composite (ledger migration, task LM28)78The master's block F where its rows are exact. A composite of `m` parts, part `j` of registration period `n j > 0`,9driven jointly one step per chronon (00:F2, 22:C26, 37-sim's composite gate):1011* the joint recurrence: the chronons at which every part returns are exactly the multiples of one period `T > 0`, the12  least common multiple of the parts' periods (`joint_recurrence`, `joint_least`);13* each pair's conserved offset lives on the gcd cycle: for two parts of periods `a`, `b` with joint period `T`, the14  number `g` with `g T = a b` divides both, and two joint states lie on one orbit of the drive exactly when their15  offsets agree modulo `g` (`pair_offset`): the orbits are the quotient `A/⟨v⟩ ≅ ℤ/g`;16* dephasing over the product period is exact: on every prime shell, a character of the composite that the drive moves17  (`Π ζ_j ≠ 1`) sums to zero over every joint recurrence, the product of the periods among them (`dephasing`).1819No axioms.20-/2122namespace FRC.Quantum2324open FRC.Shell2526/-! ## Arithmetic of remainders -/2728theorem mod_zero_of_eq_mul {t a q : Nat} (ha : 0 < a) (h : t = a * q) : t % a = 0 :=29  FRC.Nat.mod_unique ha (by rw [h, Nat.add_zero])3031theorem eq_mul_of_mod_zero {t a : Nat} (ha : 0 < a) (h : t % a = 0) : ∃ q, t = a * q :=32  match FRC.Nat.mod_spec a ha t with33  | ⟨q, hq⟩ => ⟨q, by rw [hq, h, Nat.add_zero]⟩3435theorem mul_mod_zero {t a : Nat} (ha : 0 < a) (h : t % a = 0) (k : Nat) : (t * k) % a = 0 :=36  match eq_mul_of_mod_zero ha h with37  | ⟨q, hq⟩ => mod_zero_of_eq_mul ha (by rw [hq, FRC.Nat.mul_assoc])3839/-- A summand that keeps the remainder is a multiple: `(u + v) % b = u % b → v % b = 0`. -/40theorem mod_of_add_mod {u v b : Nat} (hb : 0 < b) (h : (u + v) % b = u % b) : v % b = 0 := by41  have hr := Nat.mod_lt u hb42  have hs := Nat.mod_lt v hb43  rw [FRC.Nat.add_mod u v b hb] at h44  match Nat.lt_or_ge (u % b + v % b) b with45  | .inl hlt =>46    rw [FRC.Nat.mod_eq_of_lt hlt] at h47    exact FRC.Nat.add_left_cancel (h.trans (Nat.add_zero _).symm)48  | .inr hge =>49    rw [FRC.Nat.mod_eq_sub_mod hb hge, FRC.Nat.mod_eq_of_lt (FRC.Nat.sub_lt_of_lt_add (Nat.add_lt_add hr hs) hge)] at h50    have e : u % b + v % b = u % b + b := by51      calc u % b + v % b = (u % b + v % b - b) + b := (FRC.Nat.sub_add_cancel hge).symm52        _ = u % b + b := by rw [h]53    exact absurd hs (by rw [FRC.Nat.add_left_cancel e]; exact Nat.lt_irrefl b)5455/-- Remainders modulo a divisor: `g ∣ a` gives `(n % a) % g = n % g`. -/56theorem mod_mod_of_dvd {n a g : Nat} (hg : 0 < g) (ha : 0 < a) (h : a % g = 0) : n % a % g = n % g := by57  match FRC.Nat.mod_spec a ha n, eq_mul_of_mod_zero hg h with58  | ⟨q, hq⟩, ⟨u, hu⟩ =>59    calc n % a % g = (g * (u * q) + n % a) % g := (FRC.Nat.add_mul_mod_self_left _ _ _ hg).symm60      _ = n % g := by rw [← FRC.Nat.mul_assoc, ← hu, ← hq]6162/-- Cancelling a common summand under a remainder. -/63theorem mod_add_left_cancel {x u v g : Nat} (hg : 0 < g) (h : (x + u) % g = (x + v) % g) : u % g = v % g := by64  have e1 : (x + u) % g = (x % g + u % g) % g := FRC.Nat.add_mod _ _ _ hg65  have e2 : (x + v) % g = (x % g + v % g) % g := FRC.Nat.add_mod _ _ _ hg66  have key : ∀ w, ((g - x % g) + (x + w)) % g = w % g := fun w => by67    have hx := Nat.mod_lt x hg68    match FRC.Nat.mod_spec g hg x with69    | ⟨q, hq⟩ =>70      calc ((g - x % g) + (x + w)) % g = (g * (q + 1) + w) % g := by71            congr 172            calc (g - x % g) + (x + w) = (g - x % g) + (g * q + x % g + w) := by rw [← hq]73              _ = g * q + ((g - x % g) + x % g) + w := by74                rw [← Nat.add_assoc, Nat.add_comm (g - x % g) (g * q + x % g), Nat.add_assoc (g * q),75                  Nat.add_comm (x % g) (g - x % g), ← Nat.add_assoc (g * q)]76              _ = g * (q + 1) + w := by rw [FRC.Nat.sub_add_cancel (Nat.le_of_lt hx), Nat.mul_succ]77        _ = w % g := FRC.Nat.add_mul_mod_self_left _ _ _ hg78  rw [← key u, ← key v, FRC.Nat.add_mod (g - x % g) (x + u) g hg, FRC.Nat.add_mod (g - x % g) (x + v) g hg, h]7980theorem lt_of_mul_lt_mul {g a b : Nat} (h : g * a < g * b) : a < b :=81  match Nat.lt_or_ge a b with82  | .inl hlt => hlt83  | .inr hge => absurd (Nat.lt_of_lt_of_le h (Nat.mul_le_mul_left g hge)) (Nat.lt_irrefl _)8485theorem sub_pos {a b : Nat} (h : a < b) : 0 < b - a :=86  Nat.pos_of_ne_zero (fun e => by87    have := FRC.Nat.sub_add_cancel (Nat.le_of_lt h)88    rw [e, Nat.zero_add] at this89    exact Nat.lt_irrefl a (this ▸ h))9091/-! ## The joint recurrence (00:F2) -/9293/-- All `m` parts, of periods `n j`, are back at chronon `t`. -/94def Joint (n : Nat → Nat) (m t : Nat) : Prop := ∀ j, j < m → t % n j = 09596instance (n : Nat → Nat) (m t : Nat) : Decidable (Joint n m t) := FRC.Shell.decForallLT _ m9798/-- The product of the periods. -/99def prodN (n : Nat → Nat) : Nat → Nat100  | 0 => 1101  | m + 1 => prodN n m * n m102103theorem prodN_pos (n : Nat → Nat) (hn : ∀ j, 0 < n j) : ∀ m, 0 < prodN n m104  | 0 => Nat.zero_lt_succ 0105  | m + 1 => Nat.mul_pos (prodN_pos n hn m) (hn m)106107theorem prodN_joint (n : Nat → Nat) (hn : ∀ j, 0 < n j) : ∀ m, Joint n m (prodN n m)108  | 0 => fun _ h => absurd h (Nat.not_lt_zero _)109  | m + 1 => fun j hj => match Nat.lt_or_ge j m with110    | .inl hlt => by111      show (prodN n m * n m) % n j = 0112      exact mul_mod_zero (hn j) (prodN_joint n hn m j hlt) _113    | .inr hge => by114      have e : j = m := Nat.le_antisymm (Nat.le_of_lt_succ hj) hge115      rw [e]116      exact mod_zero_of_eq_mul (hn m) (Nat.mul_comm _ _)117118/-- 00:F2, 22:C26, 22:C10, 22:C20 — the joint recurrence of an unequal-cycle composite, found below a common multiple `L > 0` of the119periods (on a shell, a joint return below `Ω`): the chronons at which all `m` parts return are exactly the multiples of120one period `T`, `0 < T ≤ L`, which divides `L`. The search never passes `L` (Q20). -/121theorem joint_recurrence (n : Nat → Nat) (hn : ∀ j, 0 < n j) (m L : Nat) (hL : 0 < L) (hLj : Joint n m L) :122    ∃ T, T ≤ L ∧ 0 < T ∧ Joint n m T ∧ (∀ t, Joint n m t ↔ t % T = 0) ∧ L % T = 0 := by123  let P : Nat → Bool := fun t => decide (0 < t ∧ Joint n m t)124  have hP : P L = true := decide_eq_true ⟨hL, hLj⟩125  match FRC.Logic.leastBelow_some P (L + 1) L (Nat.lt_succ_self _) hP with126  | ⟨T, hT⟩ =>127    have hs := FRC.Logic.leastBelow_spec P _ T hT128    have hT' : 0 < T ∧ Joint n m T := of_decide_eq_true hs.2.1129    have hiff : ∀ t, Joint n m t ↔ t % T = 0 := fun t => by130      constructor131      · intro ht132        match FRC.Nat.mod_spec T hT'.1 t with133        | ⟨q, hq⟩ =>134          have hr : Joint n m (t % T) := fun j hj => by135            have h1 : (T * q + t % T) % n j = (T * q) % n j := by136              rw [← hq, ht j hj]137              exact (mul_mod_zero (hn j) (hT'.2 j hj) q).symm138            exact mod_of_add_mod (hn j) h1139          exact match Nat.decEq (t % T) 0 with140            | isTrue e => e141            | isFalse e =>142              have ht' : P (t % T) = true := decide_eq_true ⟨Nat.pos_of_ne_zero e, hr⟩143              Bool.noConfusion (ht'.symm.trans (hs.2.2 (t % T) (Nat.mod_lt t hT'.1)))144      · intro ht j hj145        match eq_mul_of_mod_zero hT'.1 ht with146        | ⟨q, hq⟩ => rw [hq]; exact mul_mod_zero (hn j) (hT'.2 j hj) q147    exact ⟨T, Nat.le_of_lt_succ hs.1, hT'.1, hT'.2, hiff, (hiff _).1 hLj⟩148149/-- 22:C26 — the joint period is the least common multiple: no positive joint return comes earlier. -/150theorem joint_least {n : Nat → Nat} {m T : Nat} (hiff : ∀ t, Joint n m t ↔ t % T = 0) (hT : 0 < T) :151    ∀ t, 0 < t → Joint n m t → T ≤ t := fun t ht hj =>152  match eq_mul_of_mod_zero hT ((hiff t).1 hj) with153  | ⟨q, hq⟩ => by154    rw [hq]155    match q with156    | 0 => rw [Nat.mul_zero] at hq; exact absurd (hq ▸ ht) (Nat.lt_irrefl 0)157    | q + 1 => rw [Nat.mul_succ]; exact Nat.le_add_left T _158159/-! ## The conserved offset on the gcd cycle (00:F2) -/160161/-- The last `j < N` with `g j = w` (the index of a multiple of `g`). -/162def mulIdx (g w : Nat) : Nat → Nat163  | 0 => 0164  | N + 1 => if g * N = w then N else mulIdx g w N165166theorem mulIdx_spec (g w j₀ : Nat) (h : g * j₀ = w) : ∀ N, j₀ < N → g * mulIdx g w N = w ∧ mulIdx g w N < N167  | 0, hj => absurd hj (Nat.not_lt_zero _)168  | N + 1, hj => by169    show g * (if g * N = w then N else mulIdx g w N) = w ∧ (if g * N = w then N else mulIdx g w N) < N + 1170    match (inferInstance : Decidable (g * N = w)) with171    | isTrue e => rw [ite_eq_left e]; exact ⟨e, Nat.lt_succ_self N⟩172    | isFalse e =>173      rw [ite_eq_right e]174      have hlt : j₀ < N := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (fun e' => e (e' ▸ h))175      have ih := mulIdx_spec g w j₀ h N hlt176      exact ⟨ih.1, Nat.lt_succ_of_lt ih.2⟩177178/-- 00:F2, 22:C26, 22:C15, 22:C18, 22:P3 — two parts of periods `a`, `b` with joint period `T` (a common multiple, and no positive common179multiple below it): the number `g` with `g T = a b` divides both periods, and every common divisor divides it (`g` is180the gcd); the joint drive carries `(x, y)` to `(x', y')` within one joint period exactly when the offsets agree modulo181`g` — the conserved offset on the gcd cycle, the orbits the quotient `A/⟨v⟩ ≅ ℤ/g`. -/182theorem pair_offset {a b T : Nat} (ha : 0 < a) (hb : 0 < b) (hT : 0 < T) (hTa : T % a = 0) (hTb : T % b = 0)183    (hleast : ∀ t, 0 < t → t < T → ¬ (t % a = 0 ∧ t % b = 0)) :184    ∃ g, g ≤ a ∧ 0 < g ∧ g * T = a * b ∧ a % g = 0 ∧ b % g = 0 ∧ (∀ e, 0 < e → a % e = 0 → b % e = 0 → g % e = 0) ∧185      ∀ x y x' y', x < a → y < b → x' < a → y' < b →186        ((∃ t, t < T ∧ (x + t) % a = x' ∧ (y + t) % b = y') ↔ (x + y') % g = (x' + y) % g) := by187  -- every common multiple is a multiple of `T`188  have hcm : ∀ t, t % a = 0 → t % b = 0 → t % T = 0 := fun t hta htb => by189    obtain ⟨q, hq⟩ := FRC.Nat.mod_spec T hT t190    have hr : ∀ c, 0 < c → T % c = 0 → t % c = 0 → (t % T) % c = 0 := fun c hc hTc htc =>191      mod_of_add_mod hc (by rw [← hq, htc]; exact (mul_mod_zero hc hTc q).symm)192    match Nat.decEq (t % T) 0 with193    | isTrue e => exact e194    | isFalse e => exact absurd ⟨hr a ha hTa hta, hr b hb hTb htb⟩ (hleast _ (Nat.pos_of_ne_zero e) (Nat.mod_lt t hT))195  obtain ⟨ua, hua⟩ := eq_mul_of_mod_zero ha hTa196  obtain ⟨ub, hub⟩ := eq_mul_of_mod_zero hb hTb197  have hab : (a * b) % T = 0 := hcm (a * b) (mod_zero_of_eq_mul ha rfl) (mod_zero_of_eq_mul hb (Nat.mul_comm a b))198  obtain ⟨g, hg⟩ := eq_mul_of_mod_zero hT hab199  have hgT : g * T = a * b := by rw [Nat.mul_comm, ← hg]200  have hg0 : 0 < g := Nat.pos_of_ne_zero (fun e => by201    rw [e, Nat.mul_zero] at hg; exact Nat.ne_of_gt (Nat.mul_pos ha hb) hg)202  -- `g ua = b` and `g ub = a`203  have hgb : b = g * ua := Nat.eq_of_mul_eq_mul_left ha (by204    calc a * b = g * T := hgT.symm205      _ = a * (g * ua) := by rw [hua, Nat.mul_left_comm])206  have hga : a = g * ub := Nat.eq_of_mul_eq_mul_left hb (by207    calc b * a = g * T := by rw [Nat.mul_comm, hgT]208      _ = b * (g * ub) := by rw [hub, Nat.mul_left_comm])209  have hag : a % g = 0 := mod_zero_of_eq_mul hg0 hga210  have hbg : b % g = 0 := mod_zero_of_eq_mul hg0 hgb211  have hgle : g ≤ a := by212    match ub, hga with213    | 0, e => rw [Nat.mul_zero] at e; rw [e] at ha; exact absurd ha (Nat.lt_irrefl 0)214    | u + 1, e => rw [e, Nat.mul_succ]; exact Nat.le_add_left g (g * u)215  -- `g` is the greatest common divisor: a common divisor `e` gives the common multiple `e a' b'`216  have hgcd : ∀ e, 0 < e → a % e = 0 → b % e = 0 → g % e = 0 := fun e he hae hbe => by217    obtain ⟨a', ha'⟩ := eq_mul_of_mod_zero he hae218    obtain ⟨b', hb'⟩ := eq_mul_of_mod_zero he hbe219    have hMa : (e * a' * b') % a = 0 := mod_zero_of_eq_mul ha (by rw [ha'])220    have hMb : (e * a' * b') % b = 0 :=221      mod_zero_of_eq_mul hb (by rw [hb', FRC.Nat.mul_assoc, Nat.mul_comm a' b', ← FRC.Nat.mul_assoc])222    obtain ⟨c, hc⟩ := eq_mul_of_mod_zero hT (hcm _ hMa hMb)223    have e1 : g * T = (e * c) * T :=224      calc g * T = a * b := hgT225        _ = e * (e * a' * b') := by226          rw [ha', hb', FRC.Nat.mul_assoc e a' (e * b'), FRC.Nat.mul_left_comm a' e b', FRC.Nat.mul_assoc e a' b']227        _ = e * (T * c) := by rw [hc]228        _ = (e * c) * T := by rw [Nat.mul_comm T c, ← FRC.Nat.mul_assoc]229    exact mod_zero_of_eq_mul he (Nat.eq_of_mul_eq_mul_right hT e1)230  refine ⟨g, hgle, hg0, hgT, hag, hbg, hgcd, fun x y x' y' hx hy hx' hy' => ⟨?_, ?_⟩⟩231  · -- the offset is conserved232    rintro ⟨t, _, ht1, ht2⟩233    calc (x + y') % g = (x + (y + t) % b) % g := by rw [ht2]234      _ = (x + (y + t) % b % g) % g := (FRC.Nat.add_mod_mod _ _ _ hg0).symm235      _ = (x + (y + t)) % g := by rw [mod_mod_of_dvd hg0 hb hbg, FRC.Nat.add_mod_mod _ _ _ hg0]236      _ = ((x + t) + y) % g := by rw [← Nat.add_assoc, Nat.add_right_comm]237      _ = ((x + t) % a % g + y) % g := by rw [mod_mod_of_dvd hg0 ha hag, FRC.Nat.mod_add_mod _ _ _ hg0]238      _ = (x' + y) % g := by rw [FRC.Nat.mod_add_mod _ _ _ hg0, ht1]239  · -- the offset is complete: the pigeonhole over one cycle of the second part240    intro hoff241    let d := (x' + (a - x)) % a242    have hxd : (x + d) % a = x' := by243      show (x + (x' + (a - x)) % a) % a = x'244      rw [FRC.Nat.add_mod_mod _ _ _ ha]245      calc (x + (x' + (a - x))) % a = (a * 1 + x') % a := by246            congr 1247            rw [Nat.add_left_comm, FRC.Nat.add_sub_of_le (Nat.le_of_lt hx), Nat.mul_one, Nat.add_comm]248        _ = x' := by rw [FRC.Nat.add_mul_mod_self_left _ _ _ ha, FRC.Nat.mod_eq_of_lt hx']249    -- `y' ≡ y + d (mod g)`250    have hyd : y' % g = (y + d) % g := by251      have h1 : (x + y') % g = (x + (d + y)) % g := by252        calc (x + y') % g = (x' + y) % g := hoff253          _ = ((x + d) % a % g + y) % g := by rw [hxd, FRC.Nat.mod_add_mod _ _ _ hg0]254          _ = (x + (d + y)) % g := by rw [mod_mod_of_dvd hg0 ha hag, FRC.Nat.mod_add_mod _ _ _ hg0, Nat.add_assoc]255      rw [mod_add_left_cancel hg0 h1, Nat.add_comm]256    -- the residues `w k = (y + d + a k) % b` all lie in the class of `y'` modulo `g`257    let w : Nat → Nat := fun k => (y + d + a * k) % b258    let r₀ := y' % g259    have hwg : ∀ k, w k % g = r₀ := fun k => by260      show (y + d + a * k) % b % g = y' % g261      rw [mod_mod_of_dvd hg0 hb hbg, FRC.Nat.add_mod _ _ _ hg0, mul_mod_zero hg0 hag k, Nat.add_zero,262        FRC.Nat.mod_mod _ _ hg0, hyd]263    -- the index of a residue `v < b` of that class: `v = g j + r₀`, `j < ua`264    have hidx : ∀ v, v < b → v % g = r₀ → g * mulIdx g (v - r₀) ua = v - r₀ ∧ mulIdx g (v - r₀) ua < ua ∧ r₀ ≤ v := by265      intro v hv hvg266      obtain ⟨q, hq⟩ := FRC.Nat.mod_spec g hg0 v267      rw [hvg] at hq268      have hsub : v - r₀ = g * q := by rw [hq, FRC.Nat.add_sub_cancel]269      have hqlt : q < ua := lt_of_mul_lt_mul (Nat.lt_of_le_of_lt (hq ▸ Nat.le_add_right (g * q) r₀ : g * q ≤ v)270        (hgb ▸ hv))271      have := mulIdx_spec g (v - r₀) q hsub.symm ua hqlt272      exact ⟨this.1, this.2, hq ▸ Nat.le_add_left r₀ (g * q)⟩273    let S : Nat → Nat := fun k => mulIdx g (w k - r₀) ua274    have hS : ∀ k, g * S k = w k - r₀ ∧ S k < ua ∧ r₀ ≤ w k := fun k => hidx (w k) (Nat.mod_lt _ hb) (hwg k)275    -- the residues are distinct over one cycle of length `ua`276    have key : ∀ k₁ k₂, k₁ < k₂ → k₂ < ua → w k₁ ≠ w k₂ := fun k₁ k₂ hlt hk e => by277      have h1 : (y + d + a * k₁ + a * (k₂ - k₁)) % b = (y + d + a * k₁) % b := by278        rw [Nat.add_assoc, ← Nat.mul_add, FRC.Nat.add_sub_of_le (Nat.le_of_lt hlt)]; exact e.symm279      have h2 : (a * (k₂ - k₁)) % b = 0 := mod_of_add_mod hb h1280      have h3 : (a * (k₂ - k₁)) % T = 0 := hcm _ (mod_zero_of_eq_mul ha rfl) h2281      obtain ⟨q, hq⟩ := eq_mul_of_mod_zero hT h3282      rw [hua, FRC.Nat.mul_assoc] at hq283      have h4 : k₂ - k₁ = ua * q := Nat.eq_of_mul_eq_mul_left ha hq284      have h5 : 0 < k₂ - k₁ := sub_pos hlt285      have h6 : k₂ - k₁ < ua := Nat.lt_of_le_of_lt (Nat.sub_le k₂ k₁) hk286      match q with287      | 0 => rw [h4, Nat.mul_zero] at h5; exact Nat.lt_irrefl 0 h5288      | q + 1 => rw [h4, Nat.mul_succ] at h6; exact Nat.lt_irrefl _ (Nat.lt_of_le_of_lt (Nat.le_add_left ua _) h6)289    have hw_inj : ∀ k₁ k₂, k₁ < ua → k₂ < ua → w k₁ = w k₂ → k₁ = k₂ := fun k₁ k₂ h1 h2 ew =>290      match Nat.lt_or_ge k₁ k₂ with291      | .inl hlt => absurd ew (key k₁ k₂ hlt h2)292      | .inr hge => match Nat.lt_or_ge k₂ k₁ with293        | .inl hlt => absurd ew.symm (key k₂ k₁ hlt h1)294        | .inr hge' => Nat.le_antisymm hge' hge295    have hinj : ∀ k₁ k₂, k₁ < ua → k₂ < ua → S k₁ = S k₂ → k₁ = k₂ := fun k₁ k₂ h1 h2 e =>296      hw_inj k₁ k₂ h1 h2 (by297        rw [← FRC.Nat.sub_add_cancel (hS k₁).2.2, ← FRC.Nat.sub_add_cancel (hS k₂).2.2, ← (hS k₁).1, ← (hS k₂).1, e])298    have hy'g := hidx y' hy' rfl299    obtain ⟨k, hku, hk⟩ := FRC.Logic.inj_onto ua S (fun k _ => (hS k).2.1) hinj (mulIdx g (y' - r₀) ua) hy'g.2.1300    have hwk : w k = y' := by301      rw [← FRC.Nat.sub_add_cancel (hS k).2.2, ← FRC.Nat.sub_add_cancel hy'g.2.2, ← (hS k).1, ← hy'g.1, hk]302    have hdT : d + a * k < T := by303      rw [hua]304      calc d + a * k < a + a * k := Nat.add_lt_add_right (Nat.mod_lt _ ha) (a * k)305        _ = a * (k + 1) := by rw [Nat.add_comm, Nat.mul_succ]306        _ ≤ a * ua := Nat.mul_le_mul_left a hku307    refine ⟨d + a * k, hdT, ?_, ?_⟩308    · rw [← Nat.add_assoc, Nat.add_comm (x + d), FRC.Nat.add_mul_mod_self_left _ _ _ ha, hxd]309    · rw [← Nat.add_assoc]; exact hwk310311/-! ## Dephasing over the product period (00:F2) -/312313section dephasing314variable {q : Nat} [Pos q]315316/-- Powers of a product: `(Π_j ζ_j)^t = Π_j ζ_j^t`. -/317theorem prodRange_pow (ζ : Nat → Shell q) (t : Nat) : ∀ m, prodRange (fun j => ζ j ^ t) m = (prodRange ζ m) ^ t318  | 0 => (one_pow t).symm319  | m + 1 => by320    show prodRange (fun j => ζ j ^ t) m * ζ m ^ t = (prodRange ζ m * ζ m) ^ t321    rw [prodRange_pow ζ t m, mul_pow]322323theorem prodRange_one : ∀ m, prodRange (fun _ => (1 : Shell q)) m = 1324  | 0 => rfl325  | m + 1 => by show prodRange (fun _ => (1 : Shell q)) m * 1 = 1; rw [prodRange_one m, mul_one]326327/-- 00:F2, 22:C26, 22:C7 — dephasing is exact: on a prime shell `q`, a character `χ(x) = Π_j ζ_j^{x_j}` of the composite328(`ζ_j^{n_j} = 1`) that the drive moves (`χ(v) = Π_j ζ_j ≠ 1`) sums to zero along the drive, `Σ_{t<M} χ(t v) = 0`, over329every joint recurrence `M`, the product of the periods among them. -/330theorem dephasing (hq : FRC.Nat.isPrime q) (n : Nat → Nat) (hn : ∀ j, 0 < n j) (m : Nat) (ζ : Nat → Shell q)331    (hζ : ∀ j, j < m → ζ j ^ n j = 1) (hχ : prodRange ζ m ≠ 1) (M : Nat) (hM : Joint n m M) :332    sumRange (fun t => prodRange (fun j => ζ j ^ t) m) M = 0 := by333  have e : ∀ t, t < M → prodRange (fun j => ζ j ^ t) m = (prodRange ζ m) ^ t := fun t _ => prodRange_pow ζ t m334  rw [sum_congr M e]335  have hz : (prodRange ζ m) ^ M = 1 := by336    rw [← prodRange_pow, prodRange_congr m (fun j hj => by337      obtain ⟨u, hu⟩ := eq_mul_of_mod_zero (hn j) (hM j hj)338      show ζ j ^ M = 1339      rw [hu, pow_mul, hζ j hj, one_pow]), prodRange_one]340  have hg := geom_sum_mul (prodRange ζ m) M341  rw [hz, add_neg] at hg342  match Prime.mul_eq_zero hq hg with343  | .inl h => exact h344  | .inr h => exact absurd (Prime.eq_of_sub_eq_zero h) hχ345346end dephasing347348349/-! ## The graded registration law (00:F5; 39-s173, rows B1–B5)350351An Object component of order `n` (a prime power `ℓᵃ` of the Object's faces `C_{q−1}`, `C_{q+1}`) registers in the352Subject `𝔽_p` at the depth `d = ord_n(p)`: `d = 1` absorbed into the register `C_{p−1}`, its image the unique `C_n`;353`d = 2` observable on the boost torus `C_{p+1}`, its home unique since `gcd(p − 1, p + 1) = 2`; deeper, beyond the354quadratic frame. The sign `−1` registers on both faces. A component is visible while `p^d < Ω`; on a tower with355`p² < Ω` and `Ω / p² < p` the cap is `2`, read without forming `p³` (Q20). The instances are decided by the kernel. -/356357section registration358variable {p : Nat} [Pos p]359360/-- 00:F5, absorbed (`d = 1`): a component `n ∣ p − 1` registers in `C_{p−1}` with its unique image `C_n`: some `x` has361order `n`, and every `y` with `yⁿ = 1` is a power `x^k`, `k < n` (the root bound of `Xⁿ − 1`). -/362theorem absorbed (hp : FRC.Nat.isPrime p) {n : Nat} (hn : 0 < n) (hd : n ∣ p - 1) :363    ∃ x : Shell p, x ≠ 0 ∧ Prime.HasOrder x n ∧ ∀ y : Shell p, y ^ n = 1 → ∃ k, k < n ∧ y = x ^ k := by364  have hp1 : 0 < p - 1 := by365    match p, hp.1 with366    | k + 2, _ => exact Nat.zero_lt_succ k367  obtain ⟨x, hx0, hx⟩ := Prime.exists_order_of_dvd hp n n (Nat.le_refl n) hn hd368  refine ⟨x, hx0, hx, fun y hy => ?_⟩369  match decExistsLT (fun k => y = x ^ k) n with370  | .isTrue h => exact h371  | .isFalse h =>372    exfalso373    have hdist : ∀ i j, i < n → j < n → x ^ i = x ^ j → i = j := fun i j hi hj e => by374      have key : ∀ {a b : Nat}, a ≤ b → b < n → x ^ a = x ^ b → a = b := fun {a b} hab hb e => by375        have e1 : x ^ a * x ^ (b - a) = x ^ a * 1 := by rw [← pow_add, FRC.Nat.add_sub_of_le hab, mul_one, e]376        have h1 := Prime.mul_left_cancel hp (Prime.pow_ne_zero hp hx0 a) e1377        match Nat.decEq (b - a) 0 with378        | .isTrue h0 => exact Nat.le_antisymm hab (Nat.le_of_sub_eq_zero h0)379        | .isFalse h0 => exact absurd h1 (hx.2.2 _ (Nat.lt_of_le_of_lt (Nat.sub_le b a) hb) (Nat.pos_of_ne_zero h0))380      match Nat.lt_or_ge i j with381      | .inl hlt => exact key (Nat.le_of_lt hlt) hj e382      | .inr hge => exact (key hge hi e.symm).symm383    let r : Nat → Shell p := fun i => if i < n then x ^ i else y384    have hr : ∀ i j, i ≤ n → j ≤ n → r i = r j → i = j := fun i j hi hj e => by385      change (if i < n then x ^ i else y) = (if j < n then x ^ j else y) at e386      match Nat.decLt i n, Nat.decLt j n with387      | .isTrue hi', .isTrue hj' =>388        have e' : x ^ i = x ^ j := by389          have := e; rw [ite_eq_left hi', ite_eq_left hj'] at this; exact this390        exact hdist i j hi' hj' e'391      | .isTrue hi', .isFalse hj' =>392        have e' : x ^ i = y := by393          have := e; rw [ite_eq_left hi', ite_eq_right hj'] at this; exact this394        exact absurd ⟨i, hi', e'.symm⟩ h395      | .isFalse hi', .isTrue hj' =>396        have e' : y = x ^ j := by397          have := e; rw [ite_eq_right hi', ite_eq_left hj'] at this; exact this398        exact absurd ⟨j, hj', e'⟩ h399      | .isFalse hi', .isFalse hj' =>400        exact (Nat.le_antisymm hi (Nat.not_lt.1 hi')).trans (Nat.le_antisymm hj (Nat.not_lt.1 hj')).symm401    have hroot : ∀ i, i ≤ n → Poly.eval (Poly.xn1 n : Poly p) n (r i) = 0 := fun i _ => by402      rw [Poly.eval_xn1 hn]403      match Nat.decLt i n with404      | .isTrue hi' =>405        show (if i < n then x ^ i else y) ^ n + -1 = 0406        rw [ite_eq_left hi', ← pow_mul, Nat.mul_comm, pow_mul, hx.2.1, one_pow, add_neg]407      | .isFalse hi' => show (if i < n then x ^ i else y) ^ n + -1 = 0; rw [ite_eq_right hi', hy, add_neg]408    have hz := Poly.root_bound_of (fun h => Prime.mul_eq_zero hp h) n (Poly.xn1 n) (Poly.xn1_bound n) r hr hroot n409    rw [Poly.xn1_top] at hz410    exact Prime.one_ne_zero hp hz411412/-- A prime power that divides `x y`, with the prime not dividing `y`, divides `x` (Euclid, by induction on the power). -/413theorem pow_mod_of_not_mod {l : Nat} (hl : FRC.Nat.isPrime l) {y : Nat} (hy : y % l ≠ 0) :414    ∀ a x : Nat, (x * y) % l ^ a = 0 → x % l ^ a = 0415  | 0, x, _ => FRC.Nat.mod_unique (Nat.zero_lt_succ 0) (by rw [Nat.pow_zero, Nat.one_mul, Nat.add_zero])416  | a + 1, x, h => by417    have hl0 : 0 < l := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hl.1418    have hpa : 0 < l ^ a := FRC.Nat.pos_pow_of_pos a hl0419    obtain ⟨c, hc⟩ := eq_mul_of_mod_zero (FRC.Nat.pos_pow_of_pos (a + 1) hl0) h420    have e1 : x * y = l * (l ^ a * c) := by rw [hc, Nat.pow_succ, Nat.mul_comm (l ^ a) l, FRC.Nat.mul_assoc]421    have hlx : x % l = 0 := (FRC.Nat.prime_mul_mod hl (mod_zero_of_eq_mul hl0 e1)).resolve_right hy422    obtain ⟨x', hx'⟩ := eq_mul_of_mod_zero hl0 hlx423    have e2 : x' * y = l ^ a * c := Nat.eq_of_mul_eq_mul_left hl0 (by rw [← FRC.Nat.mul_assoc, ← hx', e1])424    obtain ⟨d, hd⟩ := eq_mul_of_mod_zero hpa (pow_mod_of_not_mod hl hy a x' (mod_zero_of_eq_mul hpa e2))425    exact mod_zero_of_eq_mul (FRC.Nat.pos_pow_of_pos (a + 1) hl0)426      (by rw [hx', hd, Nat.pow_succ, Nat.mul_comm (l ^ a) l, FRC.Nat.mul_assoc])427428/-- 00:F5, the unique home (`d = 2`): on an odd shell every common divisor of `p − 1` and `p + 1` divides `2`429(`gcd(p − 1, p + 1) = 2`), so an odd prime power `ℓᵃ` dividing `(p − 1)(p + 1)` and not `p − 1` lies on the boost430torus: `ℓᵃ ∣ p + 1`. -/431theorem unique_home {p : Nat} (hp0 : 0 < p) :432    (∀ e : Nat, 0 < e → (p - 1) % e = 0 → (p + 1) % e = 0 → 2 % e = 0) ∧433    (∀ l a : Nat, FRC.Nat.isPrime l → l ≠ 2 → ((p - 1) * (p + 1)) % l ^ a = 0 → (p - 1) % l ^ a ≠ 0 →434      (p + 1) % l ^ a = 0) := by435  have hsum : p + 1 = (p - 1) + 2 := by436    rw [show (2 : Nat) = 1 + 1 from rfl, ← Nat.add_assoc, FRC.Nat.sub_add_cancel hp0]437  have common : ∀ e : Nat, 0 < e → (p - 1) % e = 0 → (p + 1) % e = 0 → 2 % e = 0 := fun e he h1 h2 => by438    rw [hsum] at h2439    exact mod_of_add_mod he (by rw [h2, h1])440  refine ⟨common, fun l a hl hl2 hprod hnot => ?_⟩441  have hl0 : 0 < l := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hl.1442  match Nat.decEq ((p - 1) % l) 0 with443  | .isFalse h1 => exact pow_mod_of_not_mod hl h1 a (p + 1) (by rw [Nat.mul_comm]; exact hprod)444  | .isTrue h1 =>445    -- `l ∣ p − 1`, so `l ∤ p + 1` (else `l ∣ 2`, `l = 2`), and then `ℓᵃ ∣ p − 1`, against the hypothesis446    have h2 : (p + 1) % l ≠ 0 := fun h2 => by447      have h := common l hl0 h1 h2448      obtain ⟨c, hc⟩ := eq_mul_of_mod_zero hl0 h449      have hle : l ≤ 2 := FRC.Nat.le_of_dvd' (Nat.zero_lt_succ 1) ⟨c, hc⟩450      exact hl2 (Nat.le_antisymm hle hl.1)451    exact absurd (pow_mod_of_not_mod hl h2 a (p - 1) hprod) hnot452453/-- 00:F5, the sign: `−1` registers on both faces, `(−1)^{p−1} = (−1)^{p+1} = 1`, of order two (`−1 ≠ 1` on an odd454shell). -/455theorem sign_both {p : Nat} [Pos p] (h2 : 2 < p) (hp2 : p % 2 = 1) :456    (-1 : Shell p) ^ (p - 1) = 1 ∧ (-1 : Shell p) ^ (p + 1) = 1 ∧ (-1 : Shell p) * -1 = 1 ∧ (-1 : Shell p) ≠ 1 := by457  obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 2 (Nat.zero_lt_succ 1) p458  rw [hp2] at hm459  have e1 : p - 1 = 2 * m := by rw [hm, FRC.Nat.add_sub_cancel]460  have e2 : p + 1 = 2 * (m + 1) := by rw [hm, Nat.mul_succ, Nat.add_assoc]461  have sq : (-1 : Shell p) * -1 = 1 := by rw [neg_mul_neg, mul_one]462  refine ⟨by rw [e1, pow_mul, pow_two, sq, one_pow], by rw [e2, pow_mul, pow_two, sq, one_pow], sq,463    Prime.neg_one_ne_one h2⟩464465/-- 00:F5, the visibility cap: on a tower with `p² < Ω < p³` the cap `K = max{k : pᵏ < Ω}` is `2` (`p < Ω`,466`p² < Ω`, and `p³` beyond the totality); every saturating tower `p² < Ω ≤ (p + 1)²`, `p ≥ 3`, has `Ω < p³`; and the467minimal tower `(173, 30 089)` is saturating; the laboratory tower `(1 373, 2 408 561)` has `p² < Ω < p³`. -/468theorem visibility_cap :469    (∀ p Ω : Nat, 1 < p → p * p < Ω → p < Ω) ∧470    (∀ p Ω : Nat, 3 ≤ p → Ω ≤ (p + 1) * (p + 1) → Ω < p * p * p) ∧471    (173 * 173 < 30089 ∧ 30089 ≤ 174 * 174) ∧ (1373 * 1373 < 2408561 ∧ 2408561 < 1373 * 1373 * 1373) := by472  refine ⟨fun p Ω hp h2 => Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_left p (Nat.lt_trans (Nat.zero_lt_succ 0) hp)) h2,473    fun p Ω hp hs => Nat.lt_of_le_of_lt hs ?_, by decide, by decide⟩474  -- (p + 1)² = p² + 2p + 1 < 3p² ≤ p³ for p ≥ 3475  have e : (p + 1) * (p + 1) = p * p + (p + (p + 1)) := by rw [Nat.mul_succ, Nat.succ_mul, Nat.add_assoc]476  have h1 : p + (p + 1) < p * p + p * p := by477    have h3 : 3 * p ≤ p * p := Nat.mul_le_mul_right p hp478    have hpp : p + (p + 1) < 3 * p := by479      rw [show 3 * p = p + (p + p) by rw [Nat.succ_mul, Nat.succ_mul, Nat.one_mul, Nat.add_assoc]]480      exact Nat.add_lt_add_left (Nat.add_lt_add_left (Nat.lt_of_lt_of_le (by decide : 1 < 3) hp) _) _481    exact Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le hpp h3) (Nat.le_add_right _ _)482  have h4 : p * p + p * p + p * p ≤ p * p * p := by483    rw [show p * p + p * p + p * p = p * p * 3 by rw [Nat.mul_succ, Nat.mul_succ, Nat.mul_one]]484    exact Nat.mul_le_mul_left _ hp485  rw [e]486  exact Nat.lt_of_lt_of_le (by rw [Nat.add_assoc (p * p) (p * p) (p * p)]; exact Nat.add_lt_add_left h1 _) h4487488/-- 00:F5, the 2-components on a Subject with `κ` odd (`p − 1 = 4κ`, `p + 1 = 4κ + 2`): the quarter absorbs (`4 ∣ p − 1`)489and the sign is on both faces (`2 ∣ p + 1`), while `8 ∤ p − 1` and `4 ∤ p + 1`, so a 2-component `2ᵃ`, `a ≥ 3`, lies on490neither torus: at depth `2` it registers in `𝔽_{p²}` off both, not on the boost torus. -/491theorem two_part_homes {κ : Nat} (hκ : κ % 2 = 1) :492    (4 * κ) % 4 = 0 ∧ (4 * κ) % 8 ≠ 0 ∧ (4 * κ + 2) % 2 = 0 ∧ (4 * κ + 2) % 4 ≠ 0 ∧493    ∀ a, 3 ≤ a → (4 * κ) % 2 ^ a ≠ 0 ∧ (4 * κ + 2) % 2 ^ a ≠ 0 := by494  obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 2 (Nat.zero_lt_succ 1) κ495  rw [hκ] at hm496  have e1 : 4 * κ = 8 * m + 4 := by rw [hm, Nat.left_distrib, ← FRC.Nat.mul_assoc]497  have e2 : 4 * κ + 2 = 4 * (2 * m + 1) + 2 := by rw [hm]498  have h8 : (4 * κ) % 8 ≠ 0 := by rw [e1, FRC.Nat.add_mul_mod_self_left _ _ _ (by decide)]; decide499  have h4 : (4 * κ + 2) % 4 ≠ 0 := by rw [e2, FRC.Nat.add_mul_mod_self_left _ _ _ (by decide)]; decide500  have hpow : ∀ a, 3 ≤ a → ∃ c, 2 ^ a = 8 * c := fun a ha =>501    ⟨2 ^ (a - 3), by rw [show (8 : Nat) = 2 ^ 3 from rfl, ← FRC.Nat.pow_add, FRC.Nat.add_sub_of_le ha]⟩502  refine ⟨mod_zero_of_eq_mul (by decide) rfl, h8, mod_zero_of_eq_mul (by decide) (by rw [e2, show 4 * (2 * m + 1) + 2 = 2 * (2 * (2 * m + 1) + 1) by rw [Nat.mul_succ 2, ← FRC.Nat.mul_assoc]]), h4,503    fun a ha => ⟨fun h => h8 ?_, fun h => h4 ?_⟩⟩504  · obtain ⟨c, hc⟩ := hpow a ha505    obtain ⟨d, hd⟩ := eq_mul_of_mod_zero (FRC.Nat.pos_pow_of_pos a (by decide)) h506    exact mod_zero_of_eq_mul (by decide) (by rw [hd, hc, FRC.Nat.mul_assoc])507  · obtain ⟨c, hc⟩ := hpow a ha508    obtain ⟨d, hd⟩ := eq_mul_of_mod_zero (FRC.Nat.pos_pow_of_pos a (by decide)) h509    exact mod_zero_of_eq_mul (by decide) (by rw [hd, hc, show (8 : Nat) = 4 * 2 from rfl, FRC.Nat.mul_assoc, FRC.Nat.mul_assoc])510511/-- 00:F5, the instances (39:B2, B3, B5), decided by the kernel: the depth of `7` (hydrogen's interior) is `6` at512`173`, `2` at `181` and `1` at `197`, each the least `d` with `pᵈ ≡ 1 (mod 7)`; hydrogen's quarter is absorbed at `173`513with the images `{1, 80, 93, 172}`, exactly the roots of `x⁴ = 1`, and its triality is observable there (`3 ∤ 172`,514`3 ∣ 174`); the proton (`q = 5`) registers whole, `4 ∣ 172` and `6 ∣ 174`; `(5, 13)` is refused, `5² > 13`. -/515theorem registration_instances :516    ((173 ^ 6) % 7 = 1 ∧ ∀ d, 0 < d → d < 6 → (173 ^ d) % 7 ≠ 1) ∧517    ((181 ^ 2) % 7 = 1 ∧ 181 % 7 ≠ 1) ∧ 197 % 7 = 1 ∧518    (∀ v, v < 173 → ((ofNat v : Shell 173) ^ 4 = 1 ↔ v = 1 ∨ v = 80 ∨ v = 93 ∨ v = 172)) ∧519    (172 % 3 ≠ 0 ∧ 174 % 3 = 0) ∧ (172 % 4 = 0 ∧ 174 % 6 = 0) ∧ 13 < 5 * 5 := by520  refine ⟨⟨by decide, fun d h0 h6 => ?_⟩, by decide, by decide, by decide +kernel, by decide, by decide, by decide⟩521  · match d, h0, h6 with522    | 1, _, _ => decide523    | 2, _, _ => decide524    | 3, _, _ => decide525    | 4, _, _ => decide526    | 5, _, _ => decide527    | k + 6, _, h => exact absurd h (Nat.not_lt_of_le (Nat.le_add_left 6 k))528end registration529530end FRC.Quantum531