Theme/Composite.lean — FrcCore

1import FrcCore.Theme.Observation23/-!4# FrcCore.Theme.Composite — the quantum theme: composites, correlations and the channel (22-quantum, 15 October 2026)56The composite formalism of 22-quantum in the shadow: a reading Subject's one drive acts diagonally on a cluster, the7offset is its conserved label, and the Bell configuration's identities are ring identities on every shell.89* the `m`-body cluster: the offset vector is drive-invariant and two configurations share an orbit exactly when their10  offset vectors agree (`offset_invariant`, `cluster_offset`, 22:C15); the winding `s` on `C_n` has period11  `n/gcd(s, n)` (`winding_period`, 22:C26);12* the synchronised orbit adds coherently, `|Σ_i χ(u_i)|² = m²`, against the offset-uniform average `m`13  (`locked_norm`, `spread_average`, 22:C15, C22); the field of `m` locked sources is `m` times one, and the14  acceleration of a test cluster is mass-free, `η = 0` (`field_linear`, `eta_zero`, 22:C22);15* the doublet readout is `σ_x` through the half-turn `v⁸ = −1` (`half_turn_sixteen`, `doublet_readout`, 22:C16);16* the Tsirelson square `S² = 8` for `S = 2(ζ + ζ⁷)`, `ζ⁴ = −1`, and no-signalling (`singlet_square`, `no_signalling`,17  22:C17, X7, P3);18* the channel complementarity `V² + C² = 1` on every shell, the product at zero coupling (`channel_complementarity`,19  `channel_product_at_zero`, 22:C19, P1);20* the drive conserves the ledger norm and the visibility revives at the recurrence (`drive_norm`, `revival`, 22:C20);21* the coherent fraction: the branch phase of `m_c` synchronised cells, the pairwise product law, the complete spread22  cancels, and the reduced channel factorises (`branch_phase`, `pair_product`, `spread_cancels`, `channel_assembly`,23  22:C21);24* inter-Subject consistency: the channels of two Subjects agree on the common core, and the joint refinement is the25  common core's partition (`order_independence`, `joint_refinement`, 22:C23, X4).2627No axioms.28-/2930namespace FRC.Composite3132open FRC.Shell33open FRC.Shell.Prime34open FRC.Quantum35open FRC.Observation3637variable {q : Nat} [Pos q]3839/-! ## 22:C15 — the cluster's offset is a conserved label -/4041/-- 22:C15 — the offset vector of a cluster on `(ℤ/N)^m` is invariant under the diagonal drive by `t` chronons:42in the cross form, `x_j + (x_0 + t) ≡ (x_j + t) + x_0 (mod N)`. -/43theorem offset_invariant {N : Nat} (hN : 0 < N) (t : Nat) (x : Nat → Nat) (j : Nat) :44    (x j + (x 0 + t) % N) % N = ((x j + t) % N + x 0) % N := by45  rw [FRC.Nat.add_mod_mod _ _ _ hN, FRC.Nat.mod_add_mod _ _ _ hN, ← Nat.add_assoc, Nat.add_right_comm]4647/-- 22:C15, lem:mbody (i)–(ii), 22:C18 — the offset is the orbit label: two configurations `x, y` of the cluster `(ℤ/N)^m`48(`0 < m`, `y` reduced) lie on one orbit of the diagonal drive exactly when their offset vectors agree,49`x_j − x_0 ≡ y_j − y_0 (mod N)` for every cell `j`; the drive time `t` is a residue, `t < N`, and no drive evolution50connects distinct offsets. -/51theorem cluster_offset {N m : Nat} (hN : 0 < N) (hm : 0 < m) (x y : Nat → Nat) (hy : ∀ j, j < m → y j < N) :52    (∃ t, t < N ∧ ∀ j, j < m → (x j + t) % N = y j) ↔ ∀ j, j < m → (x j + y 0) % N = (y j + x 0) % N := by53  constructor54  · intro ⟨t, _, ht⟩ j hj55    rw [← ht 0 hm, ← ht j hj]56    exact offset_invariant hN t x j57  · intro h58    refine ⟨(y 0 + (N - x 0 % N)) % N, Nat.mod_lt _ hN, fun j hj => ?_⟩59    rw [FRC.Nat.add_mod_mod _ _ _ hN]60    match FRC.Nat.mod_spec N hN (x 0) with61    | ⟨k, hk⟩ =>62      have hr : x 0 % N < N := Nat.mod_lt _ hN63      calc (x j + (y 0 + (N - x 0 % N))) % N = ((x j + y 0) % N + (N - x 0 % N)) % N := by64            rw [FRC.Nat.mod_add_mod _ _ _ hN, Nat.add_assoc]65        _ = ((y j + x 0) % N + (N - x 0 % N)) % N := by rw [h j hj]66        _ = (y j + x 0 + (N - x 0 % N)) % N := FRC.Nat.mod_add_mod _ _ _ hN67        _ = (N * (k + 1) + y j) % N := by68            congr 169            calc y j + x 0 + (N - x 0 % N) = y j + (N * k + x 0 % N + (N - x 0 % N)) := by rw [← hk, Nat.add_assoc]70              _ = y j + (N * k + N) := by rw [Nat.add_assoc (N * k), FRC.Nat.add_sub_of_le (Nat.le_of_lt hr)]71              _ = N * (k + 1) + y j := by rw [Nat.mul_succ, Nat.add_comm]72        _ = y j := by rw [FRC.Nat.add_mul_mod_self_left _ _ _ hN, FRC.Nat.mod_eq_of_lt (hy j hj)]7374/-! ## 22:C26 — the period of a winding -/7576/-- 22:C26 — the winding `s` on the cycle `C_n` has period `n/gcd(s, n)`: with `n = d n'`, `s = d s'` and `d` the gcd77(`s' u = n' v + 1` the Bezout witness of coprimality), the drive `x ↦ x + s` returns, `s t ≡ 0 (mod n)`, exactly when78`n' ∣ t`; the joint recurrence of a composite is then the lcm of these periods (`FRC.Quantum.joint_recurrence`). -/79theorem winding_period {n s d n' s' u v : Nat} (hd : 0 < d) (hn' : 0 < n') (hn : n = d * n') (hs : s = d * s')80    (hbez : s' * u = n' * v + 1) (t : Nat) : (s * t) % n = 0 ↔ t % n' = 0 := by81  have hn0 : 0 < n := by rw [hn]; exact Nat.mul_pos hd hn'82  constructor83  · intro h84    obtain ⟨c, hc⟩ := eq_mul_of_mod_zero hn0 h85    rw [hn, hs, FRC.Nat.mul_assoc, FRC.Nat.mul_assoc] at hc86    have e1 : s' * t = n' * c := Nat.eq_of_mul_eq_mul_left hd hc87    have e : n' * (v * t) + t = n' * (u * c) := by88      calc n' * (v * t) + t = (n' * v + 1) * t := by rw [FRC.Nat.add_mul, Nat.one_mul, FRC.Nat.mul_assoc]89        _ = s' * u * t := by rw [hbez]90        _ = u * (s' * t) := by rw [Nat.mul_comm s' u, FRC.Nat.mul_assoc]91        _ = n' * (u * c) := by rw [e1, FRC.Nat.mul_left_comm]92    calc t % n' = (n' * (v * t) + t) % n' := (FRC.Nat.add_mul_mod_self_left _ _ _ hn').symm93      _ = 0 := by rw [e]; exact mod_zero_of_eq_mul hn' rfl94  · intro h95    obtain ⟨c, hc⟩ := eq_mul_of_mod_zero hn' h96    refine mod_zero_of_eq_mul (q := s' * c) hn0 ?_97    rw [hc, hs, hn, FRC.Nat.mul_assoc, FRC.Nat.mul_assoc, FRC.Nat.mul_left_comm s']9899/-! ## The locked cluster against the spread: `m²` against `m` -/100101/-- lem:mbody (iii), 22:C15, 22:C22 — on the synchronised orbit the amplitudes add coherently: `Σ_{i<m} χ = m χ`, and the102weight `(m χ)(m χ̄) = m²` when `χ χ̄ = 1`. -/103theorem locked_norm (m : Nat) {χ χbar : Shell q} (h : χ * χbar = 1) :104    sumRange (fun _ => χ) m = ofNat m * χ ∧ sumRange (fun _ => χ) m * sumRange (fun _ => χbar) m = ofNat (m * m) := by105  refine ⟨sum_const χ m, ?_⟩106  rw [sum_const, sum_const, mul_mul_mul_comm, h, mul_one, ofNat_mul]107108/-- The sum of `F` over all configurations `v : Nat → Nat` of the cluster with `v_j < n` for `j < m` and `v_j = 0`109beyond, by recursion on the number of cells. -/110def tsum (n : Nat) (F : (Nat → Nat) → Shell q) : Nat → Shell q111  | 0 => F (fun _ => 0)112  | m + 1 => sumRange (fun θ => tsum n (fun v => F (fun j => if j = m then θ else v j)) m) n113114theorem tsum_zero (n : Nat) (F : (Nat → Nat) → Shell q) : tsum n F 0 = F (fun _ => 0) := rfl115116theorem tsum_succ (n : Nat) (F : (Nat → Nat) → Shell q) (m : Nat) :117    tsum n F (m + 1) = sumRange (fun θ => tsum n (fun v => F (fun j => if j = m then θ else v j)) m) n := rfl118119/-- The configuration sum depends on `F` pointwise. -/120theorem tsum_congr (n : Nat) {F G : (Nat → Nat) → Shell q} (h : ∀ v, F v = G v) : ∀ m, tsum n F m = tsum n G m121  | 0 => h _122  | m + 1 => by123    rw [tsum_succ, tsum_succ]124    exact sum_congr n (fun θ _ => tsum_congr n (fun v => h _) m)125126/-- The configuration sum is additive. -/127theorem tsum_add (n : Nat) (F G : (Nat → Nat) → Shell q) : ∀ m, tsum n (fun v => F v + G v) m = tsum n F m + tsum n G m128  | 0 => rfl129  | m + 1 => by130    rw [tsum_succ, tsum_succ, tsum_succ, ← sum_add]131    exact sum_congr n (fun θ _ => tsum_add n _ _ m)132133/-- The configuration sum of a constant: `n^m c`. -/134theorem tsum_const (n : Nat) (c : Shell q) : ∀ m, tsum n (fun _ => c) m = ofNat (n ^ m) * c135  | 0 => by rw [tsum_zero]; exact (one_mul c).symm136  | m + 1 => by137    rw [tsum_succ, sum_congr n (fun θ _ => tsum_const n c m), sum_const, ← mul_assoc, ofNat_mul, Nat.pow_succ,138      Nat.mul_comm]139140/-- The configuration sum of a scalar multiple. -/141theorem tsum_mul_left (n : Nat) (c : Shell q) (F : (Nat → Nat) → Shell q) :142    ∀ m, tsum n (fun v => c * F v) m = c * tsum n F m143  | 0 => rfl144  | m + 1 => by145    rw [tsum_succ, tsum_succ, ← sum_mul_left]146    exact sum_congr n (fun θ _ => tsum_mul_left n c _ m)147148theorem tsum_mul_right (n : Nat) (c : Shell q) (F : (Nat → Nat) → Shell q) (m : Nat) :149    tsum n (fun v => F v * c) m = tsum n F m * c := by150  rw [tsum_congr n (fun v => mul_comm (F v) c), tsum_mul_left, mul_comm]151152/-- The configuration sum of a sum over cells. -/153theorem tsum_sum (n m : Nat) (G : Nat → (Nat → Nat) → Shell q) :154    ∀ k, tsum n (fun v => sumRange (fun i => G i v) k) m = sumRange (fun i => tsum n (G i) m) k155  | 0 => by rw [tsum_congr n (fun v => sumRange_zero (fun i => G i v)), tsum_const, mul_zero, sumRange_zero]156  | k + 1 => by157    rw [sumRange_succ, tsum_congr n (fun v => sumRange_succ (fun i => G i v) k), tsum_add, tsum_sum n m G k]158159/-- A character of one cell `i < m` sums to zero over the configurations: `Σ_v ζ^{c + v_i} = 0` for `ζ` of order `n`,160`ζ ≠ 1`. -/161theorem tsum_cell (hq : FRC.Nat.isPrime q) {ζ : Shell q} {n : Nat} (hζ : HasOrder ζ n) (hζ1 : ζ ≠ 1) (c : Nat) :162    ∀ m i, i < m → tsum n (fun v => ζ ^ (c + v i)) m = 0163  | 0, i, hi => absurd hi (Nat.not_lt_zero i)164  | m + 1, i, hi => by165    rw [tsum_succ]166    match Nat.decEq i m with167    | .isTrue e =>168      subst e169      have e1 : ∀ θ, θ < n → tsum n (fun v => ζ ^ (c + (fun j => if j = i then θ else v j) i)) i =170          ofNat (n ^ i) * (ζ ^ c * ζ ^ θ) := fun θ _ => by171        dsimp only172        rw [tsum_congr n (fun v => by rw [if_pos rfl, pow_add]), tsum_const]173      rw [sum_congr n e1, sum_mul_left, sum_mul_left, geom_sum_zero hq n hζ.2.1 hζ1, mul_zero, mul_zero]174    | .isFalse e =>175      have hi' : i < m := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hi) e176      have e1 : ∀ θ, θ < n → tsum n (fun v => ζ ^ (c + (fun j => if j = m then θ else v j) i)) m = 0 := fun θ _ => by177        dsimp only178        rw [tsum_congr n (fun v => by rw [if_neg e]), tsum_cell hq hζ hζ1 c m i hi']179      rw [sum_congr n e1]180      exact sum_zero n (fun _ _ => rfl)181182/-- Two distinct cells `i ≠ j` carrying the characters `ζ`, `η` of order `n` (neither `1`) sum to zero over the183configurations. -/184theorem tsum_cross (hq : FRC.Nat.isPrime q) {ζ η : Shell q} {n : Nat} (hζ : HasOrder ζ n) (hζ1 : ζ ≠ 1)185    (hη : HasOrder η n) (hη1 : η ≠ 1) (c c' : Nat) :186    ∀ m i j, i < m → j < m → i ≠ j → tsum n (fun v => ζ ^ (c + v i) * η ^ (c' + v j)) m = 0187  | 0, i, _, hi, _, _ => absurd hi (Nat.not_lt_zero i)188  | m + 1, i, j, hi, hj, hij => by189    rw [tsum_succ]190    match Nat.decEq i m, Nat.decEq j m with191    | .isTrue ei, _ =>192      subst ei193      have hj' : j < i := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (fun e => hij e.symm)194      have e1 : ∀ θ, θ < n → tsum n (fun v => ζ ^ (c + (fun l => if l = i then θ else v l) i) *195          η ^ (c' + (fun l => if l = i then θ else v l) j)) i = ζ ^ (c + θ) * 0 := fun θ _ => by196        dsimp only197        rw [tsum_congr n (fun v => by rw [if_pos rfl, if_neg (Nat.ne_of_lt hj')]), tsum_mul_left,198          tsum_cell hq hη hη1 c' i j hj']199      rw [sum_congr n e1]200      exact sum_zero n (fun _ _ => mul_zero _)201    | .isFalse ei, .isTrue ej =>202      subst ej203      have hi' : i < j := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hi) ei204      have e1 : ∀ θ, θ < n → tsum n (fun v => ζ ^ (c + (fun l => if l = j then θ else v l) i) *205          η ^ (c' + (fun l => if l = j then θ else v l) j)) j = 0 * η ^ (c' + θ) := fun θ _ => by206        dsimp only207        rw [tsum_congr n (fun v => by rw [if_pos rfl, if_neg ei]), tsum_mul_right, tsum_cell hq hζ hζ1 c j i hi']208      rw [sum_congr n e1]209      exact sum_zero n (fun _ _ => zero_mul _)210    | .isFalse ei, .isFalse ej =>211      have hi' : i < m := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hi) ei212      have hj' : j < m := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) ej213      have e1 : ∀ θ, θ < n → tsum n (fun v => ζ ^ (c + (fun l => if l = m then θ else v l) i) *214          η ^ (c' + (fun l => if l = m then θ else v l) j)) m = 0 := fun θ _ => by215        dsimp only216        rw [tsum_congr n (fun v => by rw [if_neg ei, if_neg ej]), tsum_cross hq hζ hζ1 hη hη1 c c' m i j hi' hj' hij]217      rw [sum_congr n e1]218      exact sum_zero n (fun _ _ => rfl)219220/-- lem:mbody (iii), 22:C22, 22:C15 — **the offset-uniform average is `m`**: for `m` cells with independent uniform phases221on a cycle of order `n` (`ζ` of order `n`, `η = ζ⁻¹`, neither `1`), the sum over all `n^m` configurations of222`|Σ_i ζ^{v_i}|² = (Σ_i ζ^{v_i})(Σ_j η^{v_j})` is `m n^m`, the average `m`, against `m²` on the synchronised orbit:223the `√m` lives only in amplitude-coherent observables. -/224theorem spread_average (hq : FRC.Nat.isPrime q) {ζ η : Shell q} {n : Nat} (hζ : HasOrder ζ n) (hζ1 : ζ ≠ 1)225    (hη : HasOrder η n) (hη1 : η ≠ 1) (hζη : ζ * η = 1) (m : Nat) :226    tsum n (fun v => sumRange (fun i => ζ ^ (v i)) m * sumRange (fun j => η ^ (v j)) m) m = ofNat m * ofNat (n ^ m) := by227  rw [tsum_congr n (fun v => sum_mul_sum _ _ m m), tsum_sum]228  have e1 : ∀ i, i < m → tsum n (fun v => sumRange (fun j => ζ ^ (v i) * η ^ (v j)) m) m = ofNat (n ^ m) := fun i hi => by229    rw [tsum_sum]230    have e2 : ∀ j, j < m → tsum n (fun v => ζ ^ (v i) * η ^ (v j)) m = if j = i then ofNat (n ^ m) else 0 := fun j hj => by231      match Nat.decEq j i with232      | .isTrue e =>233        subst e234        rw [if_pos rfl, tsum_congr n (fun v => by rw [← mul_pow, hζη, one_pow]), tsum_const, mul_one]235      | .isFalse e =>236        rw [if_neg e]237        have := tsum_cross hq hζ hζ1 hη hη1 0 0 m i j hi hj (fun e' => e e'.symm)238        rw [tsum_congr n (fun v => by rw [Nat.zero_add, Nat.zero_add]) m] at this239        exact this240    rw [sum_congr m e2, sum_eq_single (f := fun j => if j = i then ofNat (n ^ m) else 0) hi241      (fun j _ hne => if_neg hne), if_pos rfl]242  rw [sum_congr m e1, sum_const]243244/-- 22:C22 (i) — the stationary field is linear in its sources with coefficient exactly `m` per locked cluster of `m`245cells: `Σ_{i<m} u = m u`. -/246theorem field_linear (m : Nat) (u : Shell q) : sumRange (fun _ => u) m = ofNat m * u := sum_const u m247248/-- 22:C22 (ii) — the exact equivalence-principle null: the pull `m_t ∇u` on a locked test cluster against its inertia249`m_t` gives the acceleration `∇u` for every `m_t` (`w = m_t⁻¹`), so `η = 0` identically. -/250theorem eta_zero (mt w g : Shell q) (hw : mt * w = 1) : (mt * g) * w = g := by251  rw [mul_assoc, mul_comm g w, ← mul_assoc, hw, one_mul]252253/-! ## 22:C16 — the doublet readout is `σ_x` -/254255/-- 22:C16 — an element of order `16` has `v⁸ = −1`: the half-turn supplies the sign. -/256theorem half_turn_sixteen (hq : FRC.Nat.isPrime q) {v : Shell q} (hv : HasOrder v 16) : v ^ 8 = -1 := by257  have hsq : v ^ 8 * v ^ 8 = 1 := by rw [← pow_add]; exact hv.2.1258  match sq_eq_one hq hsq with259  | .inl e => exact absurd e (hv.2.2 8 (by decide) (by decide))260  | .inr e => exact e261262/-- The square of an element of order `16` has order `8`. -/263theorem order_eight_of_sixteen (hq : FRC.Nat.isPrime q) {v : Shell q} (hv : HasOrder v 16) : HasOrder (v ^ 2) 8 := by264  refine ⟨by decide, by rw [← pow_mul]; exact hv.2.1, fun l hl hl0 e => ?_⟩265  rw [← pow_mul] at e266  exact hv.2.2 (2 * l) (Nat.mul_lt_mul_of_pos_left hl (by decide)) (Nat.mul_pos (by decide) hl0) e267268/-- 22:C16 — **the forced readout is `σ_x`**: on the `C_{16}` Object `⟨v⟩` read by a core-`C_8` Subject269(`ω = v²` the core's generator), the doublet state `u^k + λ u^{k+8}` registers on the matched channel `r = k mod 8`270over the two cosets `s ∈ {0, 1}` (the fibre `v^s ⟨ω⟩`) as `Ψ(s) = 8 v^{sk} (1 + λ (v⁸)^s)`, that is `Ψ(0) = 8(1 + λ)`271and `Ψ(1) = 8 v^k (1 − λ)` by the half-turn `v⁸ = −1` (`half_turn_sixteen`). -/272theorem doublet_readout (hq : FRC.Nat.isPrime q) {v : Shell q} (hv : HasOrder v 16) (k s : Nat) (lam : Shell q) :273    sumRange (fun j => ((v ^ s * (v ^ 2) ^ j) ^ k + lam * (v ^ s * (v ^ 2) ^ j) ^ (k + 8)) *274      (v ^ 2) ^ ((8 - k % 8) * j)) 8 = ofNat 8 * (v ^ (s * k) * (1 + lam * (v ^ 8) ^ s)) := by275  have hω := order_eight_of_sixteen hq hv276  have e1 : ∀ j, ((v ^ s * (v ^ 2) ^ j) ^ k + lam * (v ^ s * (v ^ 2) ^ j) ^ (k + 8)) * (v ^ 2) ^ ((8 - k % 8) * j) =277      (v ^ (s * k) * (1 + lam * (v ^ 8) ^ s)) * ((v ^ 2) ^ (k * j) * (v ^ 2) ^ ((8 - k % 8) * j)) := fun j => by278    have h8 : ((v ^ 2) ^ j) ^ 8 = 1 := by rw [pow_mul_comm, hω.2.1, one_pow]279    have ha : (v ^ s * (v ^ 2) ^ j) ^ k = v ^ (s * k) * (v ^ 2) ^ (k * j) := by280      rw [mul_pow, ← pow_mul v s k, ← pow_mul (v ^ 2) j k, Nat.mul_comm j k]281    have hb : (v ^ s * (v ^ 2) ^ j) ^ (k + 8) = v ^ (s * k) * (v ^ 8) ^ s * (v ^ 2) ^ (k * j) := by282      rw [mul_pow, pow_add, pow_add, h8, mul_one, ← pow_mul v s k, ← pow_mul v s 8, ← pow_mul (v ^ 2) j k,283        Nat.mul_comm s 8, pow_mul v 8 s, Nat.mul_comm j k]284    rw [ha, hb]285    exact Shell.Frame.RE.sound (Shell.Frame.look [v ^ (s * k), (v ^ 2) ^ (k * j), lam, (v ^ 8) ^ s,286      (v ^ 2) ^ ((8 - k % 8) * j)])287      (.mul (.add (.mul (.var 0) (.var 1)) (.mul (.var 2) (.mul (.mul (.var 0) (.var 3)) (.var 1)))) (.var 4))288      (.mul (.mul (.var 0) (.add .one (.mul (.var 2) (.var 3)))) (.mul (.var 1) (.var 4)))289      (by decide +kernel)290  rw [sum_congr 8 (fun j _ => e1 j), sum_mul_left, selection hq hω k (Nat.mod_lt k (by decide)), if_pos rfl,291    mul_comm]292293/-! ## 22:C17, X7, P3 — the Tsirelson square and no-signalling -/294295/-- 22:C17, 22:X7, 22:C25, 22:P3 — the Tsirelson square: `S = 2(ζ + ζ⁷)` for `ζ⁴ = −1` has `S² = 8` on every shell, the shadow of the296ring identity `S² = 8` in `ℤ[ζ₈]`. -/297theorem singlet_square {ζ : Shell q} (h4 : ζ ^ 4 = -1) : (2 * (ζ + ζ ^ 7)) * (2 * (ζ + ζ ^ 7)) = 8 := by298  rw [mul_mul_mul_comm, tsirelson h4]299  show ofNat 2 * ofNat 2 * ofNat 2 = ofNat 8300  rw [ofNat_mul, ofNat_mul]301302/-- 22:C17 — no-signalling: the marginal of one wing, `c(1 + E) + c(1 − E)` over the two outcomes of the other303(`c = 1/4`), is `2c`, independent of the correlator and so of the far setting. -/304theorem no_signalling (c E : Shell q) : c * (1 + E) + c * (1 + -E) = c * 2 := by305  rw [two_eq]306  exact Shell.Frame.RE.sound (Shell.Frame.look [c, E])307    (.add (.mul (.var 0) (.add .one (.var 1))) (.mul (.var 0) (.add .one (.neg (.var 1)))))308    (.mul (.var 0) (.add .one .one)) (by decide +kernel)309310/-! ## 22:C19, P1 — the channel complementarity -/311312/-- 22:C19, 22:P1 — **`V² + C² = 1`** on every shell: for a unit phase `x` with inverse `y`, the visibility313`V = (x + y)/2` and the concurrence `C = (x − y)/(2i)` (`h = 1/2`, `i² = −1`, `1/i = −i`) satisfy `V² + C² = 1`314exactly, the which-path complementarity of the pure gravitational channel. -/315theorem channel_complementarity {h x y i : Shell q} (hh : h * 2 = 1) (hxy : x * y = 1) (hi : i * i = -1) :316    (h * (x + y)) * (h * (x + y)) + (h * (x + -y) * -i) * (h * (x + -y) * -i) = 1 := by317  have e : (h * (x + y)) * (h * (x + y)) + (h * (x + -y) * -i) * (h * (x + -y) * -i) =318      (h * 2) * (h * 2) * (x * y) + h * h * ((x + -y) * (x + -y)) * (i * i + 1) := by319    rw [two_eq]320    exact Shell.Frame.RE.sound (Shell.Frame.look [h, x, y, i]) (.add (.mul (.mul (.var 0) (.add (.var 1) (.var 2))) (.mul (.var 0) (.add (.var 1) (.var 2)))) (.mul (.mul (.mul (.var 0) (.add (.var 1) (.neg (.var 2)))) (.neg (.var 3))) (.mul (.mul (.var 0) (.add (.var 1) (.neg (.var 2)))) (.neg (.var 3))))) (.add (.mul (.mul (.mul (.var 0) (.add .one .one)) (.mul (.var 0) (.add .one .one))) (.mul (.var 1) (.var 2))) (.mul (.mul (.mul (.var 0) (.var 0)) (.mul (.add (.var 1) (.neg (.var 2))) (.add (.var 1) (.neg (.var 2))))) (.add (.mul (.var 3) (.var 3)) .one))) (by decide +kernel)321  rw [e, hh, hxy, hi, neg_add, mul_zero, mul_one, mul_one, add_zero]322323/-- 22:C19 — at zero coupling the branch state is a product: the concurrence vanishes, `C = h (x − x)(−i) = 0`. -/324theorem channel_product_at_zero (h x i : Shell q) : h * (x + -x) * -i = 0 := by325  rw [add_neg, mul_zero, zero_mul]326327/-! ## 22:C20 — no collapse, exact revival -/328329/-- 22:C20 — the drive conserves the ledger norm: a unit phase `u` (`u ū = 1`) leaves `a ā` unchanged, so an isolated330superposition keeps unit fringe contrast at every drive time. -/331theorem drive_norm {u ub : Shell q} (hu : u * ub = 1) (a ab : Shell q) : (u * a) * (ub * ab) = a * ab := by332  rw [mul_mul_mul_comm, hu, one_mul]333334/-- 22:C20 — the exact revival: the visibility `V(t) = Σ_E p_E ζ^{E t}` returns to `Σ_E p_E` at the recurrence `n`335(`ζ^n = 1`): dephasing, never collapse. -/336theorem revival {ζ : Shell q} {n : Nat} (hn : ζ ^ n = 1) (p : Nat → Shell q) (M : Nat) :337    sumRange (fun E => p E * ζ ^ (E * n)) M = sumRange p M :=338  sum_congr M (fun E _ => by rw [Nat.mul_comm, pow_mul, hn, one_pow, mul_one])339340/-! ## 22:C21 — the coherent-fraction channel -/341342/-- A constant product is a power. -/343theorem prodRange_const (x : Shell q) : ∀ m, prodRange (fun _ => x) m = x ^ m344  | 0 => rfl345  | m + 1 => by show prodRange (fun _ => x) m * x = x ^ (m + 1); rw [prodRange_const x m, pow_succ]346347/-- 22:C21 (ii), 22:P1 — the branch phase of `m_c` synchronised cells is the coherent product `ζ^{m_c a}`. -/348theorem branch_phase (ζ : Shell q) (a mc : Nat) : prodRange (fun _ => ζ ^ a) mc = ζ ^ (mc * a) := by349  rw [prodRange_const, ← pow_mul, Nat.mul_comm]350351/-- 22:C21 (ii) — the pairwise law: the phase of `m₁` against `m₂` synchronised cells is `ζ^{m₁ m₂ a}`. -/352theorem pair_product (ζ : Shell q) (a m1 m2 : Nat) : (ζ ^ (m1 * a)) ^ m2 = ζ ^ (m1 * m2 * a) := by353  rw [← pow_mul, FRC.Nat.mul_assoc, Nat.mul_comm a m2, ← FRC.Nat.mul_assoc]354355/-- 22:C21 (iii) — a complete sector sum vanishes: the offset-spread cells' phases cancel over one cycle. -/356theorem spread_cancels (hq : FRC.Nat.isPrime q) {ζ : Shell q} {n : Nat} (hζ : HasOrder ζ n) (hζ1 : ζ ≠ 1) :357    sumRange (fun θ => ζ ^ θ) n = 0 := geom_sum_zero hq n hζ.2.1 hζ1358359/-- 22:C21 (iii), 22:P1 — the reduced channel factorises: the offset distribution's partial sum times the coherent phase,360`Σ_θ p_θ ζ^{θ + c} = (Σ_θ p_θ ζ^θ) ζ^c = χ_inc · ζ^{f φ}`. -/361theorem channel_assembly (ζ : Shell q) (p : Nat → Shell q) (n c : Nat) :362    sumRange (fun θ => p θ * ζ ^ (θ + c)) n = sumRange (fun θ => p θ * ζ ^ θ) n * ζ ^ c := by363  rw [← sum_mul_right]364  exact sum_congr n (fun θ _ => by rw [pow_add, mul_assoc])365366/-! ## 22:C23, X4 — inter-Subject consistency -/367368/-- 22:C23 (ii), 22:X4 — shared-core agreement: with the common core of order `e` dividing both cores `a`, `b`, the channels369`r ≡ k (mod a)` of `S` and `r' ≡ k (mod b)` of `S'` agree on the common core, `r ≡ r' (mod e)`: both induce the one370character `η_{k mod e}`. -/371theorem order_independence {a b e r r' k : Nat} (he : 0 < e) (ha : 0 < a) (hb : 0 < b) (hae : a % e = 0)372    (hbe : b % e = 0) (hr : r % a = k % a) (hr' : r' % b = k % b) : r % e = r' % e := by373  rw [← mod_mod_of_dvd (n := r) he ha hae, hr, mod_mod_of_dvd he ha hae, ← mod_mod_of_dvd (n := r') he hb hbe, hr',374    mod_mod_of_dvd he hb hbe]375376/-- 22:C23 (i), 22:X4 — joint refinement: the common cosets of two cores (classes modulo `α` and modulo `β` on the Object377cycle) are the classes modulo one period `T`, the common core's, in either order; `T` lies below the product378`αβ` (`FRC.Quantum.joint_recurrence` on the two parts, the search bounded by `αβ`). -/379theorem joint_refinement (α β : Nat) (hα : 0 < α) (hβ : 0 < β) :380    ∃ T, T ≤ α * β ∧ 0 < T ∧ ∀ x, (x % α = 0 ∧ x % β = 0) ↔ x % T = 0 := by381  let n : Nat → Nat := fun j => if j = 0 then α else β382  have hn : ∀ j, 0 < n j := fun j => by383    show 0 < (if j = 0 then α else β)384    match Nat.decEq j 0 with385    | .isTrue e => rw [if_pos e]; exact hα386    | .isFalse e => rw [if_neg e]; exact hβ387  have hL : Joint n 2 (α * β) := fun j hj => by388    show (α * β) % (if j = 0 then α else β) = 0389    match j with390    | 0 => rw [if_pos rfl]; exact mod_zero_of_eq_mul hα rfl391    | 1 => rw [if_neg (by decide), Nat.mul_comm]; exact mod_zero_of_eq_mul hβ rfl392    | j + 2 => exact absurd hj (Nat.not_lt_of_le (Nat.le_add_left 2 j))393  obtain ⟨T, hTL, hT0, _, hiff, _⟩ := joint_recurrence n hn 2 (α * β) (Nat.mul_pos hα hβ) hL394  refine ⟨T, hTL, hT0, fun x => Iff.trans ?_ (hiff x)⟩395  constructor396  · intro ⟨h0, h1⟩ j hj397    show x % (if j = 0 then α else β) = 0398    match j with399    | 0 => rw [if_pos rfl]; exact h0400    | 1 => rw [if_neg (by decide)]; exact h1401    | j + 2 => exact absurd hj (Nat.not_lt_of_le (Nat.le_add_left 2 j))402  · intro h403    constructor404    · have := h 0 (by decide)405      exact (show x % (if 0 = 0 then α else β) = 0 from this) |> fun e => by rwa [if_pos rfl] at e406    · have := h 1 (by decide)407      exact (show x % (if 1 = 0 then α else β) = 0 from this) |> fun e => by rwa [if_neg (by decide)] at e408409/-! ## The worked carriers (Table `tab:configs`), decided by the kernel -/410411instance decHasOrder {p : Nat} [Pos p] (x : Shell p) (n : Nat) : Decidable (HasOrder x n) :=412  have : Decidable (∀ l, l < n → 0 < l → x ^ l ≠ 1) := FRC.Shell.decForallLT (fun l => 0 < l → x ^ l ≠ 1) n413  inferInstanceAs (Decidable (0 < n ∧ x ^ n = 1 ∧ ∀ l, l < n → 0 < l → x ^ l ≠ 1))414415/-- 22:C24, the worked carrier `𝔽₁₅₇` (`κ = 39`): `g = 5` is primitive, the quarter-turn `I = g^{−39} = g^{117} = 28`,416`I² = −1`; the Subject `S₅₃` has the cycle `C₅₂ = ⟨g³ = 125⟩`, the Object `O₁₃` the cycle `C₁₂ = ⟨g¹³ = 22⟩`, the core417`Q₄` (`gcd(52, 12) = 4`), three outcomes (`12/4 = 3`). -/418theorem carrier_157 :419    (157 : Nat) = 4 * 39 + 1 ∧ HasOrder (5 : Shell 157) 156 ∧ (5 : Shell 157) ^ 117 = 28 ∧420    (28 : Shell 157) * 28 = -1 ∧ (5 : Shell 157) ^ 3 = 125 ∧ HasOrder (125 : Shell 157) 52 ∧421    (5 : Shell 157) ^ 13 = 22 ∧ HasOrder (22 : Shell 157) 12 ∧422    (52 % 4 = 0 ∧ 12 % 4 = 0 ∧ ∀ e, e < 53 → 52 % e = 0 → 12 % e = 0 → 4 % e = 0) ∧ 12 = 4 * 3 := by423  decide +kernel424425/-- 22:C24, 22:X5 — the worked carrier `𝔽₄₂₁` (`κ = 105`): `g = 2` is primitive, `I = g^{−105} = g^{315} = 392`, `I² = −1`;426the Subject `S₆₁` (`C₆₀`) resolves `O₂₉` (`C₂₈`) through the core `Q₄` (`gcd(60, 28) = 4`) in seven outcomes427(`28 = 4 · 7`) and absorbs `O₁₃` (`C₁₂`, `gcd(60, 12) = 12`, one outcome): quantumness is the subgroup index. -/428theorem carrier_421 :429    (421 : Nat) = 4 * 105 + 1 ∧ HasOrder (2 : Shell 421) 420 ∧ (2 : Shell 421) ^ 315 = 392 ∧430    (392 : Shell 421) * 392 = -1 ∧431    (60 % 4 = 0 ∧ 28 % 4 = 0 ∧ ∀ e, e < 61 → 60 % e = 0 → 28 % e = 0 → 4 % e = 0) ∧ 28 = 4 * 7 ∧432    (60 % 12 = 0 ∧ 12 % 12 = 0 ∧ ∀ e, e < 61 → 60 % e = 0 → 12 % e = 0 → 12 % e = 0) ∧ 12 = 12 * 1 := by433  decide +kernel434435/-- 22:C16, 22:C17 — the worked carrier `𝔽₆₄₁` (`κ = 160`): `g = 3` is primitive; the Object generator `g_O = g⁴⁰ = 601`436has order `16` and `g_O⁸ = −1` (the doublet's sign); the setting step `ζ₈₀ = g⁸ = 151` has order `80`; the octant437`ζ₈ = g⁸⁰ = 318` has `ζ₈⁴ = −1`, `(ζ₈ + ζ₈⁷)² = 2` and `S² = 8`; the Bell core is `C₈` (`gcd(40, 16) = 8`). -/438theorem carrier_641 :439    (641 : Nat) = 4 * 160 + 1 ∧ HasOrder (3 : Shell 641) 640 ∧ (3 : Shell 641) ^ 40 = 601 ∧440    HasOrder (601 : Shell 641) 16 ∧ (601 : Shell 641) ^ 8 = -1 ∧ (3 : Shell 641) ^ 8 = 151 ∧441    HasOrder (151 : Shell 641) 80 ∧ (3 : Shell 641) ^ 80 = 318 ∧ (318 : Shell 641) ^ 4 = -1 ∧442    (318 + (318 : Shell 641) ^ 7) * (318 + (318 : Shell 641) ^ 7) = 2 ∧443    (2 * (318 + (318 : Shell 641) ^ 7)) * (2 * (318 + (318 : Shell 641) ^ 7)) = 8 ∧444    (40 % 8 = 0 ∧ 16 % 8 = 0 ∧ ∀ e, e < 41 → 40 % e = 0 → 16 % e = 0 → 8 % e = 0) := by445  decide +kernel446447end FRC.Composite448