/-
  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

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

-- mu on ℤ-cast inputs = mu_int / 1792 (exact).
-- ring cannot handle Finset.sum directly; we factor 1/1792 from each sum first.
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]
  -- Factor 1/1792 from each weighted sum: ∑ f*(c/D) = (∑ f*c)/D
  have factor : ∀ (f : Fin 8 → ℤ) (j : Fin 8),
      ∑ i : Fin 8, (f i : ℚ) * ((C_int i j : ℚ) / 1792) =
      (∑ i : Fin 8, (f i : ℚ) * (C_int i j : ℚ)) / 1792 := fun f j => by
    rw [Finset.sum_div]; congr 1; ext i; ring
  rw [factor X k, factor Y k]
  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

-- 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]
  -- Rewrite each v k as a cast of v_int k
  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)
  -- Inner mu: mu(cast X)(cast Y) k = cast(mu_int X Y k) / 1792
  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
  have hbc : mu (v b) (v c) = fun k => (mu_int (v_int b) (v_int c) k : ℚ) / 1792 :=
    funext fun k => by rw [hvb, hvc]; exact mu_scale _ _ k
  have hca : mu (v c) (v a) = fun k => (mu_int (v_int c) (v_int a) k : ℚ) / 1792 :=
    funext fun k => by rw [hvc, hva]; exact mu_scale _ _ k
  -- Outer mu: mu((cast Z)/1792)(cast W) = cast(mu_int Z W) / 1792²
  -- Step: rewrite first arg as (1/1792)·cast Z, apply linearity, then mu_scale.
  have habc : mu (mu (v a) (v b)) (v c) ℓ =
      (mu_int (mu_int (v_int a) (v_int b)) (v_int c) ℓ : ℚ) / 1792 ^ 2 := by
    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
  have hbca : mu (mu (v b) (v c)) (v a) ℓ =
      (mu_int (mu_int (v_int b) (v_int c)) (v_int a) ℓ : ℚ) / 1792 ^ 2 := by
    rw [hbc, hva]
    have heq : (fun k => (mu_int (v_int b) (v_int c) k : ℚ) / 1792) =
               fun k => (1 / 1792 : ℚ) * (mu_int (v_int b) (v_int c) k : ℚ) := by
      ext; ring
    rw [heq, mu_linear_first (1 / 1792), mu_scale]; ring
  have hcab : mu (mu (v c) (v a)) (v b) ℓ =
      (mu_int (mu_int (v_int c) (v_int a)) (v_int b) ℓ : ℚ) / 1792 ^ 2 := by
    rw [hca, hvb]
    have heq : (fun k => (mu_int (v_int c) (v_int a) k : ℚ) / 1792) =
               fun k => (1 / 1792 : ℚ) * (mu_int (v_int c) (v_int a) k : ℚ) := by
      ext; ring
    rw [heq, mu_linear_first (1 / 1792), mu_scale]; ring
  rw [habc, hbca, hcab]
  -- Integer sum = 0 (by decide), cast to ℚ, clear 1792² denominator
  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⟩
  simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_univ, true_and,
             Finset.not_mem_empty, iff_false, ne_eq, not_not]
  exact Jacobiator_basis_zero_int a b c

/-- 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
