Theme/Tally.lean — FrcCore

1/-!2# FrcCore.Theme.Tally — the pair tally on the `Q₄` core (the extension theme; 00:C11, the push of 8 October 2026)34A file of its own, importing nothing, so that the certificates whose closures reach the extension theme (20-rh) stay5within the size budget of decision Q03. Its python side is `frc/extension.py` (`q4_kernel`, `q4_tally`, …).67The stationary core-valued `Q₄` sector: kernels `K : Q₄ → ℤ[i]` with `K(−d) = conj K(d)` (two-way), tally-valued on8the sector's states. The admissible kernels are the tally combinations `K = Σ_r c_r η_r` of the four characters9`η_r(d) = i^{rd}`; the pair tally `F(K, ψ) = Σ_{u,v} K(v − u) ψ_u conj ψ_v` on a pure winding `ψ_k(u) = i^{ku}` reads the10coefficient, `F(K_c, ψ_k) = 16 c_k`, so the tallies are fixed by the pure windings; Fourier inversion recovers every11coefficient; a single-channel response (channel-selectivity) is a scaled unit coefficient vector, the Born ray; the12core DFT has determinant `−16i`; and a linear functional leaves the tally cone on `i ψ₀`. The box `−1 ≤ c_r ≤ 3` of coefficients (negative ones included) is exhausted by the kernel for the fixing formula and13the tally criterion, the cube `0 ≤ c_r ≤ 3` for the two-way, inversion and selectivity clauses, as the paper's witness14exhausts it; the kernels, states and bilinear form the paper's Lemma degree and its witness U3, U5, U6a name are15instances decided by the kernel. Gaussian integers as pairs. -/1617namespace FRC.Extension.Tally1819/-- A Gaussian integer `re + im·i`. -/20structure GI where21  re : Int22  im : Int23deriving DecidableEq2425namespace GI26def add (x y : GI) : GI := ⟨x.re + y.re, x.im + y.im⟩27def mul (x y : GI) : GI := ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩28def conj (x : GI) : GI := ⟨x.re, -x.im⟩29def smul (c : Int) (x : GI) : GI := ⟨c * x.re, c * x.im⟩30instance : Add GI := ⟨add⟩31instance : Mul GI := ⟨mul⟩32def zero : GI := ⟨0, 0⟩33def i : GI := ⟨0, 1⟩34/-- `i^n`. -/35def ipow (n : Nat) : GI := match n % 4 with36  | 0 => ⟨1, 0⟩ | 1 => ⟨0, 1⟩ | 2 => ⟨-1, 0⟩ | _ => ⟨0, -1⟩37/-- A Gaussian integer is a tally when it is a nonnegative integer. -/38def tally (x : GI) : Prop := x.im = 0 ∧ 0 ≤ x.re39instance (x : GI) : Decidable (tally x) := inferInstanceAs (Decidable (_ ∧ _))40end GI4142open GI4344/-- The sum of a function over `Q₄`. -/45def sum4 (f : Nat → GI) : GI := f 0 + f 1 + f 2 + f 346/-- The character `η_r(d) = i^{rd}`. -/47def eta (r d : Nat) : GI := ipow (r * d)48/-- The kernel `K_c = Σ_r c_r η_r` with the coefficients `c = (c₀, c₁, c₂, c₃)`. -/49def kernel (c₀ c₁ c₂ c₃ : Int) (d : Nat) : GI :=50  smul c₀ (eta 0 d) + smul c₁ (eta 1 d) + smul c₂ (eta 2 d) + smul c₃ (eta 3 d)51/-- The pure winding `ψ_k(u) = i^{ku}` restricted to the fibre. -/52def psi (k u : Nat) : GI := ipow (k * u)53/-- The pair tally `F(K, ψ) = Σ_{u,v} K(v − u) ψ_u conj ψ_v`, the offset read modulo four. -/54def F (K : Nat → GI) (ψ : Nat → GI) : GI := sum4 fun u => sum4 fun v => K ((v + 4 - u) % 4) * ψ u * conj (ψ v)55/-- The coefficient `c_k` of the cube point `(c₀, c₁, c₂, c₃)` at the channel `k`. -/56def coeff (c₀ c₁ c₂ c₃ : Int) (k : Nat) : Int := match k % 4 with57  | 0 => c₀ | 1 => c₁ | 2 => c₂ | _ => c₃58/-- Fourier inversion: `Σ_d K(d) i^{−rd}`. -/59def inversion (K : Nat → GI) (r : Nat) : GI := sum4 fun d => K d * ipow ((4 - r % 4) * d)60/-- The number of channels `k < 4` on which the kernel responds. -/61def responses (K : Nat → GI) : Nat :=62  (if F K (psi 0) = zero then 0 else 1) + (if F K (psi 1) = zero then 0 else 1) +63  (if F K (psi 2) = zero then 0 else 1) + (if F K (psi 3) = zero then 0 else 1)64/-- The number of nonzero coefficients. -/65def support (c₀ c₁ c₂ c₃ : Int) : Nat :=66  (if c₀ = 0 then 0 else 1) + (if c₁ = 0 then 0 else 1) + (if c₂ = 0 then 0 else 1) + (if c₃ = 0 then 0 else 1)6768set_option maxRecDepth 4000 in69/-- 00:C11 (i), 22:C12 — the pure windings fix the tallies on the box `−1 ≤ c_r ≤ 3` (the naturals `a, b, c, d < 5`, cast to70`ℤ` and shifted by one), which contains negative coefficients: `F(K_c, ψ_k) = 16 c_k` for every kernel of the box and71every channel `k`. -/72theorem winding_fixing : ∀ a : Nat, a < 5 → ∀ b : Nat, b < 5 → ∀ c : Nat, c < 5 → ∀ d : Nat, d < 5 →73    ∀ k : Nat, k < 4 →74    F (kernel (Int.ofNat a - 1) (Int.ofNat b - 1) (Int.ofNat c - 1) (Int.ofNat d - 1)) (psi k) =75      ⟨16 * coeff (Int.ofNat a - 1) (Int.ofNat b - 1) (Int.ofNat c - 1) (Int.ofNat d - 1) k, 0⟩ := by decide +kernel7677set_option maxRecDepth 4000 in78/-- 00:C11 (i′), 22:C12, 22:X6 — the tally criterion on the box: the pair tally of `K_c` on `ψ_k` is a tally (a nonnegative integer)79iff `0 ≤ c_k` — the cone's two halves: every tally combination is tally-valued on the windings, and a kernel with a80negative coefficient is excluded by its own winding. -/81theorem tally_criterion : ∀ a : Nat, a < 5 → ∀ b : Nat, b < 5 → ∀ c : Nat, c < 5 → ∀ d : Nat, d < 5 →82    ∀ k : Nat, k < 4 →83    (tally (F (kernel (Int.ofNat a - 1) (Int.ofNat b - 1) (Int.ofNat c - 1) (Int.ofNat d - 1)) (psi k)) ↔84      (0 : Int) ≤ coeff (Int.ofNat a - 1) (Int.ofNat b - 1) (Int.ofNat c - 1) (Int.ofNat d - 1) k) := by decide +kernel8586/-- 00:C11 (ii), 22:C12 — every kernel of the cube is two-way, `K(−d) = conj K(d)`, and tally-valued on the pure windings. -/87theorem two_way : ∀ a : Nat, a < 4 → ∀ b : Nat, b < 4 → ∀ c : Nat, c < 4 → ∀ d : Nat, d < 4 →88    (∀ e, e < 4 → kernel (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d) ((4 - e) % 4) = conj (kernel (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d) e)) ∧89    (∀ k, k < 4 → tally (F (kernel (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d)) (psi k))) := by decide9091/-- 00:C11 (iii), 22:C3, 22:C12 — Fourier inversion recovers every coefficient exactly: `Σ_d K(d) i^{−rd} = 4 c_r`. -/92theorem fourier_inversion : ∀ a : Nat, a < 4 → ∀ b : Nat, b < 4 → ∀ c : Nat, c < 4 → ∀ d : Nat, d < 4 →93    ∀ r, r < 4 → inversion (kernel (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d)) r = ⟨4 * coeff (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d) r, 0⟩ := by decide9495/-- 00:C11 (iv), 22:C12, 22:X6 — channel-selectivity picks the ray: a kernel of the cube responds on exactly one channel iff its96coefficient vector is a scaled unit vector. -/97theorem channel_selectivity : ∀ a : Nat, a < 4 → ∀ b : Nat, b < 4 → ∀ c : Nat, c < 4 → ∀ d : Nat, d < 4 →98    (responses (kernel (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d)) = 1 ↔ support (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d) = 1) := by decide99100/-- 00:C11 (v), 22:C3, 22:C12 — the core DFT matrix `(i^{ru})` is invertible: its determinant is `−16i`. -/101theorem dft_det :102    let M := fun r u => ipow (r * u)103    let d2 := fun a b c d : GI => a * d + smul (-1) (b * c)104    let e := fun r => M r105    let det3 := fun (f g h : Nat → GI) => f 1 * d2 (g 2) (g 3) (h 2) (h 3) + smul (-1) (f 2 * d2 (g 1) (g 3) (h 1) (h 3)) + f 3 * d2 (g 1) (g 2) (h 1) (h 2)106    e 0 0 * det3 (e 1) (e 2) (e 3) + smul (-1) (e 1 0 * det3 (e 0) (e 2) (e 3)) +107      e 2 0 * det3 (e 0) (e 1) (e 3) + smul (-1) (e 3 0 * det3 (e 0) (e 1) (e 2)) = ⟨0, -16⟩ := by decide108109/-- The unconjugated bilinear form `B(K, ψ) = Σ_{u,v} K(v − u) ψ_u ψ_v` of the same kernel. -/110def B (K : Nat → GI) (ψ : Nat → GI) : GI := sum4 fun u => sum4 fun v => K ((v + 4 - u) % 4) * ψ u * ψ v111/-- The fibre norm `K = [d = 0]`. -/112def fibreNorm (d : Nat) : GI := if d % 4 = 0 then ⟨1, 0⟩ else ⟨0, 0⟩113/-- A two-way kernel outside the box, `5η₁ − 2η₂ + η₃ = (4, 2 + 4i, −8, 2 − 4i)`. -/114def kout (d : Nat) : GI := match d % 4 with115  | 0 => ⟨4, 0⟩ | 1 => ⟨2, 4⟩ | 2 => ⟨-8, 0⟩ | _ => ⟨2, -4⟩116/-- The Gaussian-lattice state `(1 + i) e₀`. -/117def psiA (u : Nat) : GI := if u = 0 then ⟨1, 1⟩ else ⟨0, 0⟩118/-- The Gaussian-lattice state `e₀ + i e₁`. -/119def psiB (u : Nat) : GI := if u = 0 then ⟨1, 0⟩ else if u = 1 then ⟨0, 1⟩ else ⟨0, 0⟩120121/-- 00:C11 (vi), 22:C12 — the witnesses of the cone's boundary (22-quantum's U3, U5, U6a): the negative coefficient122`c = (1, −1, 1, 0)` is excluded by its own winding, `F(K_c, ψ₁) = −16`; the two-way kernel `5η₁ − 2η₂ + η₃` outside the123box is excluded on `ψ₂` and Fourier inversion recovers `4c = (0, 20, −8, 4)`; the fibre norm `[d = 0]` is two-way,124responds `(4, 4, 4, 4)` with `4c_r = 1` on every channel (no tally combination) and fails channel-selectivity; the125single character `η₁` responds `16` on its channel and `0` elsewhere, so `η₁/16` reads `1` (c = 1/16, no tally). -/126theorem cone_boundary :127    F (kernel 1 (-1) 1 0) (psi 1) = ⟨-16, 0⟩ ∧ ¬ tally (F (kernel 1 (-1) 1 0) (psi 1)) ∧128    (∀ e, e < 4 → kout ((4 - e) % 4) = conj (kout e)) ∧ F kout (psi 2) = ⟨-32, 0⟩ ∧ ¬ tally (F kout (psi 2)) ∧129    inversion kout 0 = ⟨0, 0⟩ ∧ inversion kout 1 = ⟨20, 0⟩ ∧ inversion kout 2 = ⟨-8, 0⟩ ∧ inversion kout 3 = ⟨4, 0⟩ ∧130    (∀ d, d < 4 → smul 4 (kout d) = sum4 (fun r => inversion kout r * ipow (r * d))) ∧131    (∀ e, e < 4 → fibreNorm ((4 - e) % 4) = conj (fibreNorm e)) ∧ (∀ k, k < 4 → F fibreNorm (psi k) = ⟨4, 0⟩) ∧132    responses fibreNorm = 4 ∧ (∀ r, r < 4 → inversion fibreNorm r = ⟨1, 0⟩) ∧133    F (kernel 0 1 0 0) (psi 1) = ⟨16, 0⟩ ∧ F (kernel 0 1 0 0) (psi 0) = ⟨0, 0⟩ ∧ responses (kernel 0 1 0 0) = 1 := by decide134135/-- 00:C11 (vii), 22:C12 — the minimal degree is forced (22-quantum Lemma degree): a linear functional constant on the orbit136vanishes on every nontrivial winding (the complete character sums), and on the trivial winding `F(i ψ₀) = i F(ψ₀)`137leaves the tally cone for every nonzero multiplier `c ≤ 4`; and the unconjugated bilinear form leaves the tally line138on Gaussian-lattice states where the conjugated form of the same kernel stays on it: `B(fn, (1 + i)e₀) = 2i` against139`F = 2`, `B([d = 1], e₀ + i e₁) = i`, and `B(K_(1,1,0,0), (1 + i)e₀) = 4i` against `F = 4`. -/140theorem linear_exclusion :141    (∀ k, k < 4 → 0 < k → sum4 (fun u => ipow (k * u)) = zero) ∧142    (∀ c, c < 5 → 0 < c → ¬ tally (i * ⟨4 * Int.ofNat c, 0⟩)) ∧143    B fibreNorm psiA = ⟨0, 2⟩ ∧ ¬ tally (B fibreNorm psiA) ∧ F fibreNorm psiA = ⟨2, 0⟩ ∧ tally (F fibreNorm psiA) ∧144    B (fun d => if d % 4 = 1 then ⟨1, 0⟩ else ⟨0, 0⟩) psiB = ⟨0, 1⟩ ∧145    ¬ tally (B (fun d => if d % 4 = 1 then ⟨1, 0⟩ else ⟨0, 0⟩) psiB) ∧146    B (kernel 1 1 0 0) psiA = ⟨0, 4⟩ ∧ ¬ tally (B (kernel 1 1 0 0) psiA) ∧ F (kernel 1 1 0 0) psiA = ⟨4, 0⟩ := by decide147148end FRC.Extension.Tally149