Theme/Interference.lean — FrcCore

1import FrcCore.Theme.Field2import FrcCore.Ring34/-!5# FrcCore.Theme.Interference — the quantum theme: the interference hierarchy and the splitting depth (22-quantum, 15 October 2026)67Two laws of the ledger read on every shell, where the ledger's conjugation is any additive map `c` (the shadow of8`ζ ↦ ζ⁻¹` on the windings, extended additively) and the weight is `w(x) = x · c(x)`:910* the Sorkin hierarchy: the `k`-fold mixed difference of the weight vanishes for every `k ≥ 3` and every base point,11  while the second difference is the cross term `a c(b) + b c(a)`, nonzero at `a = b = 1` with `c` the identity12  (`sorkin_hierarchy`, `sorkin_second`, `sorkin_second_witness`, 22:C8, X8, P2): the interference term `I_k`13  (inclusion–exclusion of the pair count over the paths, the mixed difference at the origin) is zero exactly for14  `k ≥ 3` and generically nonzero for `k = 2`;15* the Hadamard layers: on a shell with a quarter-turn `i² = −1`, `(1 + i)² = 2i`, so `k` balanced layers give the16  amplitude `(1 + i)^k = 2^m i^m` (`k = 2m`) or `2^m i^m (1 + i)` (`k = 2m + 1`) (`hadamard_even`, `hadamard_odd`,17  22:C14); the minimal tally norm `T(k) = 2^{k + [k odd]}` is monotone and the ceiling `k* = max{k : d T(k) < Ω}` is18  decided on the worked carrier `Ω = 641`: `8` for the unit core, `6` for the Bell core `d = 8` (`tally_norm_mono`,19  `ceiling_641`, 22:C14, P5).2021No axioms.22-/2324namespace FRC.Interference2526open FRC.Shell27open FRC.Shell.Prime2829variable {q : Nat} [Pos q]3031/-! ## The Sorkin hierarchy -/3233/-- A conjugation on the shell: an additive map (the shadow of the ledger's conjugation). -/34def Additive (c : Shell q → Shell q) : Prop := ∀ x y, c (x + y) = c x + c y3536/-- The weight `w(x) = x · c(x)`, the shadow of the squared amplitude `x x̄`. -/37def weight (c : Shell q → Shell q) (x : Shell q) : Shell q := x * c x3839/-- The `k`-fold mixed difference of `f` along the directions `a 0, …, a (k−1)`:40`Δ_{a_{k−1}} ⋯ Δ_{a_0} f (x)`, with `Δ_a f (x) = f (x + a) − f (x)`. The Sorkin term `I_k` of the paths `a_0, …, a_{k−1}`41is the difference at the origin. -/42def mixedDiff (a : Nat → Shell q) (f : Shell q → Shell q) : Nat → Shell q → Shell q43  | 0, x => f x44  | k + 1, x => mixedDiff a f k (x + a k) + -(mixedDiff a f k x)4546theorem mixedDiff_zero (a : Nat → Shell q) (f : Shell q → Shell q) (x : Shell q) : mixedDiff a f 0 x = f x := rfl4748theorem mixedDiff_succ (a : Nat → Shell q) (f : Shell q → Shell q) (k : Nat) (x : Shell q) :49    mixedDiff a f (k + 1) x = mixedDiff a f k (x + a k) + -(mixedDiff a f k x) := rfl5051/-- The first difference of the weight: `Δ_a w (x) = x c(a) + a c(x) + a c(a)`. -/52theorem weight_diff1 {c : Shell q → Shell q} (hc : Additive c) (a : Nat → Shell q) (x : Shell q) :53    mixedDiff a (weight c) 1 x = x * c (a 0) + a 0 * c x + a 0 * c (a 0) := by54  rw [mixedDiff_succ, mixedDiff_zero, mixedDiff_zero]55  unfold weight56  rw [hc]57  exact Shell.Frame.RE.sound (Shell.Frame.look [x, a 0, c x, c (a 0)])58    (.add (.mul (.add (.var 0) (.var 1)) (.add (.var 2) (.var 3))) (.neg (.mul (.var 0) (.var 2))))59    (.add (.add (.mul (.var 0) (.var 3)) (.mul (.var 1) (.var 2))) (.mul (.var 1) (.var 3)))60    (by decide +kernel)6162/-- 22:C8 — the second difference is the cross term: `Δ_b Δ_a w (x) = b c(a) + a c(b)`, independent of `x`. -/63theorem sorkin_second {c : Shell q → Shell q} (hc : Additive c) (a : Nat → Shell q) (x : Shell q) :64    mixedDiff a (weight c) 2 x = a 1 * c (a 0) + a 0 * c (a 1) := by65  rw [mixedDiff_succ, weight_diff1 hc, weight_diff1 hc, hc]66  exact Shell.Frame.RE.sound (Shell.Frame.look [x, a 0, a 1, c x, c (a 0), c (a 1)])67    (.add (.add (.add (.mul (.add (.var 0) (.var 2)) (.var 4)) (.mul (.var 1) (.add (.var 3) (.var 5)))) (.mul (.var 1) (.var 4)))68      (.neg (.add (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 3))) (.mul (.var 1) (.var 4)))))69    (.add (.mul (.var 2) (.var 4)) (.mul (.var 1) (.var 5)))70    (by decide +kernel)7172/-- The third difference vanishes identically. -/73theorem sorkin_third {c : Shell q → Shell q} (hc : Additive c) (a : Nat → Shell q) (x : Shell q) :74    mixedDiff a (weight c) 3 x = 0 := by75  rw [mixedDiff_succ, sorkin_second hc, sorkin_second hc, add_neg]7677/-- 22:C8, 22:X8, 22:P2 — **the Sorkin hierarchy**: for every additive conjugation `c`, every family of paths `a` and every78base point `x`, the `k`-fold mixed difference of the weight `w(x) = x c(x)` is zero for every `k ≥ 3`; so the79interference terms `I_k = Δ_{a_{k−1}} ⋯ Δ_{a_0} w (0)` vanish exactly from the third order on, on every channel and80outcome (the ledger's value reduces to the shadow, and a vanishing shadow lifts to a multiple of `Ω`). -/81theorem sorkin_hierarchy {c : Shell q → Shell q} (hc : Additive c) (a : Nat → Shell q) :82    ∀ k, ∀ x, mixedDiff a (weight c) (k + 3) x = 083  | 0, x => sorkin_third hc a x84  | k + 1, x => by85    rw [mixedDiff_succ, sorkin_hierarchy hc a k, sorkin_hierarchy hc a k, add_neg]8687/-- The identity is additive. -/88theorem additive_id : Additive (fun x : Shell q => x) := fun _ _ => rfl8990/-- 22:C8 — `I₂` is generically nonzero: with `c` the identity and the paths `a = b = 1`, `I₂ = 2 ≠ 0` on every91shell `q > 2`. -/92theorem sorkin_second_witness (h2 : 2 < q) :93    mixedDiff (fun _ => (1 : Shell q)) (weight fun x => x) 2 0 ≠ 0 := by94  rw [sorkin_second additive_id]95  show (1 : Shell q) * 1 + 1 * 1 ≠ 096  rw [mul_one, ← two_eq]97  exact ofNat_ne_zero (by decide) h29899/-! ## The Hadamard layers and the splitting depth -/100101/-- `ofNat` of a power is the power of `ofNat`. -/102theorem ofNat_pow (a : Nat) : ∀ m, (ofNat (a ^ m) : Shell q) = ofNat a ^ m103  | 0 => rfl104  | m + 1 => by rw [Nat.pow_succ, ← ofNat_mul, ofNat_pow a m, pow_succ]105106/-- One balanced layer squared: `(1 + i)² = 2i` for a quarter-turn `i² = −1`. -/107theorem hadamard_sq {i : Shell q} (hi : i * i = -1) : (1 + i) * (1 + i) = 2 * i := by108  have e : (1 + i) * (1 + i) = 1 + (i + i) + i * i :=109    Shell.Frame.RE.sound (Shell.Frame.look [i])110      (.mul (.add .one (.var 0)) (.add .one (.var 0)))111      (.add (.add .one (.add (.var 0) (.var 0))) (.mul (.var 0) (.var 0)))112      (by decide +kernel)113  rw [e, hi, add_assoc, add_comm (i + i), ← add_assoc, add_neg, zero_add, two_eq, right_distrib, one_mul]114115/-- 22:C14, 22:P5 — `2m` balanced layers give the amplitude `(1 + i)^{2m} = 2^m i^m`. -/116theorem hadamard_even {i : Shell q} (hi : i * i = -1) (m : Nat) : (1 + i) ^ (2 * m) = ofNat (2 ^ m) * i ^ m := by117  rw [pow_mul, pow_two, hadamard_sq hi, mul_pow, ofNat_pow]; rfl118119/-- 22:C14 — `2m + 1` balanced layers give the amplitude `(1 + i)^{2m+1} = 2^m i^m (1 + i)`. -/120theorem hadamard_odd {i : Shell q} (hi : i * i = -1) (m : Nat) :121    (1 + i) ^ (2 * m + 1) = ofNat (2 ^ m) * i ^ m * (1 + i) := by122  rw [pow_succ, hadamard_even hi]123124/-- The minimal tally norm after `k` balanced layers: `T(k) = 2^{k + [k odd]}`, that is `2^k` for even `k` and125`2^{k+1}` for odd `k`. -/126def tallyNorm (k : Nat) : Nat := 2 ^ (k + k % 2)127128/-- 22:C14, 22:P5 — the tally norm is monotone in the depth. -/129theorem tally_norm_mono {k k' : Nat} (h : k ≤ k') : tallyNorm k ≤ tallyNorm k' := by130  unfold tallyNorm131  refine Nat.pow_le_pow_right (by decide) ?_132  match Nat.eq_or_lt_of_le h with133  | .inl e => rw [e]; exact Nat.le_refl _134  | .inr hlt =>135    have h1 : k % 2 ≤ 1 := Nat.le_of_lt_succ (Nat.mod_lt k (by decide))136    calc k + k % 2 ≤ k + 1 := Nat.add_le_add_left h1 k137      _ ≤ k' := hlt138      _ ≤ k' + k' % 2 := Nat.le_add_right k' _139140/-- 22:C14, 22:P5 — **the ceiling on the worked carrier** `Ω = 641`: the largest depth with `T(k) < Ω` is `k* = 8` for the141unit core (`T(8) = 256`, `T(9) = 1024`), and with the Bell core `d = 8` it is `6` (`8 T(6) = 512`, `8 T(7) = 2048`). -/142theorem ceiling_641 : (∀ k, tallyNorm k < 641 ↔ k ≤ 8) ∧ (∀ k, 8 * tallyNorm k < 641 ↔ k ≤ 6) := by143  have t8 : tallyNorm 8 = 256 := by decide144  have t9 : tallyNorm 9 = 1024 := by decide145  have t6 : tallyNorm 6 = 64 := by decide146  have t7 : tallyNorm 7 = 256 := by decide147  constructor148  · intro k149    constructor150    · intro h151      match Nat.lt_or_ge 8 k with152      | .inl hlt =>153        have := tally_norm_mono (Nat.succ_le_of_lt hlt)154        rw [t9] at this155        exact absurd (Nat.lt_of_le_of_lt this h) (by decide)156      | .inr hge => exact hge157    · intro h158      have := tally_norm_mono h159      rw [t8] at this160      exact Nat.lt_of_le_of_lt this (by decide)161  · intro k162    constructor163    · intro h164      match Nat.lt_or_ge 6 k with165      | .inl hlt =>166        have := Nat.mul_le_mul_left 8 (tally_norm_mono (Nat.succ_le_of_lt hlt))167        rw [t7] at this168        exact absurd (Nat.lt_of_le_of_lt this h) (by decide)169      | .inr hge => exact hge170    · intro h171      have := Nat.mul_le_mul_left 8 (tally_norm_mono h)172      rw [t6] at this173      exact Nat.lt_of_le_of_lt this (by decide)174175end FRC.Interference176