/-
  CartanConnection.lean — Algebraic MC integrability for the Sidon crossing matrix

  Defines the 2-cochain μ ∈ C²(V,V) from the Sidon crossing matrix (I₂, I₄)
  and proves d_CE μ = 0 (the Jacobiator vanishes) by finite computation.

  For 2-cochains the Nijenhuis–Richardson self-bracket satisfies
  [μ,μ]_{NR}(X,Y,Z) = 2·J_μ(X,Y,Z).  d_CE μ + ½[μ,μ]_{NR} = 0 → d_CE μ = 0.

  Fusion-of-fusions context (see BREAKGLASS_NR_BRACKET_PROPOSAL.md):
    Layer 2b (analytic):  Sidon-orthogonality bypass (row-sum norm bound)
    Layer 2c (algebraic): Jacobiator vanishing — THIS MODULE
    Layer 2d (YB):        [μ,μ]_{NR}=0 ⇔ Yang-Baxter integrability
    Layer 2e (TL):        Factorization through Fibonacci TL quotient
    PIST:                 Same Sidon support separation drives gates
    VCN:                  Vanishing terms = structural zero gaps

  Proof strategy (integer bypass, replaces native_decide per AGENTS.md §5):
    D = lcm(7, 256) = 1792.  C_weight i j = C_int i j / D (exact).
    mu on ℤ-valued inputs scales by 1/D; Jacobiator scales by 1/D².
    decide on ℤ (binary arithmetic, no GCD) verifies 7³×8 = 2744 cases.
    Scaling then lifts the ℤ result to the ℚ theorem.
-/

import Mathlib.Data.Matrix.Basic
import Mathlib.Tactic

open scoped BigOperators

namespace SilverSight.PIST.CartanConnection

/-- The standard basis vectors of ℚ⁸ indexed by Fin 8. -/
def basisVec (i : Fin 8) : Fin 8 → ℚ := λ j => if i = j then 1 else 0

/-- The crossing weight C[i,j], from Layer 1 invariants I₂ + I₄:
    σ = 39/256 (diagonal), τ = 1/7 (same-block off-diagonal), 0 (cross-block). -/
def C_weight (i j : Fin 8) : ℚ :=
  if i = j then (39/256 : ℚ)
  else if i.val / 2 = j.val / 2 then (1/7 : ℚ)
  else 0

/-- The 2-cochain μ ∈ C²(ℚ⁸, ℚ⁸) associated to the Sidon crossing matrix.
    On basis vectors: μ(e_i, e_j) = C[i,j]·(e_i − e_j).
    This is alternating: μ(e_j,e_i) = −μ(e_i,e_j).

    Explicit formula:
      μ(X,Y)[k] = (C·X)[k]·Y[k] − X[k]·(C·Y)[k] -/
def mu (X Y : Fin 8 → ℚ) : Fin 8 → ℚ :=
  λ k => (∑ i : Fin 8, X i * C_weight i k) * Y k - X k * (∑ j : Fin 8, Y j * C_weight k j)

/-- The Chevalley–Eilenberg differential (Jacobiator) of a 2-cochain,
    in the abelian case where the bracket on V is trivial:
      (d_CE μ)(X,Y,Z) = μ(μ(X,Y), Z) + μ(μ(Y,Z), X) + μ(μ(Z,X), Y). -/
def Jacobiator (μ : (Fin 8 → ℚ) → (Fin 8 → ℚ) → (Fin 8 → ℚ))
    (X Y Z : Fin 8 → ℚ) : Fin 8 → ℚ :=
  μ (μ X Y) Z + μ (μ Y Z) X + μ (μ Z X) Y

/-- The 7 basis vectors v_k = e_k − e_7 of V = ker(Σ) = {w ∈ ℚ⁸ | Σ w_i = 0}.
    k ranges over Fin 7, embedded into indices 0–6 of Fin 8. -/
def v (k : Fin 7) : Fin 8 → ℚ :=
  λ i => if i = (k.castSucc : Fin 8) then 1
    else if i = 7 then -1
    else 0

-- ─── Integer bypass ──────────────────────────────────────────────────────────
-- D = lcm(7, 256) = 1792.  Exact: C_weight i j = C_int i j / 1792.
-- ─────────────────────────────────────────────────────────────────────────────

private def C_int (i j : Fin 8) : ℤ :=
  if i = j then 273                       -- 1792 × (39/256) = 7 × 39
  else if i.val / 2 = j.val / 2 then 256  -- 1792 × (1/7)
  else 0

/-- Block-diagonal structure: C_int vanishes across distinct 2-blocks.
    Useful for structural reasoning about the Sidon support separation. -/
private lemma C_int_cross_block_zero (i j : Fin 8)
    (h : i.val / 2 ≠ j.val / 2) : C_int i j = 0 := by
  simp only [C_int]
  split_ifs <;> simp_all

private lemma C_weight_scale (i j : Fin 8) : C_weight i j = (C_int i j : ℚ) / 1792 := by
  simp only [C_weight, C_int]; split_ifs <;> norm_num

private def mu_int (X Y : Fin 8 → ℤ) (k : Fin 8) : ℤ :=
  (∑ i : Fin 8, X i * C_int i k) * Y k - X k * (∑ j : Fin 8, Y j * C_int k j)

private def v_int (k : Fin 7) (i : Fin 8) : ℤ :=
  if i = k.castSucc then 1 else if i = (7 : Fin 8) then -1 else 0

private lemma v_eq_cast (k : Fin 7) (i : Fin 8) : v k i = (v_int k i : ℚ) := by
  simp only [v, v_int]; split_ifs <;> norm_num

-- mu is linear in its first argument: mu(c·X, Y) = c·mu(X, Y)
private lemma mu_linear_first (c : ℚ) (X Y : Fin 8 → ℚ) (k : Fin 8) :
    mu (fun i => c * X i) Y k = c * mu X Y k := by
  simp only [mu]
  have h : ∑ i : Fin 8, c * X i * C_weight i k = c * ∑ i : Fin 8, X i * C_weight i k := by
    rw [Finset.mul_sum]; congr 1; ext i; ring
  rw [h]; ring

-- General factor: ∑ i, f i * ((g i : ℚ) / D) = (∑ i, f i * (g i : ℚ)) / D.
-- Handles both weighted sums in mu (first arg varies in C_int col, second in row).
private lemma factor_sum (f : Fin 8 → ℚ) (g : Fin 8 → ℤ) :
    ∑ i, f i * ((g i : ℚ) / 1792) = (∑ i, f i * (g i : ℚ)) / 1792 := by
  rw [Finset.sum_div]; congr 1; ext i; ring

-- mu on ℤ-cast inputs = mu_int / 1792 (exact).
private lemma mu_scale (X Y : Fin 8 → ℤ) (k : Fin 8) :
    mu (fun i => (X i : ℚ)) (fun i => (Y i : ℚ)) k = (mu_int X Y k : ℚ) / 1792 := by
  simp only [mu, mu_int, C_weight_scale]
  rw [factor_sum (fun i => (X i : ℚ)) (fun i => C_int i k),
      factor_sum (fun j => (Y j : ℚ)) (fun j => C_int k j)]
  push_cast
  ring

-- 7³ × 8 = 2744 ℤ arithmetic cases.
-- Binary-integer kernel evaluation: no GCD chains, completes in < 1s.
-- Per AGENTS.md §5: decide is preferred over native_decide when feasible.
private lemma Jacobiator_int_zero : ∀ a b c : Fin 7, ∀ ℓ : Fin 8,
    mu_int (mu_int (v_int a) (v_int b)) (v_int c) ℓ +
    mu_int (mu_int (v_int b) (v_int c)) (v_int a) ℓ +
    mu_int (mu_int (v_int c) (v_int a)) (v_int b) ℓ = 0 := by decide

-- Single factor-and-lift: mu(mu(v a, v b), v c) ℓ = cast(mu_int...) / 1792².
-- This captures the pattern previously triplicated in Jacobiator_basis_zero_int.
private lemma mu_double_lift (a b c : Fin 7) (ℓ : Fin 8) :
    mu (mu (v a) (v b)) (v c) ℓ =
    (mu_int (mu_int (v_int a) (v_int b)) (v_int c) ℓ : ℚ) / 1792 ^ 2 := by
  have hva : v a = fun i => (v_int a i : ℚ) := funext (v_eq_cast a)
  have hvb : v b = fun i => (v_int b i : ℚ) := funext (v_eq_cast b)
  have hvc : v c = fun i => (v_int c i : ℚ) := funext (v_eq_cast c)
  have hab : mu (v a) (v b) = fun k => (mu_int (v_int a) (v_int b) k : ℚ) / 1792 :=
    funext fun k => by rw [hva, hvb]; exact mu_scale _ _ k
  rw [hab, hvc]
  have heq : (fun k => (mu_int (v_int a) (v_int b) k : ℚ) / 1792) =
             fun k => (1 / 1792 : ℚ) * (mu_int (v_int a) (v_int b) k : ℚ) := by
    ext; ring
  rw [heq, mu_linear_first (1 / 1792), mu_scale]; ring

-- Jacobiator vanishes on every basis triple (ℚ, lifted from the ℤ computation).
private lemma Jacobiator_basis_zero_int (a b c : Fin 7) :
    Jacobiator mu (v a) (v b) (v c) = 0 := by
  funext ℓ
  simp only [Jacobiator, Pi.add_apply, Pi.zero_apply]
  have habc := mu_double_lift a b c ℓ
  have hbca := mu_double_lift b c a ℓ
  have hcab := mu_double_lift c a b ℓ
  rw [habc, hbca, hcab]
  have hint := Jacobiator_int_zero a b c ℓ
  have hq : (mu_int (mu_int (v_int a) (v_int b)) (v_int c) ℓ : ℚ) +
            (mu_int (mu_int (v_int b) (v_int c)) (v_int a) ℓ : ℚ) +
            (mu_int (mu_int (v_int c) (v_int a)) (v_int b) ℓ : ℚ) = 0 := by
    exact_mod_cast hint
  field_simp
  linarith

/-- Theorem (Gate C): The Jacobiator of μ vanishes on all 7³ = 343 basis
    triples of V.  Proof: integer bypass (decide on ℤ, D=1792 scaling).
    By trilinearity this extends to all of V, proving d_CE μ = 0. -/
theorem Jacobiator_basis_all : ((Finset.univ : Finset (Fin 7)).product
    ((Finset.univ : Finset (Fin 7)).product (Finset.univ : Finset (Fin 7)))).filter
    (λ (ijk : Fin 7 × Fin 7 × Fin 7) => Jacobiator mu (v ijk.1) (v ijk.2.1) (v ijk.2.2) ≠ 0) = ∅ := by
  ext ⟨a, b, c⟩
  refine ⟨fun h => ?_, fun h => (Finset.notMem_empty _ h).elim⟩
  rw [Finset.mem_filter] at h
  exact (h.2 (Jacobiator_basis_zero_int a b c)).elim

/-- Convenience: the Jacobiator vanishes for any single basis triple. -/
lemma Jacobiator_basis_zero (i j k : Fin 7) : Jacobiator mu (v i) (v j) (v k) = 0 :=
  Jacobiator_basis_zero_int i j k

end SilverSight.PIST.CartanConnection