Theme/Pair.lean — FrcCore

1import FrcCore.Theme.Subject23/-!4# FrcCore.Theme.Pair — the pair `(p, Ω)`: the window, the leak rate, the joint cycle, the tick arithmetic and the5covering parity theorem (the subject theme's second file; 38-s13, 12 October 2026)67The arithmetic of a Subject `p = 4κ + 1` hosted by a Carrier `Ω = 4S + 1`, from *The Light Cone of the Minimal Pair*8(tree `38-s13-20260801`), on the naturals and on the shell:910* **38:A2** the tower congruence `4a − κb = 1` has a solution for every odd `κ` (`tower_solvable`);11* **38:A8, 38:B2** the resolvable window: `4k < p` exactly when `k ≤ κ`, and two window heights conserve exactly,12  `k₁ + k₂ ≤ 2κ < 4κ` (`window`, `window_sum`);13* **38:C10, 38:X1, 38:X3** the per-chronon leak rate `(κ/S)/(p − 1) = 1/(4S) = 1/(Ω − 1)`, `κ`-free, as integer14  identities (`leak_rate`);15* **38:C14, 38:B5, 38:B7** the joint cycle of a `κ`-odd pair (`S = 2m` even): for `ℓ` a common multiple of16  `κ = 2a + 1` and `m` with `ℓ/m` odd, the shell is home and the Carrier reads the half at `4ℓ` ticks, both home at `8ℓ`17  (`joint_cycle`); on frames, `g^{4ℓ} = 1` and `h^{4ℓ} = −1` (`joint_cycle_frame`);18* **38:C1, 38:C4, 38:C5** the flow law as a tick count on the cycle, home at the row's own clock and the parity image19  half a cycle on (`tick`, `tick_home`, `tick_half`); the half turn as the point reflection (`half_turn`);20* **38:D12** the covering parity theorem: the reflection identity `⌊ab/p⌋ + ⌊(p − a)b/p⌋ = b − 1` on a prime shell21  (`reflection_identity`), the four candidate identities and the multiplicity `μ ∈ {1, 3}` with `μ = 3` exactly on the22  even rows and the position law of the odd sector (`covering_parity`), the quotients taken as the division23  algorithm's (`FRC.Nat.mod_spec`, `quot_unique`), the parities decided by the kernel on the eight-case table.2425No prelude division lemma is used (they carry `propext`); the quotients are named by their defining equations. No axioms.26-/2728namespace FRC.Pair2930open FRC.Shell3132/-! ## 38:A2 — the tower congruence -/3334/-- 38:A2 — the tower congruence `4a − κb = 1` is solvable for every odd `κ`: `(a, b) = ((3κ + 1)/4, 3)` for35`κ ≡ 1 (mod 4)` and `((κ + 1)/4, 1)` for `κ ≡ 3 (mod 4)` — the instances `(1, 1)` at `κ = 3`, `(4, 3)` at `κ = 5`,36`(2, 1)` at `κ = 7`. -/37theorem tower_solvable (κ : Nat) (hκ : κ % 2 = 1) : ∃ a b : Nat, 4 * a = κ * b + 1 := by38  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec 4 (by decide) κ39  have hr : κ % 4 = 1 ∨ κ % 4 = 3 := by40    have h2 : (4 * q + κ % 4) % 2 = 1 := by rw [← hq]; exact hκ41    have e4 : 4 * q = 2 * (2 * q) := by rw [← FRC.Nat.mul_assoc]42    rw [e4, FRC.Nat.add_mul_mod_self_left (κ % 4) (2 * q) 2 (by decide)] at h243    have key : ∀ r, r < 4 → r % 2 = 1 → r = 1 ∨ r = 3 := by decide44    exact key _ (Nat.mod_lt κ (by decide)) h245  match hr with46  | .inl h1 =>47    refine ⟨3 * q + 1, 3, ?_⟩48    rw [hq, h1]49    calc 4 * (3 * q + 1) = 4 * (3 * q) + 4 := Nat.mul_add 4 (3 * q) 150      _ = 4 * q * 3 + 4 := by rw [Nat.mul_comm 3 q, ← FRC.Nat.mul_assoc]51      _ = (4 * q + 1) * 3 + 1 := by rw [FRC.Nat.add_mul, Nat.one_mul, Nat.add_assoc]52  | .inr h3 =>53    refine ⟨q + 1, 1, ?_⟩54    rw [hq, h3, Nat.mul_one, Nat.mul_add, Nat.mul_one]5556/-! ## 38:A8, 38:B2 — the resolvable window -/5758/-- 38:A8, 38:B2, 38:D1 — the capacity clause: `4k < p = 4κ + 1` exactly when `k ≤ κ`; the window `|k̂| ≤ κ`, and the59radial ladder's `κ` shells. -/60theorem window (κ k : Nat) : 4 * k < 4 * κ + 1 ↔ k ≤ κ :=61  ⟨fun h => Nat.le_of_mul_le_mul_left (Nat.le_of_lt_succ h) (by decide : 0 < 4),62   fun h => Nat.lt_succ_of_le (Nat.mul_le_mul_left 4 h)⟩6364/-- 38:A8 — pairwise conservation on the window is exact: two heights of magnitude at most `κ` sum to at most `2κ`,65strictly inside one period `4κ = p − 1`. -/66theorem window_sum {κ k₁ k₂ : Nat} (hκ : 0 < κ) (h₁ : k₁ ≤ κ) (h₂ : k₂ ≤ κ) :67    k₁ + k₂ ≤ 2 * κ ∧ 2 * κ < 4 * κ := by68  refine ⟨by rw [Nat.two_mul]; exact Nat.add_le_add h₁ h₂, ?_⟩69  have e : 4 * κ = 2 * κ + 2 * κ := FRC.Nat.add_mul 2 2 κ70  rw [e]; exact Nat.lt_add_of_pos_right (Nat.mul_pos (by decide) hκ)7172/-! ## 38:C10 — the per-chronon leak rate -/7374/-- 38:C10, 38:C7, 38:C13, 38:C14, 38:X1, 38:X3 — the leak rate per chronon is `κ`-free: `(κ/S)/(p − 1) = 1/(4S) = 1/(Ω − 1)`, as the integer75identities `κ · 4S = S · (p − 1)`, `4S = Ω − 1`, and the temporal face on the cover `2(Ω − 1) = 8S`. -/76theorem leak_rate {p Ω κ S : Nat} (hp : p = 4 * κ + 1) (hΩ : Ω = 4 * S + 1) :77    κ * (4 * S) = S * (p - 1) ∧ 4 * S = Ω - 1 ∧ 2 * (Ω - 1) = 8 * S := by78  have e1 : p - 1 = 4 * κ := by rw [hp]; exact FRC.Nat.add_sub_cancel (4 * κ) 179  have e2 : Ω - 1 = 4 * S := by rw [hΩ]; exact FRC.Nat.add_sub_cancel (4 * S) 180  refine ⟨?_, e2.symm, ?_⟩81  · rw [e1]82    calc κ * (4 * S) = 4 * S * κ := Nat.mul_comm κ (4 * S)83      _ = 4 * (S * κ) := FRC.Nat.mul_assoc 4 S κ84      _ = S * (4 * κ) := FRC.Nat.mul_left_comm 4 S κ85  · rw [e2, ← FRC.Nat.mul_assoc]8687/-- A multiple of the modulus is `0` modulo it. -/88theorem mod_mul_self (p q : Nat) (hp : 0 < p) : (p * q) % p = 0 :=89  FRC.Nat.mod_unique hp (Nat.add_zero (p * q)).symm9091/-! ## 38:C14 — the joint cycle -/9293/-- 38:C14, 38:B5, 38:B7 — the joint cycle of a `κ`-odd pair with `S` even: `κ = 2a + 1`, `S = 2m`, `ℓ` a common multiple94of `2a + 1` and `m` with `ℓ/m` odd (`ℓ = (2a + 1)(2u + 1) = m(2v + 1)`). At `4ℓ` ticks the shell is home (`4ℓ ≡ 0 mod 4κ`)95and the Carrier reads the half (`4ℓ ≡ 4m = (Ω − 1)/2 mod 8m`); at `8ℓ` both are home. At the instance `ℓ = 87 = 3 · 29`. -/96theorem joint_cycle {a m u v ℓ : Nat} (hm : 0 < m) (hu : ℓ = (2 * a + 1) * (2 * u + 1)) (hv : ℓ = m * (2 * v + 1)) :97    (4 * ℓ) % (4 * (2 * a + 1)) = 0 ∧ (4 * ℓ) % (8 * m) = 4 * m ∧98    (8 * ℓ) % (4 * (2 * a + 1)) = 0 ∧ (8 * ℓ) % (8 * m) = 0 := by99  have ha0 : 0 < 4 * (2 * a + 1) := Nat.mul_pos (by decide) (Nat.zero_lt_succ _)100  have hb0 : 0 < 8 * m := Nat.mul_pos (by decide) hm101  have hb4 : 4 * m < 8 * m := Nat.mul_lt_mul_of_pos_right (by decide : 4 < 8) hm102  -- `4ℓ = (4(2a + 1)) (2u + 1)` and `8ℓ = (4(2a + 1)) (2(2u + 1))`103  have e1 : 4 * ℓ = 4 * (2 * a + 1) * (2 * u + 1) := by rw [hu, FRC.Nat.mul_assoc]104  have e3 : 8 * ℓ = 4 * (2 * a + 1) * (2 * (2 * u + 1)) := by105    rw [hu]106    calc 8 * ((2 * a + 1) * (2 * u + 1)) = 4 * (2 * ((2 * a + 1) * (2 * u + 1))) := FRC.Nat.mul_assoc 4 2 _107      _ = 4 * ((2 * a + 1) * (2 * (2 * u + 1))) := by rw [FRC.Nat.mul_left_comm 2 (2 * a + 1)]108      _ = 4 * (2 * a + 1) * (2 * (2 * u + 1)) := (FRC.Nat.mul_assoc 4 _ _).symm109  -- `4ℓ = 8m v + 4m` and `8ℓ = (8m) (2v + 1)`110  have e2 : 4 * ℓ = 8 * m * v + 4 * m := by111    rw [hv]112    calc 4 * (m * (2 * v + 1)) = 4 * (m * (2 * v) + m) := by rw [Nat.mul_add, Nat.mul_one]113      _ = 4 * (m * (2 * v)) + 4 * m := Nat.mul_add 4 _ _114      _ = 4 * (2 * (m * v)) + 4 * m := by rw [FRC.Nat.mul_left_comm m 2 v]115      _ = 4 * 2 * (m * v) + 4 * m := by rw [FRC.Nat.mul_assoc 4 2]116      _ = 8 * m * v + 4 * m := by rw [← FRC.Nat.mul_assoc 8]117  have e4 : 8 * ℓ = 8 * m * (2 * v + 1) := by rw [hv, FRC.Nat.mul_assoc]118  refine ⟨by rw [e1, mod_mul_self _ _ ha0], FRC.Nat.mod_unique hb4 e2, by rw [e3, mod_mul_self _ _ ha0],119    by rw [e4, mod_mul_self _ _ hb0]⟩120121/-- 38:C14 on the frames: a Subject frame of odd capacity `κ = 2a + 1` and a Carrier frame of even capacity `S = 2m`122return together — at `4ℓ` the Subject's drive is home, `g^{4ℓ} = 1`, and the Carrier's reads the half, `h^{4ℓ} = −1`123(the sign event); at `8ℓ` both are home. -/124theorem joint_cycle_frame {p Ω : Nat} [Pos p] [Pos Ω] {a m : Nat} {g : Shell p} {h : Shell Ω}125    (F : Frame p (2 * a + 1) g) (G : Frame Ω (2 * m) h) (hm : 0 < m) {u v ℓ : Nat}126    (hu : ℓ = (2 * a + 1) * (2 * u + 1)) (hv : ℓ = m * (2 * v + 1)) :127    g ^ (4 * ℓ) = 1 ∧ h ^ (4 * ℓ) = -1 ∧ g ^ (8 * ℓ) = 1 ∧ h ^ (8 * ℓ) = 1 := by128  obtain ⟨c1, c2, c3, c4⟩ := joint_cycle hm hu hv129  have eS : Ω - 1 = 8 * m := by130    rw [G.n_eq]; show 4 * (2 * m) = 8 * m131    rw [← FRC.Nat.mul_assoc]132  have eH : 2 * (2 * m) = 4 * m := by rw [← FRC.Nat.mul_assoc]133  refine ⟨F.pow_eq_one_of_mod (by rw [F.n_eq]; exact c1), ?_, F.pow_eq_one_of_mod (by rw [F.n_eq]; exact c3),134    G.pow_eq_one_of_mod (by rw [eS]; exact c4)⟩135  rw [G.pow_mod, eS, c2, ← eH]; exact G.half_period136137/-- 38:C14 — the joint returns are exactly the common multiples of the two periods, so the least is `lcm(p − 1, Ω − 1)`;138for `κ` odd and `S = 2m` even it is `8ℓ`, `ℓ` the least common multiple of `κ` and `m` (`joint_return_eight`), whose139cofactor over `m` is odd (`joint_cycle_frame`). -/140theorem joint_return_iff {p Ω : Nat} [Pos p] [Pos Ω] {κ S : Nat} {g : Shell p} {h : Shell Ω}141    (F : Frame p κ g) (G : Frame Ω S h) (n : Nat) :142    g ^ n = 1 ∧ h ^ n = 1 ↔ n % (p - 1) = 0 ∧ n % (Ω - 1) = 0 :=143  ⟨fun ⟨hg, hh⟩ => ⟨F.mod_eq_zero_of_pow_eq_one hg, G.mod_eq_zero_of_pow_eq_one hh⟩,144   fun ⟨hg, hh⟩ => ⟨F.pow_eq_one_of_mod hg, G.pow_eq_one_of_mod hh⟩⟩145146/-- 38:C14 — every common multiple of the periods `4κ` (`κ = 2a + 1` odd) and `8m` (`S = 2m` even) is eight times a common147multiple of `κ` and `m`: with `joint_return_iff` the least joint return is `8ℓ`, `ℓ = lcm(κ, m)`, and its half `4ℓ` is148`joint_cycle_frame`'s sign event (`ℓ/m = κ/gcd(κ, m)` is odd). -/149theorem joint_return_eight {a m n : Nat} (hm : 0 < m) (h4 : n % (4 * (2 * a + 1)) = 0) (h8 : n % (8 * m) = 0) :150    ∃ k, n = 8 * k ∧ k % (2 * a + 1) = 0 ∧ k % m = 0 := by151  have ha0 : 0 < 4 * (2 * a + 1) := Nat.mul_pos (by decide) (Nat.zero_lt_succ _)152  have hb0 : 0 < 8 * m := Nat.mul_pos (by decide) hm153  obtain ⟨v, hv⟩ := FRC.Nat.mod_spec _ hb0 n154  obtain ⟨u, hu⟩ := FRC.Nat.mod_spec _ ha0 n155  rw [h8, Nat.add_zero] at hv156  rw [h4, Nat.add_zero] at hu157  refine ⟨m * v, by rw [hv, FRC.Nat.mul_assoc], ?_, mod_mul_self _ _ hm⟩158  have e : (2 * a + 1) * u = 2 * (m * v) := by159    apply Nat.eq_of_mul_eq_mul_left (show 0 < 4 by decide)160    calc 4 * ((2 * a + 1) * u) = 4 * (2 * a + 1) * u := (FRC.Nat.mul_assoc _ _ _).symm161      _ = 8 * m * v := hu.symm.trans hv162      _ = 4 * (2 * (m * v)) := by163        show 4 * 2 * m * v = 4 * (2 * (m * v))164        rw [FRC.Nat.mul_assoc (4 * 2), FRC.Nat.mul_assoc 4 2]165  obtain ⟨k, hk⟩ := FRC.Nat.mod_spec 2 (by decide) u166  rcases FRC.Nat.mod_two_cases u with h0 | h1167  · rw [h0, Nat.add_zero] at hk168    rw [hk, FRC.Nat.mul_left_comm] at e169    rw [← Nat.eq_of_mul_eq_mul_left (show 0 < 2 by decide) e]170    exact mod_mul_self _ _ (Nat.zero_lt_succ _)171  · rw [h1] at hk172    rw [hk, Nat.mul_add, Nat.mul_one, FRC.Nat.mul_left_comm, ← Nat.add_assoc, Nat.add_comm (2 * ((2 * a + 1) * k)) (2 * a),173      ← Nat.mul_add] at e174    -- `2 (a + (2a + 1) k) + 1 = 2 m'`: odd against even175    have h1' : (2 * (a + (2 * a + 1) * k) + 1) % 2 = 1 := FRC.Nat.mod_unique (by decide) rfl176    rw [e, mod_mul_self _ _ (by decide)] at h1'177    exact absurd h1' (by decide)178179/-! ## 38:C1, 38:C4, 38:C5 — the tick arithmetic of the flow -/180181/-- 38:C1 — the flow law as a tick count: on the cycle of `n` ticks, row `k` at clock `b` stands at182`(k − b) mod n`, read as `(k + (n − b mod n)) mod n`; the law `φ(k) = −(b_C − k)π/116` is this count in units of183`2π/232`. -/184def tick (n k b : Nat) : Nat := (k + (n - b % n)) % n185186/-- 38:C1, 38:C5 — home: at the row's own clock the count is `0`. -/187theorem tick_home (n : Nat) (hn : 0 < n) (k : Nat) : tick n k k = 0 := by188  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec n hn k189  have hle : k % n ≤ n := Nat.le_of_lt (FRC.Nat.mod_lt' k hn)190  have e : k + (n - k % n) = n * (q + 1) + 0 := by191    rw [Nat.add_zero, Nat.mul_add, Nat.mul_one]192    calc k + (n - k % n) = n * q + k % n + (n - k % n) := by rw [← hq]193      _ = n * q + (k % n + (n - k % n)) := Nat.add_assoc _ _ _194      _ = n * q + n := by rw [FRC.Nat.add_sub_of_le hle]195  exact FRC.Nat.mod_unique hn e196197/-- 38:C5, 38:B7 — the parity image: half a cycle on from the row's own clock the count is the half, `m` on `2m` ticks198(`116` on `C₂₃₂`: `b_C = 116 + k`). -/199theorem tick_half (m : Nat) (hm : 0 < m) (k : Nat) : tick (2 * m) k (k + m) = m := by200  have h2 : 0 < 2 * m := Nat.mul_pos (by decide) hm201  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec (2 * m) h2 (k + m)202  have hle : (k + m) % (2 * m) ≤ 2 * m := Nat.le_of_lt (FRC.Nat.mod_lt' (k + m) h2)203  -- `tick + m ≡ 0`: `k + (2m − r) + m = (k + m) + (2m − r) = 2m q + r + (2m − r) = 2m (q + 1)`204  have e : k + (2 * m - (k + m) % (2 * m)) + m = 2 * m * (q + 1) + 0 := by205    rw [Nat.add_zero, Nat.mul_add, Nat.mul_one, Nat.add_right_comm]206    calc k + m + (2 * m - (k + m) % (2 * m))207        = 2 * m * q + (k + m) % (2 * m) + (2 * m - (k + m) % (2 * m)) := by rw [← hq]208      _ = 2 * m * q + ((k + m) % (2 * m) + (2 * m - (k + m) % (2 * m))) := Nat.add_assoc _ _ _209      _ = 2 * m * q + 2 * m := by rw [FRC.Nat.add_sub_of_le hle]210  have hz : (k + (2 * m - (k + m) % (2 * m)) + m) % (2 * m) = 0 := FRC.Nat.mod_unique h2 e211  -- the count `t < 2m` with `(t + m) % 2m = 0` is `m`212  unfold tick213  obtain ⟨s, hs⟩ := FRC.Nat.mod_spec (2 * m) h2 (k + (2 * m - (k + m) % (2 * m)))214  have ht := FRC.Nat.mod_lt' (k + (2 * m - (k + m) % (2 * m))) h2215  generalize (k + (2 * m - (k + m) % (2 * m))) % (2 * m) = t at hs ht hz216  generalize k + (2 * m - (k + m) % (2 * m)) = x at hs hz217  rw [hs, Nat.add_assoc, FRC.Nat.add_mul_mod_self_left _ _ _ h2] at hz218  obtain ⟨c, hc⟩ := FRC.Nat.mod_spec (2 * m) h2 (t + m)219  rw [hz, Nat.add_zero] at hc220  -- `t + m = 2m c` with `m ≤ t + m < 3m`: `c = 1`221  match c with222  | 0 => exact absurd (hc.trans (Nat.mul_zero _)) (Nat.ne_of_gt (Nat.lt_of_lt_of_le hm (Nat.le_add_left m t)))223  | 1 =>224    rw [Nat.mul_one, Nat.two_mul] at hc225    exact Nat.add_right_cancel hc226  | c + 2 =>227    have h3 : 2 * m * 2 ≤ 2 * m * (c + 2) := Nat.mul_le_mul_left _ (Nat.le_add_left 2 c)228    have hmle : m ≤ 2 * m := by rw [Nat.two_mul]; exact Nat.le_add_left m m229    have h4 : t + m < 2 * m * 2 := by230      rw [Nat.mul_comm (2 * m) 2, Nat.two_mul (2 * m)]231      exact Nat.lt_of_lt_of_le (Nat.add_lt_add_right ht m) (Nat.add_le_add_left hmle (2 * m))232    exact absurd (hc ▸ Nat.lt_of_lt_of_le h4 h3) (Nat.lt_irrefl _)233234/-- 38:C4 — the half turn on the cycle of `2m` ticks is the point reflection: two half turns are the identity, the235reflection `x ↦ 2m − x` is the negation (`x + (2m − x) ≡ 0`), and the rim `m` is its own reflection (the rim kiss). -/236theorem half_turn (m : Nat) (hm : 0 < m) (x : Nat) :237    (x + m + m) % (2 * m) = x % (2 * m) ∧ (x + (2 * m - x % (2 * m))) % (2 * m) = 0 ∧238    (2 * m - m % (2 * m)) % (2 * m) = m % (2 * m) := by239  have h2 : 0 < 2 * m := Nat.mul_pos (by decide) hm240  have hm2 : m < 2 * m := by rw [Nat.two_mul]; exact Nat.lt_add_of_pos_right hm241  refine ⟨?_, tick_home (2 * m) h2 x, ?_⟩242  · rw [Nat.add_assoc, ← Nat.two_mul, FRC.Nat.add_mod x (2 * m) (2 * m) h2, FRC.Nat.mod_self _ h2, Nat.add_zero,243      FRC.Nat.mod_mod x _ h2]244  · rw [FRC.Nat.mod_eq_of_lt hm2]245    have e : 2 * m - m = m := by rw [Nat.two_mul]; exact FRC.Nat.add_sub_cancel m m246    rw [e, FRC.Nat.mod_eq_of_lt hm2]247248/-! ## 38:D12 — the reflection identity and the covering parity theorem -/249250/-- 38:D12 — the reflection identity on a prime shell: for `0 < a, b < p` the quotients of `ab` and `(p − a)b` by `p`251sum to `b − 1`, `⌊ab/p⌋ + ⌊(p − a)b/p⌋ + 1 = b`. The quotients are the division algorithm's: `ab = p q₁ + (ab mod p)`252and `(p − a)b = p q₂ + ((p − a)b mod p)` (`FRC.Nat.mod_spec` names them, `quot_unique` makes them unique). -/253theorem reflection_identity {p a b q₁ q₂ : Nat} (hp : FRC.Nat.isPrime p) (ha0 : 0 < a) (ha : a < p)254    (hb0 : 0 < b) (hb : b < p) (h₁ : a * b = p * q₁ + (a * b) % p)255    (h₂ : (p - a) * b = p * q₂ + ((p - a) * b) % p) : q₁ + q₂ + 1 = b := by256  have hp0 : 0 < p := Nat.lt_of_lt_of_le (by decide) hp.1257  have hr1 := FRC.Nat.mod_lt' (a * b) hp0258  have hr2 := FRC.Nat.mod_lt' ((p - a) * b) hp0259  -- `ab mod p ≠ 0`: `p` prime, `a, b` nonzero residues260  have hne : (a * b) % p ≠ 0 := fun h0 =>261    match FRC.Nat.prime_mul_mod hp h0 with262    | .inl h => Nat.ne_of_gt ha0 (by rw [FRC.Nat.mod_eq_of_lt ha] at h; exact h)263    | .inr h => Nat.ne_of_gt hb0 (by rw [FRC.Nat.mod_eq_of_lt hb] at h; exact h)264  -- `pb = p (q₁ + q₂) + (r₁ + r₂)`265  have hsum : p * b = p * (q₁ + q₂) + ((a * b) % p + ((p - a) * b) % p) := by266    calc p * b = (a + (p - a)) * b := by rw [FRC.Nat.add_sub_of_le (Nat.le_of_lt ha)]267      _ = a * b + (p - a) * b := FRC.Nat.add_mul a (p - a) b268      _ = p * q₁ + (a * b) % p + (p * q₂ + ((p - a) * b) % p) := by rw [← h₁, ← h₂]269      _ = p * (q₁ + q₂) + ((a * b) % p + ((p - a) * b) % p) := by270        rw [Nat.mul_add, FRC.Nat.add_add_add_comm]271  -- the residues sum to `0` or `p`; not `0`272  have hmod : ((a * b) % p + ((p - a) * b) % p) % p = 0 := by273    have := FRC.Nat.add_mul_mod_self_left ((a * b) % p + ((p - a) * b) % p) (q₁ + q₂) p hp0274    rw [← hsum] at this275    rw [← this]; exact mod_mul_self p b hp0276  obtain ⟨c, hc⟩ := FRC.Nat.mod_spec p hp0 ((a * b) % p + ((p - a) * b) % p)277  rw [hmod, Nat.add_zero] at hc278  have hlt2 : (a * b) % p + ((p - a) * b) % p < p * 2 := by279    rw [Nat.mul_two]; exact Nat.add_lt_add hr1 hr2280  match c with281  | 0 =>282    rw [Nat.mul_zero] at hc283    exact absurd (Nat.eq_zero_of_le_zero (hc ▸ Nat.le_add_right _ _)) hne284  | 1 =>285    rw [Nat.mul_one] at hc286    rw [hc] at hsum287    have e : p * b = p * (q₁ + q₂ + 1) := by rw [hsum, Nat.mul_succ]288    exact (Nat.eq_of_mul_eq_mul_left hp0 e).symm289  | c + 2 =>290    have h3 : p * 2 ≤ p * (c + 2) := Nat.mul_le_mul_left p (Nat.le_add_left 2 c)291    exact absurd (hc ▸ Nat.lt_of_lt_of_le hlt2 h3) (Nat.lt_irrefl _)292293/-- The multiplicity of a node from the wrap counts of its four candidate slots `(M, a)`, `(p − M, a)`, `(M, p − a)`,294`(p − M, p − a)`, which must be even, odd, odd, even in turn to land on the node's route. -/295def mu (A B C D : Nat) : Nat :=296  (if A % 2 = 0 then 1 else 0) + (if B % 2 = 1 then 1 else 0) + (if C % 2 = 1 then 1 else 0) +297    (if D % 2 = 0 then 1 else 0)298299theorem mu_mod (A B C D : Nat) : mu A B C D = mu (A % 2) (B % 2) (C % 2) (D % 2) := by300  unfold mu301  rw [FRC.Nat.mod_mod A 2 (by decide), FRC.Nat.mod_mod B 2 (by decide), FRC.Nat.mod_mod C 2 (by decide),302    FRC.Nat.mod_mod D 2 (by decide)]303304/-- 38:D12 — the eight-case parity table, decided by the kernel on the residues: with `x = ā`, `y = M̄`, `z = α = A mod 2`,305`u, v, t` the parities of `B, C, D` and `w = k̄`, the relations `k̄ = ā M̄ + α`, `A + B + 1 = a`, `A + C + 1 = M`,306`C + D + 1 = p − a` force `μ = 3` exactly when `k̄ = 0`, `μ ∈ {1, 3}`, and on an odd row the single match is a direct307slot (wrap `A` even or `B` odd, parameter `a`) exactly when `a` is odd. -/308theorem parity_table : ∀ x, x < 2 → ∀ y, y < 2 → ∀ z, z < 2 → ∀ u, u < 2 → ∀ v, v < 2 → ∀ t, t < 2 →309    ∀ w, w < 2 → (z + w) % 2 = (x * y) % 2 → (z + u + 1) % 2 = x → (z + v + 1) % 2 = y → (v + t + 1) % 2 = (1 + x) % 2 →310    (mu z u v t = 3 ↔ w = 0) ∧ (mu z u v t = 1 ∨ mu z u v t = 3) ∧ (w = 1 → (x = 1 ↔ (z = 0 ∨ u = 1))) := by311  decide312313/-- Two residues mod 2 from a sum: `(s + x) % 2 = 1` with `s, x < 2` gives `s = (1 + x) % 2`. -/314theorem odd_sum_residue : ∀ s, s < 2 → ∀ x, x < 2 → (s + x) % 2 = 1 → s = (1 + x) % 2 := by decide315316/-- 38:D12, 38:D7 — **the covering parity theorem** (Theorem *The covering parity theorem*, Lemma *The all-shell parity317table*). On an odd prime shell `p`, a node of shell `a` and row `k` (`0 < a, k < p`) with `M = k a⁻¹` (`aM ≡ k`,318`0 < M < p`) has the four candidate slots with wrap counts `A = ⌊aM/p⌋`, `B = ⌊(p − M)a/p⌋`, `C = ⌊M(p − a)/p⌋`,319`D = ⌊(p − M)(p − a)/p⌋`, the quotients of the division algorithm. Then the reflection identity four ways,320`A + B + 1 = a`, `A + C + 1 = M`, `C + D + 1 = p − a`, `B + D + 1 = p − M`; `aM = pA + k` exactly; and the multiplicity321`μ = mu A B C D` of the node satisfies `μ = 3` exactly when `k` is even, `μ ∈ {1, 3}` (so no node is missed), and on an322odd row the single match is direct (`A` even or `B` odd, parameter `a`) exactly when the shell `a` is odd. -/323theorem covering_parity {p a k M A B C D : Nat} (hp : FRC.Nat.isPrime p) (hodd : p % 2 = 1)324    (ha0 : 0 < a) (ha : a < p) (_hk0 : 0 < k) (hk : k < p) (hM0 : 0 < M) (hM : M < p)325    (hA : a * M = p * A + k)326    (hB : (p - M) * a = p * B + ((p - M) * a) % p)327    (hC : M * (p - a) = p * C + (M * (p - a)) % p)328    (hD : (p - M) * (p - a) = p * D + ((p - M) * (p - a)) % p) :329    (A + B + 1 = a ∧ A + C + 1 = M ∧ C + D + 1 = p - a ∧ B + D + 1 = p - M) ∧330    (mu A B C D = 3 ↔ k % 2 = 0) ∧ (mu A B C D = 1 ∨ mu A B C D = 3) ∧331    (k % 2 = 1 → (a % 2 = 1 ↔ (A % 2 = 0 ∨ B % 2 = 1))) := by332  have hp0 : 0 < p := Nat.lt_of_lt_of_le (by decide) hp.1333  have hpa0 : 0 < p - a := FRC.Nat.le_sub_of_add_le (by rw [Nat.add_comm]; exact Nat.succ_le_of_lt ha)334  have hpa : p - a < p := Nat.sub_lt hp0 ha0335  have hpM0 : 0 < p - M := FRC.Nat.le_sub_of_add_le (by rw [Nat.add_comm]; exact Nat.succ_le_of_lt hM)336  have hpM : p - M < p := Nat.sub_lt hp0 hM0337  -- `A` is the quotient of `aM`: `aM mod p = k`338  have hA' : a * M = p * A + (a * M) % p := by rw [FRC.Nat.mod_unique hk hA]; exact hA339  have hMa : M * a = p * A + (M * a) % p := by rw [Nat.mul_comm M a]; exact hA'340  have hB' : (p - M) * a = p * B + ((p - M) * a) % p := hB341  have hCb : (p - a) * M = p * C + ((p - a) * M) % p := by rw [Nat.mul_comm (p - a) M]; exact hC342  have hDb : (p - a) * (p - M) = p * D + ((p - a) * (p - M)) % p := by343    rw [Nat.mul_comm (p - a) (p - M)]; exact hD344  have haM : a * (p - M) = p * B + (a * (p - M)) % p := by rw [Nat.mul_comm a (p - M)]; exact hB'345  have hMpa : M * (p - a) = p * C + (M * (p - a)) % p := hC346  have i1 : A + B + 1 = a := reflection_identity hp hM0 hM ha0 ha hMa hB'347  have i2 : A + C + 1 = M := reflection_identity hp ha0 ha hM0 hM hA' hCb348  have i3 : C + D + 1 = p - a := reflection_identity hp hM0 hM hpa0 hpa hMpa hD349  have i4 : B + D + 1 = p - M := reflection_identity hp ha0 ha hpM0 hpM haM hDb350  refine ⟨⟨i1, i2, i3, i4⟩, ?_⟩351  -- the parities: every relation read modulo `2`352  have two : 0 < 2 := by decide353  have r1 : (A % 2 + k % 2) % 2 = (a % 2 * (M % 2)) % 2 := by354    have e : (a * M) % 2 = (p * A + k) % 2 := by rw [hA]355    rw [FRC.Nat.mul_mod a M 2 two, FRC.Nat.add_mod (p * A) k 2 two, FRC.Nat.mul_mod p A 2 two, hodd, Nat.one_mul,356      FRC.Nat.mod_mod A 2 two] at e357    exact e.symm358  have r2 : (A % 2 + B % 2 + 1) % 2 = a % 2 := by359    rw [← i1, FRC.Nat.add_mod (A + B) 1 2 two, FRC.Nat.add_mod A B 2 two, FRC.Nat.mod_add_mod _ _ 2 two]360  have r3 : (A % 2 + C % 2 + 1) % 2 = M % 2 := by361    rw [← i2, FRC.Nat.add_mod (A + C) 1 2 two, FRC.Nat.add_mod A C 2 two, FRC.Nat.mod_add_mod _ _ 2 two]362  have r4 : (C % 2 + D % 2 + 1) % 2 = (1 + a % 2) % 2 := by363    have e : ((p - a) % 2 + a % 2) % 2 = 1 := by364      rw [← FRC.Nat.add_mod (p - a) a 2 two, FRC.Nat.sub_add_cancel (Nat.le_of_lt ha)]; exact hodd365    rw [← odd_sum_residue _ (FRC.Nat.mod_lt' (p - a) two) _ (FRC.Nat.mod_lt' a two) e, ← i3,366      FRC.Nat.add_mod (C + D) 1 2 two, FRC.Nat.add_mod C D 2 two, FRC.Nat.mod_add_mod _ _ 2 two]367  have t := parity_table (a % 2) (FRC.Nat.mod_lt' a two) (M % 2) (FRC.Nat.mod_lt' M two) (A % 2)368    (FRC.Nat.mod_lt' A two) (B % 2) (FRC.Nat.mod_lt' B two) (C % 2) (FRC.Nat.mod_lt' C two) (D % 2)369    (FRC.Nat.mod_lt' D two) (k % 2) (FRC.Nat.mod_lt' k two) r1 r2 r3 r4370  rw [mu_mod]371  exact t372373374/-! ## The instance (13, 233): the pair, the sky, the flow and the meridians, decided by the kernel (38-s13) -/375376/-- The number of `x < n` with `P x` (as `Frame.natCount`, restated so that the subject theme stands without the frame file). -/377def count (P : Nat → Prop) [DecidablePred P] : Nat → Nat378  | 0 => 0379  | n + 1 => count P n + if P n then 1 else 0380381/-- 38:A1 — the Subject frame `(13; 3, 2)`: `2` generates `𝔽₁₃^×`. -/382theorem pair_frame : Frame 13 3 (2 : Shell 13) := ⟨rfl, Nat.zero_lt_succ 2, by decide +kernel⟩383384385/-- 38:A1, 38:A2 — the pair `(13, 233)`: `p = 13 = 4·3 + 1`, `Ω = 233 = 4·58 + 1`, the drive `g = 2` (`pair_frame`),386`i = 5 = −g³ = g⁹`, `i² = −1`, and the tower identity `g = 3·5` with `3 = g⁴`, `3³ = 1`, `5⁴ = 1`; the frame is `pair_frame`. -/387theorem pair_register :388    (13 : Nat) = 4 * 3 + 1 ∧ (233 : Nat) = 4 * 58 + 1 ∧ (12 : Nat) = 4 * 3 ∧ 58 % 4 = 2 ∧ 58 % 3 = 1 ∧ 13 * 13 < 233 ∧389    (5 : Shell 13) = -(2 ^ 3) ∧ (2 : Shell 13) ^ 9 = 5 ∧ (5 : Shell 13) * 5 = -1 ∧ (2 : Shell 13) ^ 4 = 3 ∧390    (3 : Shell 13) * 5 = 2 ∧ (3 : Shell 13) ^ 3 = 1 ∧ (5 : Shell 13) ^ 4 = 1 ∧ (2 : Shell 13) ^ 12 = 1 ∧391    (2 : Shell 13) ^ 6 = -1 ∧ 4 * 1 = 3 * 1 + 1 := by decide +kernel392393/-- 38:A3 — the channel at the instance: `gcd(12, 14) = 2`, `gcd(12, 28) = 4`, `N(i) = i² = −1` — as the divisor394facts the kernel decides: `2 ∣ 12, 14` and no `d > 2` divides both; `4 ∣ 12, 28` and no `d > 4` divides both. -/395theorem channel_instance :396    12 % 2 = 0 ∧ 14 % 2 = 0 ∧ (∀ d, d < 15 → 2 < d → ¬ (12 % d = 0 ∧ 14 % d = 0)) ∧397    12 % 4 = 0 ∧ 28 % 4 = 0 ∧ (∀ d, d < 29 → 4 < d → ¬ (12 % d = 0 ∧ 28 % d = 0)) ∧398    (5 : Shell 13) * 5 = -1 ∧ (5 : Shell 13) ^ 13 = 5 := by decide +kernel399400/-- 38:A4 — the Carrier frame `(233; 58, 78)` and its quarter roots: `78⁵⁸ = 89 = h`, `h² = −1`, `ħ = 144 = −h`,401`ħh = 1`, `ħ + h = 0` (`= Ω`), `78¹¹⁶ = −1`, `78²³² = 1`; the octant `ζ₈ = 97`: `97² = 89`, `97⁴ = −1`, `97⁸ = 1`;402the Fibonacci convergents `h = 13/8`, `ħ = 8/13` on `𝔽₂₃₃` and `233 = 13² + 8²`. -/403theorem carrier_frame : Frame 233 58 (78 : Shell 233) := ⟨rfl, Nat.zero_lt_succ 57, by decide +kernel⟩404405/-- 38:A4 — the Carrier quarter roots as the kernel decides them (the clauses of `carrier_frame`'s docstring), with406`78²⁹ = 97` and the Fibonacci steps `233 = 144 + 89`, `144 = 89 + 55`, `89 = 55 + 34`, `13 = 8 + 5`. -/407theorem carrier_roots :408    (78 : Shell 233) ^ 58 = 89 ∧ (89 : Shell 233) * 89 = -1 ∧ (144 : Shell 233) = -89 ∧ (144 : Shell 233) * 89 = 1 ∧409    (144 : Shell 233) + 89 = 0 ∧ (78 : Shell 233) ^ 116 = -1 ∧ (78 : Shell 233) ^ 232 = 1 ∧410    (97 : Shell 233) ^ 2 = 89 ∧ (97 : Shell 233) ^ 4 = -1 ∧ (97 : Shell 233) ^ 8 = 1 ∧ (78 : Shell 233) ^ 29 = 97 ∧411    (89 : Shell 233) * 8 = 13 ∧ (144 : Shell 233) * 13 = 8 ∧ (233 : Nat) = 13 * 13 + 8 * 8 ∧412    (233 : Nat) = 144 + 89 ∧ (144 : Nat) = 89 + 55 ∧ (89 : Nat) = 55 + 34 ∧ (13 : Nat) = 8 + 5 := by decide +kernel413414/-- 38:A6 — the FRC algebra half on `𝔽₁₃`: `2⁻¹ = 7`, `−2⁻¹ = 6`, `2·6 = −1`; the seam `13/2` lies between the rows415`6` and `7`. -/416theorem half_instance :417    (2 : Shell 13) * 7 = 1 ∧ (6 : Shell 13) = -7 ∧ (2 : Shell 13) * 6 = -1 ∧ 6 * 2 < 13 ∧ 13 < 7 * 2 := by418  decide +kernel419420/-- 38:A8, 38:B2 — the resolvable window at the instance: `4|k̂| < 13` exactly for `|k̂| ≤ 3`, the window `{0, ±1, ±2, ±3}`;421the symmetric heights `k̂ ∈ {−5, …, 6}` of `C₁₂`; two window heights sum within `6 < 12`. -/422theorem window_instance :423    (∀ k, k < 13 → (4 * k < 13 ↔ k ≤ 3)) ∧ (∀ k₁, k₁ < 4 → ∀ k₂, k₂ < 4 → k₁ + k₂ ≤ 6) ∧ 6 < 12 ∧424    (2 * 3 - 1 : Nat) = 5 ∧ (2 * 3 : Nat) = 6 := by decide +kernel425426/-! ## B. The sky -/427428/-- The retarded label of row `k` at chronon `t` on the Subject: the cell's residue times the drive state `t − k`,429one chronon of lookback per row. -/430def label (k t : Nat) : Shell 13 := ofNat k * 2 ^ ((t + 12 - k % 12) % 12)431432/-- 38:B1 — the node field `72 = 3·2·12` (three shells, two routes, twelve rows) and the retarded labels: every row's433label advances by the drive each chronon and returns after twelve. -/434theorem node_field :435    (3 : Nat) * 2 * 12 = 72 ∧436    (∀ k, k < 13 → ∀ t, t < 12 → label k (t + 1) = 2 * label k t ∧ label k (t + 12) = label k t) ∧437    (∀ k, k < 13 → label k k = ofNat k) := by decide +kernel438439/-- 38:B3 — the mounting: `×3 = g⁴` (four drive steps, `3³ = 1`), `120° = 8` steps of `C₂₄` (`8 = 24/3`),440quarter-blind (`8 ≡ 4 ≡ 0 mod 4`, `4 ≡ 1 mod 3`); the count `3·48 + 12 = 156 = 13·12`. -/441theorem mounting :442    (2 : Shell 13) ^ 4 = 3 ∧ (3 : Shell 13) ^ 3 = 1 ∧ (3 : Shell 13) ^ 2 = 9 ∧ (8 : Nat) * 15 = 120 ∧443    (3 : Nat) * 8 = 24 ∧ 8 % 4 = 0 ∧ 4 % 4 = 0 ∧ 4 % 3 = 1 ∧ (3 : Nat) * 48 + 12 = 156 ∧ (156 : Nat) = 13 * 12 := by444  decide +kernel445446/-- 38:B4 — the sky chronon `C₂₄` is the fibre product of `C₁₂` and `C₈` over `C₄`: the class-compatible pairs447number `12·8/4 = 24`, the map `C₂₄ → C₁₂ ×_{C₄} C₈` is injective, antipodal at `+12`, closed at `+24`; `232 = 8·29`. -/448theorem sky_chronon :449    count (fun n => (n / 8) % 4 = (n % 8) % 4) 96 = 24 ∧ (12 : Nat) * 8 = 24 * 4 ∧450    (∀ s, s < 24 → ∀ t, t < 24 → s % 12 = t % 12 → s % 8 = t % 8 → s = t) ∧451    (∀ s, s < 24 → (s + 12) % 24 ≠ s ∧ (s + 12 + 12) % 24 = s) ∧ (232 : Nat) = 8 * 29 := by decide +kernel452453/-- 38:B5, 38:C14 — the recurrence data at the instance: `696 = lcm(12, 232) = 58·12 = 3·232` is the least common454return, `1392 = 2·696` the spinor recurrence; the joint cycle's `ℓ = 87 = 3·29`: at `4ℓ = 348` the shell is home455(`348 ≡ 0 mod 12`) and the Carrier reads the half (`348 ≡ 116 mod 232`, `78³⁴⁸ = −1`), at `8ℓ = 696` both are home. -/456theorem recurrence :457    (696 : Nat) % 12 = 0 ∧ (696 : Nat) % 232 = 0 ∧ (696 : Nat) = 58 * 12 ∧ (696 : Nat) = 3 * 232 ∧458    (1392 : Nat) = 2 * 696 ∧ (∀ n, n < 696 → 0 < n → n % 12 = 0 → n % 232 ≠ 0) ∧459    (87 : Nat) = 3 * 29 ∧ (87 : Nat) = (2 * 1 + 1) * (2 * 14 + 1) ∧ (87 : Nat) = (2 * 14 + 1) * (2 * 1 + 1) ∧460    (4 * 87 : Nat) % 12 = 0 ∧ (4 * 87 : Nat) % 232 = 116 ∧ (2 : Shell 13) ^ 348 = 1 ∧ (78 : Shell 233) ^ 348 = -1 ∧461    (2 : Shell 13) ^ 696 = 1 ∧ (78 : Shell 233) ^ 696 = 1 := by decide +kernel462463/-- 38:B7 — the frame leak: the tick `π/116` reaches `π/2` at the quarter station `b_C = 58` (`58·4 = 232`), the halved464tick `π/232` being its reading on `C₄₆₄` (`1/464` of the turn); the composed rate `1/12 + 1/232 = 61/696`; between two (home, home) events every465class-compatible pair `(s mod 12, c mod 232)` occurs once: the pairs number `12·232/4 = 696` and the map466`t ↦ (t mod 12, t mod 232)` has trivial kernel on `[0, 696)`. -/467theorem frame_leak :468    (58 : Nat) * 4 = 232 ∧ (58 : Nat) * 2 = 116 ∧ (232 : Nat) * 2 = 464 ∧ (61 : Nat) * (12 * 232) = 696 * (232 + 12) ∧469    (12 : Nat) * 232 = 4 * 696 ∧470    count (fun n => (n / 232) % 4 = (n % 232) % 4) (12 * 232) = 696 ∧471    (∀ t, t < 696 → t % 12 = 0 → t % 232 = 0 → t = 0) := by decide +kernel472473/-! ## C. The flow -/474475/-- 38:C1, 38:C5, 38:D1 — the flow law as tick counts on `C₂₃₂` (`tick`): row `k` is home at `b_C = k` and at its476parity image (`116`) at `b_C = 116 + k`, for every row; the count returns the row at every clock state. -/477theorem flow_stations :478    (∀ k, k < 232 → tick 232 k k = 0 ∧ tick 232 k (116 + k) = 116) ∧479    (∀ b, b < 232 → ∀ k, k < 13 → (tick 232 k b + b) % 232 = k) ∧ (116 : Nat) = 232 / 2 := by480  decide +kernel481482/-- 38:C3 — ownership: the origin is no station (the capacity stations are `d` with `0 < d` and `4d < 13` or483`4(13 − d) < 13`, the set `{1, 2, 3, 10, 11, 12}`), and at every clock state the origin's count is the clock's own:484the rays anchor at the Observer. -/485theorem ownership :486    (∀ d, d < 13 → ((0 < d ∧ (4 * d < 13 ∨ 4 * (13 - d) < 13)) ↔487      (d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 10 ∨ d = 11 ∨ d = 12))) ∧488    (∀ b, b < 232 → (tick 232 0 b + b) % 232 = 0) := by decide +kernel489490/-- 38:C4 — the half turn on `C₄₆₄` at the instance: two half turns are the identity and the rim `232` is its own491reflection (`FRC.Pair.half_turn` in general). -/492theorem half_turn_instance :493    (∀ x, x < 464 → (x + 232 + 232) % 464 = x ∧ (x + (464 - x % 464)) % 464 = 0) ∧494    (464 - 232 % 464) % 464 = 232 := by decide +kernel495496/-- 38:C6 — the dilation instance `3/58 = 12/232` and the `(53, 13)` kill test in the auxiliary modulus `157`497(`53 = 4·13 + 1`; `S = 39 ≡ 3 mod 4`, not admissible): `5` primitive mod `157` (`5⁷⁸, 5⁵², 5¹² ≠ 1`, `5¹⁵⁶ = 1`), `5¹³ = 22`, `3 ∤ 13`, `22⁹ = 28 = 5⁻³⁹`, `22⁴` of order `3`, the idempotent498`117·13 ≡ 117 mod 156`, `5³⁹ = 129`; `12/52 = 3/13`, `lcm(12, 52) = 156` with the half event at `78`. -/499theorem kill_test :500    (3 : Nat) * 232 = 58 * 12 ∧ (53 : Nat) = 4 * 13 + 1 ∧ (157 : Nat) = 4 * 39 + 1 ∧ 39 % 4 = 3 ∧501    (5 : Shell 157) ^ 78 ≠ 1 ∧ (5 : Shell 157) ^ 52 ≠ 1 ∧ (5 : Shell 157) ^ 12 ≠ 1 ∧ (5 : Shell 157) ^ 156 = 1 ∧502    (5 : Shell 157) ^ 13 = 22 ∧ 13 % 3 ≠ 0 ∧503    (22 : Shell 157) ^ 9 = 28 ∧ (5 : Shell 157) ^ 39 * 28 = 1 ∧ (22 : Shell 157) ^ 4 ≠ 1 ∧504    ((22 : Shell 157) ^ 4) ^ 3 = 1 ∧ (117 : Nat) * 13 % 156 = 117 ∧ (5 : Shell 157) ^ 39 = 129 ∧505    (12 : Nat) * 13 = 52 * 3 ∧ (156 : Nat) % 12 = 0 ∧ (156 : Nat) % 52 = 0 ∧506    (∀ n, n < 156 → 0 < n → n % 12 = 0 → n % 52 ≠ 0) ∧ (78 : Nat) * 2 = 156 := by decide +kernel507508/-- 38:C7, 38:C10, 38:X1 — the two faces at the instance: the angular face `12/232 = 3/58 = κ/S`, the temporal face509`12/464 = 3/116 = κ/(2S)`, their ratio `2`; the per-chronon rate `1/232` at `(13, 233)` and at `(5, 233)`. -/510theorem two_faces :511    (12 : Nat) * 58 = 3 * 232 ∧ (12 : Nat) * 116 = 3 * 464 ∧ (3 : Nat) * 116 = 2 * (3 * 58) ∧512    (3 : Nat) * (4 * 58) = 58 * (13 - 1) ∧ (1 : Nat) * (4 * 58) = 58 * (5 - 1) ∧ (4 : Nat) * 58 = 233 - 1 ∧513    (3 : Nat) * 58 = 174 := by decide +kernel514515/-! ## D. The meridians and the covering -/516517/-- The tent fold of `u = mt` on `𝔽₁₃`: the row `u − 13w` on an even sheet `w = ⌊u/13⌋`, `13(w + 1) − u` on an odd one. -/518def tent (p u : Nat) : Nat := if (u / p) % 2 = 0 then u - p * (u / p) else p * (u / p + 1) - u519520/-- The sheet parity of the slot `(m, t)`: the route flips on odd sheets. -/521def sheet (p m t : Nat) : Nat := (m * t / p) % 2522523/-- The shell of the parameter `t`: `min(t, p − t) − 1`. -/524def shellOf (p t : Nat) : Nat := (if t ≤ p - t then t else p - t) - 1525526/-- A parameter is a station of capacity `κ`: `1 ≤ t ≤ κ` or `p − κ ≤ t ≤ p − 1`. -/527def isParam (p κ t : Nat) : Bool := (1 ≤ t && t ≤ κ) || (p - κ ≤ t && t ≤ p - 1)528529/-- The multiplicity of the node (shell `s`, route `e`, row `k`) under the covering by the windings `1..p − 1`, both530rays and the stations: the slots are indexed by `n < (p − 1)·2·p` as `m = n / (2p) + 1`, ray `= (n / p) % 2`,531`t = n % p`. -/532def mult (p κ s e k : Nat) : Nat :=533  count (fun n => isParam p κ (n % p) = true ∧ shellOf p (n % p) = s ∧534    ((n / p) % 2 + sheet p (n / (2 * p) + 1) (n % p)) % 2 = e ∧ tent p ((n / (2 * p) + 1) * (n % p)) = k)535    ((p - 1) * 2 * p)536537/-- 38:D1 — the capacity stations `4d < 13` select `{1, 2, 3, 10, 11, 12}` (shells `0, 1, 2` twice); the threading538on all `232` states is `flow_stations`. -/539theorem stations :540    (∀ t, t < 13 → (isParam 13 3 t = true ↔ (t = 1 ∨ t = 2 ∨ t = 3 ∨ t = 10 ∨ t = 11 ∨ t = 12))) ∧541    shellOf 13 1 = 0 ∧ shellOf 13 2 = 1 ∧ shellOf 13 3 = 2 ∧ shellOf 13 10 = 2 ∧ shellOf 13 11 = 1 ∧542    shellOf 13 12 = 0 ∧ count (fun t => isParam 13 3 t = true) 13 = 6 := by decide +kernel543544/-- 38:D2 — the step law `11π/12 + π/13 + π/232 = π − (π/156 − π/232)` as exact fractions of `π/9048`545(`9048 = lcm(12, 13, 232)`): `8294 + 696 + 39 = 9029 = 9048 − (58 − 39)`; `156 = 13·12`. -/546theorem step_law :547    (9048 : Nat) = 12 * 754 ∧ (11 : Nat) * 754 = 8294 ∧ (13 : Nat) * 696 = 9048 ∧ (232 : Nat) * 39 = 9048 ∧548    (156 : Nat) * 58 = 9048 ∧ (8294 : Nat) + 696 + 39 = 9029 ∧ (9048 : Nat) - (58 - 39) = 9029 ∧549    (156 : Nat) = 13 * 12 ∧ (232 : Nat) = 233 - 1 ∧ (9048 : Nat) % 12 = 0 ∧ (9048 : Nat) % 13 = 0 ∧550    (9048 : Nat) % 232 = 0 := by decide +kernel551552/-- 38:D3 — the scale-tower circuit: the tower's period is the drive's, `4κ = 12 = p − 1`, with the period points553`0`, `13/2` (the seam, `2·6 < 13 < 2·7`) and `13`. -/554theorem tower_period :555    (4 : Nat) * 3 = 12 ∧ (12 : Nat) = 13 - 1 ∧ (2 : Shell 13) ^ 12 = 1 ∧ (∀ k, k < 12 → 0 < k → (2 : Shell 13) ^ k ≠ 1) ∧556    2 * 6 < 13 ∧ 13 < 2 * 7 := by decide +kernel557558/-- 38:D5 — the four rays and the four quarter classes on `𝔽₁₃`: the classes of `dlog mod 4` number three cells559each, the quarter `i = g⁹` carries class `1` and `−1 = g⁶` class `2`; the quarter fold `a = 13/4` lies between560`3` and `4` (`4·3 < 13 < 4·4`). -/561theorem quarter_classes :562    (∀ c, c < 4 → count (fun j => j % 4 = c) 12 = 3) ∧ 9 % 4 = 1 ∧ 6 % 4 = 2 ∧ (2 : Shell 13) ^ 9 = 5 ∧563    (2 : Shell 13) ^ 6 = -1 ∧ 4 * 3 < 13 ∧ 13 < 4 * 4 := by decide +kernel564565/-- 38:D6, 38:D13 — the momentum dual `M₃` at winding `5 = g⁹ = −g³`: its stations on the tent shells are the rows566`5, 10, 11` (direct, `t = 1, 2, 3`) and `2, 3, 8` (echo, `t = 10, 11, 12`), the route flipping on the odd sheets567(`t = 3, 10`); the fold is `C₂₆`-periodic; the axis passages `t = 13j/5` drawn are `13/5` and `52/5`. -/568theorem momentum_dual :569    (2 : Shell 13) ^ 9 = 5 ∧ (5 : Shell 13) = -(2 ^ 3) ∧570    tent 13 (5 * 1) = 5 ∧ tent 13 (5 * 2) = 10 ∧ tent 13 (5 * 3) = 11 ∧ tent 13 (5 * 10) = 2 ∧571    tent 13 (5 * 11) = 3 ∧ tent 13 (5 * 12) = 8 ∧572    sheet 13 5 1 = 0 ∧ sheet 13 5 2 = 0 ∧ sheet 13 5 3 = 1 ∧ sheet 13 5 10 = 1 ∧ sheet 13 5 11 = 0 ∧573    sheet 13 5 12 = 0 ∧ (∀ u, u < 200 → tent 13 (u + 26) = tent 13 u) ∧574    4 * 13 ≤ 13 * 5 ∧ 39 * 5 ≤ 4 * 52 ∧ ¬ (4 * 26 ≤ 13 * 5 ∨ 39 * 5 ≤ 4 * 26) ∧575    ¬ (4 * 39 ≤ 13 * 5 ∨ 39 * 5 ≤ 4 * 39) := by decide +kernel576577/-- 38:D7, 38:D13 — the covering at the instance: `144` slots (twelve windings, two rays, six stations) over the578`72` nodes, every node of multiplicity `3` on the even rows and `1` on the odd rows: `36` once and `36` thrice,579`144 = 36 + 108`; winding `1` is `M₀` (rows `t`, no flip) and winding `5` is `M₃`. -/580theorem covering_instance :581    count (fun n => isParam 13 3 (n % 13) = true) (12 * 2 * 13) = 144 ∧ (3 : Nat) * 2 * 12 = 72 ∧582    (∀ s, s < 3 → ∀ e, e < 2 → ∀ k, k < 13 → 0 < k → mult 13 3 s e k = if k % 2 = 0 then 3 else 1) ∧583    (36 : Nat) * 1 + 36 * 3 = 144 ∧ (3 : Nat) * 2 * 6 = 36 ∧584    (∀ t, t < 13 → isParam 13 3 t = true → tent 13 (1 * t) = t ∧ sheet 13 1 t = 0) := by decide +kernel585586/-- 38:D8 — the half-cell ramification `t_{1/2} = 13/(2m)` lies in the drawn first segment `[0, 13/4]` for every587sibling `m ≥ 2` (`4·13 ≤ 13·2m`) and not for `M₀` (`m = 1`, `13/2` the seam); the axis passage `13/m` is drawn588exactly for `m ≥ 4`. -/589theorem ramification :590    (∀ m, m < 13 → 2 ≤ m → 4 * 13 ≤ 13 * (2 * m)) ∧ ¬ (4 * 13 ≤ 13 * 2) ∧ (2 * 6 < 13 ∧ 13 < 2 * 7) ∧591    (∀ m, m < 13 → 1 ≤ m → (4 * 13 ≤ 13 * m ↔ 4 ≤ m)) := by decide +kernel592593/-- 38:D9 — the horizon fold fusion `5·39 ≡ −13 (mod 104)`: `5·39 + 13 = 208 = 2·104`, `104 = 8·13`, `39 = 3·13`;594eight ray ends fuse into four points (`8 = 2·4`). -/595theorem fusion :596    (5 : Nat) * 39 + 13 = 2 * 104 ∧ (5 * 39 + 13 : Nat) % 104 = 0 ∧ (104 : Nat) = 8 * 13 ∧ (39 : Nat) = 3 * 13 ∧597    (8 : Nat) = 2 * 4 := by decide +kernel598599/-- The inverse of a shell index `a ∈ {1, 2, 3}` on `𝔽₁₃`: `1, 7, 9`. -/600def inv13 (a : Nat) : Nat := if a = 1 then 1 else if a = 2 then 7 else 9601602/-- 38:D12 at the instance — the reflection identity `⌊ab/13⌋ + ⌊(13 − a)b/13⌋ + 1 = b` for all `0 < a, b < 13`,603and the parity decider: for every node (shell `a ∈ {1, 2, 3}`, row `k`), with `M = k a⁻¹`, the four candidate wraps604give `μ = 3` on the even rows and `1` on the odd rows (`FRC.Pair.mu`); the general theorem is605`covering_parity`. -/606theorem parity_instance :607    (∀ a, a < 13 → 0 < a → ∀ b, b < 13 → 0 < b → a * b / 13 + (13 - a) * b / 13 + 1 = b) ∧608    (∀ a, a < 4 → 0 < a → a * inv13 a % 13 = 1) ∧609    (∀ a, a < 4 → 0 < a → ∀ k, k < 13 → 0 < k →610      mu (a * (k * inv13 a % 13) / 13) ((13 - k * inv13 a % 13) * a / 13)611        ((k * inv13 a % 13) * (13 - a) / 13) ((13 - k * inv13 a % 13) * (13 - a) / 13) =612        if k % 2 = 0 then 3 else 1) := by decide +kernel613614/-- 38:D12, 38:D7 — the parity decider agrees with the covering at the instance: for every node (shell `a ∈ {1, 2, 3}`,615row `k`) on either route, the multiplicity counted over the `144` slots (`mult`) is the decider's value (`mu`). -/616theorem mult_eq_mu :617    ∀ a, a < 4 → 0 < a → ∀ e, e < 2 → ∀ k, k < 13 → 0 < k →618      mult 13 3 (a - 1) e k =619        mu (a * (k * inv13 a % 13) / 13) ((13 - k * inv13 a % 13) * a / 13)620          ((k * inv13 a % 13) * (13 - a) / 13) ((13 - k * inv13 a % 13) * (13 - a) / 13) := by decide +kernel621622end FRC.Pair623