/-
  ============================================================
  SDP CERTIFICATE VERIFICATION ENGINE

  Sparse polynomial arithmetic over ℚ for verifying
  SOS (Sum-of-Squares) certificates produced by external
  SDP solvers.

  Architecture:
  - External SDP solver (Python shim) → rational coefficients
  - This module: expand Σ qᵢ² + Σ sⱼgⱼ, compare with target p
  - Verification is FINITE: polynomial arithmetic + coefficient check
  - native_decide-compatible: all operations are decidable

  Pipeline:
    sdp_sos_solver.py → GoormaghtighCert.lean (data) → here (verify)
  ============================================================
-/

import Mathlib.Data.Rat.Defs
import Mathlib.Data.Fintype.Basic
import Mathlib.Tactic

namespace Semantics.SDPVerify

-- ============================================================
-- §0  SPARSE POLYNOMIAL REPRESENTATION
-- ============================================================

/-- A monomial exponent vector over n variables.
    Example: x₀²x₂³ in 4 variables → fun i => [2, 0, 3, 0][i] -/
abbrev Exponent (n : ℕ) := Fin n → ℕ

/-- A term is a (coefficient, exponent) pair. -/
structure Term (n : ℕ) where
  coeff : ℚ
  expon : Exponent n
  deriving Repr

/-- A sparse polynomial: a list of terms.
    Invariant: no duplicate exponents after normalization.
    Example: 3x₀² + 2x₁ = [(3, [2,0,0,0]), (2, [0,1,0,0])] -/
abbrev SparsePoly (n : ℕ) := List (Term n)

instance : Inhabited (SparsePoly n) := ⟨[]⟩

-- ============================================================
-- §1  EXPONENT OPERATIONS
-- ============================================================

section ExponentOps

/-- Decidable equality for exponent vectors. -/
instance : DecidableEq (Exponent n) := inferInstance

/-- Add two exponent vectors (monomial multiplication).
    x₀²x₁ · x₁x₂ = x₀²x₁²x₂ → [2,1,0,0] + [0,1,1,0] = [2,2,1,0] -/
def exponentAdd {n : ℕ} (a b : Exponent n) : Exponent n :=
  fun i => a i + b i

/-- Zero exponent (constant monomial). -/
def exponentZero (n : ℕ) : Exponent n := fun _ => 0

/-- Compare exponents lexicographically (for sorting/normalization).
    Returns true if a < b in lex order. -/
def exponentLt {n : ℕ} (a b : Exponent n) : Bool :=
  let rec go (i : ℕ) : Bool :=
    if h : i < n then
      if a ⟨i, h⟩ < b ⟨i, h⟩ then true
      else if a ⟨i, h⟩ > b ⟨i, h⟩ then false
      else go (i + 1)
    else false
  go 0

/-- Check exponent equality. -/
def exponentEq {n : ℕ} (a b : Exponent n) : Bool :=
  (List.range n).all fun i =>
    match Nat.decLt i n with
    | .isTrue h => a ⟨i, h⟩ == b ⟨i, h⟩
    | .isFalse _ => true

end ExponentOps

-- ============================================================
-- §2  POLYNOMIAL ARITHMETIC
-- ============================================================

section PolyArith

/-- The zero polynomial. -/
def zeroPoly (n : ℕ) : SparsePoly n := []

/-- A constant polynomial. -/
def constPoly {n : ℕ} (c : ℚ) : SparsePoly n :=
  if c == 0 then [] else [⟨c, exponentZero n⟩]

/-- A single-variable monomial: c · xᵢᵏ -/
def monomialPoly {n : ℕ} (c : ℚ) (var : Fin n) (deg : ℕ) : SparsePoly n :=
  if c == 0 then []
  else [⟨c, fun j => if j == var then deg else 0⟩]

/-- Add two sparse polynomials (concatenate terms, normalize later). -/
def addPoly {n : ℕ} (p q : SparsePoly n) : SparsePoly n := p ++ q

/-- Scale a polynomial by a rational constant. -/
def scalePoly {n : ℕ} (c : ℚ) (p : SparsePoly n) : SparsePoly n :=
  p.map fun t => ⟨c * t.coeff, t.expon⟩

/-- Negate a polynomial. -/
def negPoly {n : ℕ} (p : SparsePoly n) : SparsePoly n :=
  p.map fun t => ⟨-t.coeff, t.expon⟩

/-- Multiply a single term by a polynomial. -/
def mulTermPoly {n : ℕ} (t : Term n) (p : SparsePoly n) : SparsePoly n :=
  p.map fun s => ⟨t.coeff * s.coeff, exponentAdd t.expon s.expon⟩

/-- Multiply two sparse polynomials (distribute and collect). -/
def mulPoly {n : ℕ} (p q : SparsePoly n) : SparsePoly n :=
  p.foldl (fun acc t => acc ++ mulTermPoly t q) []

/-- Square a polynomial: p² = p · p. -/
def sqPoly {n : ℕ} (p : SparsePoly n) : SparsePoly n :=
  mulPoly p p

/-- Sum of squares: Σᵢ qᵢ². -/
def sumSqPoly {n : ℕ} (qs : List (SparsePoly n)) : SparsePoly n :=
  qs.foldl (fun acc q => addPoly acc (sqPoly q)) (zeroPoly n)

/-- Weighted sum: Σⱼ sⱼ · gⱼ. -/
def weightedSumPoly {n : ℕ} (pairs : List (SparsePoly n × SparsePoly n)) : SparsePoly n :=
  pairs.foldl (fun acc (s, g) => addPoly acc (mulPoly s g)) (zeroPoly n)

end PolyArith

-- ============================================================
-- §3  NORMALIZATION (collect like terms, sort, drop zeros)
-- ============================================================

section Normalize

/-- Insert a term into a sorted (by exponent) accumulator,
    merging coefficients if the exponent already exists. -/
def insertTerm {n : ℕ} (t : Term n) (acc : List (Term n)) : List (Term n) :=
  match acc with
  | [] => [t]
  | h :: rest =>
    if t.expon == h.expon then
      ⟨t.coeff + h.coeff, h.expon⟩ :: rest
    else if exponentLt t.expon h.expon then
      t :: h :: rest
    else
      h :: insertTerm t rest

/-- Normalize a polynomial: collect like terms, sort by exponent, drop zeros.
    After normalization, no two terms share the same exponent. -/
def normalizePoly {n : ℕ} (p : SparsePoly n) : SparsePoly n :=
  let sorted := p.foldl (fun acc t => insertTerm t acc) []
  sorted.filter fun t => t.coeff != 0

end Normalize

-- ============================================================
-- §4  COEFFICIENT-WISE EQUALITY
-- ============================================================

section Equality

/-- Check if two normalized polynomials are equal (same terms in order). -/
def polyEqNormalized {n : ℕ} (p q : List (Term n)) : Bool :=
  match p, q with
  | [], [] => true
  | [], _ => false
  | _, [] => false
  | hp :: rp, hq :: rq =>
    hp.expon == hq.expon &&
    hp.coeff == hq.coeff &&
    polyEqNormalized rp rq

/-- Check if two sparse polynomials are equal
    (normalize both, then compare). -/
def polyEq {n : ℕ} (p q : SparsePoly n) : Bool :=
  polyEqNormalized (normalizePoly p) (normalizePoly q)

/-- Check if a polynomial is zero (all coefficients vanish). -/
def polyIsZero {n : ℕ} (p : SparsePoly n) : Bool :=
  (normalizePoly p).isEmpty

end Equality

-- ============================================================
-- §5  CERTIFICATE VERIFICATION
-- ============================================================

section Verify

/-- An SDP certificate: the output of the SDP solver, rationalized.
    Contains:
    - sos_components: the SOS polynomials qᵢ (each as SparsePoly)
    - weighted_pairs: the weighted SOS pairs (sⱼ, gⱼ)
    - target: the polynomial p to verify against

    The certificate is VALID iff:
      normalize(Σ qᵢ² + Σ sⱼ·gⱼ) = normalize(p) -/
structure SDPCertificate (n : ℕ) where
  sos_components : List (SparsePoly n)
  weighted_pairs : List (SparsePoly n × SparsePoly n)
  target         : SparsePoly n
  degree         : ℕ
  level          : ℕ

/-- Verify an SDP certificate: expand the SOS representation and
    check coefficient-wise equality with the target polynomial.

    This is the KEY function. It replaces the sorry in PutinarBackbone.
    The computation is FINITE and EXACT (rational arithmetic).

    Returns true iff: Σ qᵢ² + Σ sⱼ·gⱼ = p (coefficient-wise). -/
def verifyCertificate {n : ℕ} (cert : SDPCertificate n) : Bool :=
  let sosSum := sumSqPoly cert.sos_components
  let weightedSum := weightedSumPoly cert.weighted_pairs
  let lhs := addPoly sosSum weightedSum
  polyEq lhs cert.target

/-- Verify that all SOS components are well-formed:
    each has finite degree and rational coefficients. -/
def verifyCertificateWellFormed {n : ℕ} (cert : SDPCertificate n) : Bool :=
  -- Check that the SOS components are non-empty
  !cert.sos_components.isEmpty &&
  -- Check that all coefficients are finite (not NaN — always true for ℚ)
  true

end Verify

-- ============================================================
-- §6  SOUNDNESS
-- ============================================================

section Soundness

/-- Evaluate a single term at point x. -/
def evalTerm {n : ℕ} (t : Term n) (x : Fin n → ℝ) : ℝ :=
  (t.coeff : ℝ) * Finset.univ.prod (fun i : Fin n => x i ^ t.expon i)

/-- Evaluate a sparse polynomial at a point (semantic evaluation).
    Maps the algebraic representation to the semantic value. -/
noncomputable def evalSparsePoly {n : ℕ} (p : SparsePoly n) (x : Fin n → ℝ) : ℝ :=
  p.foldl (fun acc t => acc + evalTerm t x) 0

/-- Pure arithmetic lemma: foldl + a distributes.
    Proved by induction without touching evalSparsePoly, so no loop risk. -/
lemma foldl_add {n : ℕ} (a : ℝ) (p : SparsePoly n) (x : Fin n → ℝ) :
    p.foldl (fun acc t => acc + evalTerm t x) a = a + p.foldl (fun acc t => acc + evalTerm t x) 0 := by
  induction p generalizing a with
  | nil => simp
  | cons t ts ih =>
    calc
      (t :: ts).foldl (fun acc t => acc + evalTerm t x) a
          = ts.foldl (fun acc t => acc + evalTerm t x) (a + evalTerm t x) := rfl
      _ = (a + evalTerm t x) + ts.foldl (fun acc t => acc + evalTerm t x) 0 := by rw [ih (a + evalTerm t x)]
      _ = a + (evalTerm t x + ts.foldl (fun acc t => acc + evalTerm t x) 0) := by ring
      _ = a + ((t :: ts).foldl (fun acc t => acc + evalTerm t x) 0) := by
        have h : evalTerm t x + ts.foldl (fun acc t => acc + evalTerm t x) 0
            = (t :: ts).foldl (fun acc t => acc + evalTerm t x) 0 := by
          calc
            evalTerm t x + ts.foldl (fun acc t => acc + evalTerm t x) 0
                = ts.foldl (fun acc t => acc + evalTerm t x) (evalTerm t x) := by rw [ih (evalTerm t x)]
            _ = (t :: ts).foldl (fun acc t => acc + evalTerm t x) 0 := by simp
        rw [h]

lemma evalSparsePoly_foldl_add {n : ℕ} (a : ℝ) (p : SparsePoly n) (x : Fin n → ℝ) :
    p.foldl (fun acc t => acc + evalTerm t x) a = a + evalSparsePoly p x := by
  rw [foldl_add, evalSparsePoly]

lemma eval_cons {n : ℕ} (t : Term n) (ts : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (t :: ts) x = evalTerm t x + evalSparsePoly ts x := by
  calc
    evalSparsePoly (t :: ts) x = (t :: ts).foldl (fun acc t => acc + evalTerm t x) 0 := rfl
    _ = ts.foldl (fun acc t => acc + evalTerm t x) (evalTerm t x) := by simp
    _ = evalTerm t x + evalSparsePoly ts x := by rw [evalSparsePoly_foldl_add]

lemma evalSparsePoly_append {n : ℕ} (p q : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (p ++ q) x = evalSparsePoly p x + evalSparsePoly q x := by
  induction p generalizing q with
  | nil => simp [evalSparsePoly]
  | cons t ts ih =>
    calc
      evalSparsePoly ((t :: ts) ++ q) x
          = evalSparsePoly (t :: (ts ++ q)) x := by simp
      _ = evalTerm t x + evalSparsePoly (ts ++ q) x := by rw [eval_cons]
      _ = evalTerm t x + (evalSparsePoly ts x + evalSparsePoly q x) := by rw [ih]
      _ = (evalTerm t x + evalSparsePoly ts x) + evalSparsePoly q x := by ring
      _ = evalSparsePoly (t :: ts) x + evalSparsePoly q x := by rw [eval_cons]

lemma evalTerm_exponentAdd {n : ℕ} (t s : Term n) (x : Fin n → ℝ) :
    evalTerm { coeff := t.coeff * s.coeff, expon := exponentAdd t.expon s.expon } x = evalTerm t x * evalTerm s x := by
  dsimp [evalTerm, exponentAdd]
  calc
    ((t.coeff * s.coeff : ℚ) : ℝ) * ∏ i : Fin n, x i ^ (t.expon i + s.expon i)
        = ((t.coeff : ℚ) : ℝ) * ((s.coeff : ℚ) : ℝ) * ∏ i : Fin n, (x i ^ t.expon i * x i ^ s.expon i) := by
      simp [mul_assoc, pow_add]
    _ = ((t.coeff : ℚ) : ℝ) * ((s.coeff : ℚ) : ℝ) * ((∏ i : Fin n, x i ^ t.expon i) * (∏ i : Fin n, x i ^ s.expon i)) := by
      rw [Finset.prod_mul_distrib]
    _ = ((t.coeff : ℚ) : ℝ) * (∏ i : Fin n, x i ^ t.expon i) * (((s.coeff : ℚ) : ℝ) * (∏ i : Fin n, x i ^ s.expon i)) := by ring
    _ = evalTerm t x * evalTerm s x := rfl

lemma eval_mulTermPoly {n : ℕ} (t : Term n) (q : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (mulTermPoly t q) x = evalTerm t x * evalSparsePoly q x := by
  induction q with
  | nil => simp [evalSparsePoly, mulTermPoly]
  | cons s ss ih =>
    calc
      evalSparsePoly (mulTermPoly t (s :: ss)) x
          = evalSparsePoly ([⟨t.coeff * s.coeff, exponentAdd t.expon s.expon⟩] ++ mulTermPoly t ss) x := by
        simp [mulTermPoly]
      _ = evalSparsePoly [⟨t.coeff * s.coeff, exponentAdd t.expon s.expon⟩] x + evalSparsePoly (mulTermPoly t ss) x := by
        rw [evalSparsePoly_append]
      _ = (evalTerm t x * evalTerm s x) + (evalTerm t x * evalSparsePoly ss x) := by
        have h_single : evalSparsePoly [⟨t.coeff * s.coeff, exponentAdd t.expon s.expon⟩] x
            = evalTerm ⟨t.coeff * s.coeff, exponentAdd t.expon s.expon⟩ x := by
          simp [evalSparsePoly]
        rw [h_single, ih, evalTerm_exponentAdd t s x]
      _ = evalTerm t x * (evalTerm s x + evalSparsePoly ss x) := by ring
      _ = evalTerm t x * evalSparsePoly (s :: ss) x := by rw [eval_cons]

lemma eval_mul {n : ℕ} (p q : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (mulPoly p q) x = evalSparsePoly p x * evalSparsePoly q x := by
  induction p generalizing q with
  | nil => simp [evalSparsePoly, mulPoly]
  | cons t ts ih =>
    calc
      evalSparsePoly (mulPoly (t :: ts) q) x
          = evalSparsePoly (mulTermPoly t q ++ mulPoly ts q) x := by
        simp [mulPoly, List.foldl]
      _ = evalSparsePoly (mulTermPoly t q) x + evalSparsePoly (mulPoly ts q) x := by
        rw [evalSparsePoly_append]
      _ = (evalTerm t x * evalSparsePoly q x) + (evalSparsePoly ts x * evalSparsePoly q x) := by
        simp [eval_mulTermPoly, ih]
      _ = (evalTerm t x + evalSparsePoly ts x) * evalSparsePoly q x := by ring
      _ = evalSparsePoly (t :: ts) x * evalSparsePoly q x := by rw [eval_cons]

lemma eval_sqPoly {n : ℕ} (q : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (sqPoly q) x = (evalSparsePoly q x)^2 := by
  rw [sqPoly, eval_mul]; ring

lemma sumSqPoly_foldl_add {n : ℕ} (acc : SparsePoly n) (qs : List (SparsePoly n)) :
    qs.foldl (fun acc' q => addPoly acc' (sqPoly q)) acc = addPoly acc (sumSqPoly qs) := by
  induction qs generalizing acc with
  | nil => simp [sumSqPoly, zeroPoly, addPoly]
  | cons q qs ih =>
    simp [sumSqPoly, List.foldl, addPoly, ih, List.append_assoc, zeroPoly]

lemma eval_sumSqPoly {n : ℕ} (qs : List (SparsePoly n)) (x : Fin n → ℝ) :
    evalSparsePoly (sumSqPoly qs) x = (qs.map (fun q => (evalSparsePoly q x)^2)).sum := by
  induction qs with
  | nil => simp [evalSparsePoly, sumSqPoly, zeroPoly]
  | cons q qs ih =>
    calc
      evalSparsePoly (sumSqPoly (q :: qs)) x
          = evalSparsePoly (qs.foldl (fun acc' q => addPoly acc' (sqPoly q)) (sqPoly q)) x := by
        simp [sumSqPoly, addPoly, List.foldl, zeroPoly]
      _ = evalSparsePoly (addPoly (sqPoly q) (sumSqPoly qs)) x := by
        rw [sumSqPoly_foldl_add (sqPoly q) qs]
      _ = evalSparsePoly (sqPoly q ++ sumSqPoly qs) x := by rw [addPoly]
      _ = evalSparsePoly (sqPoly q) x + evalSparsePoly (sumSqPoly qs) x := by rw [evalSparsePoly_append]
      _ = (evalSparsePoly q x)^2 + (qs.map (fun q => (evalSparsePoly q x)^2)).sum := by
        simp [eval_sqPoly, ih]
      _ = ((q :: qs).map (fun q => (evalSparsePoly q x)^2)).sum := by simp

lemma weightedSumPoly_foldl_add {n : ℕ} (acc : SparsePoly n) (pairs : List (SparsePoly n × SparsePoly n)) :
    pairs.foldl (fun acc' (s, g) => addPoly acc' (mulPoly s g)) acc = addPoly acc (weightedSumPoly pairs) := by
  induction pairs generalizing acc with
  | nil => simp [weightedSumPoly, zeroPoly, addPoly]
  | cons pair pairs ih =>
    rcases pair with ⟨s, g⟩
    simp [weightedSumPoly, List.foldl, addPoly, ih, List.append_assoc, zeroPoly]

lemma eval_weightedSumPoly {n : ℕ} (pairs : List (SparsePoly n × SparsePoly n)) (x : Fin n → ℝ) :
    evalSparsePoly (weightedSumPoly pairs) x =
    (pairs.map (fun (s, g) => evalSparsePoly s x * evalSparsePoly g x)).sum := by
  induction pairs with
  | nil => simp [evalSparsePoly, weightedSumPoly, zeroPoly]
  | cons pair pairs ih =>
    rcases pair with ⟨s, g⟩
    calc
      evalSparsePoly (weightedSumPoly (⟨s, g⟩ :: pairs)) x
          = evalSparsePoly (pairs.foldl (fun acc' (s, g) => addPoly acc' (mulPoly s g)) (mulPoly s g)) x := by
        simp [weightedSumPoly, addPoly, List.foldl, zeroPoly]
      _ = evalSparsePoly (addPoly (mulPoly s g) (weightedSumPoly pairs)) x := by
        rw [weightedSumPoly_foldl_add (mulPoly s g) pairs]
      _ = evalSparsePoly (mulPoly s g ++ weightedSumPoly pairs) x := by rw [addPoly]
      _ = evalSparsePoly (mulPoly s g) x + evalSparsePoly (weightedSumPoly pairs) x := by rw [evalSparsePoly_append]
      _ = (evalSparsePoly s x * evalSparsePoly g x) + (pairs.map (fun (s, g) => evalSparsePoly s x * evalSparsePoly g x)).sum := by
        simp [eval_mul, ih]
      _ = ((⟨s, g⟩ :: pairs).map (fun (s, g) => evalSparsePoly s x * evalSparsePoly g x)).sum := by simp

theorem sqPoly_eval_nonneg {n : ℕ} (q : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (sqPoly q) x ≥ 0 := by
  rw [eval_sqPoly]
  exact sq_nonneg _

lemma evalTerm_add_same_exponent {n : ℕ} (t s : Term n) (x : Fin n → ℝ) (h_exp : t.expon = s.expon) :
    evalTerm t x + evalTerm s x = evalTerm { coeff := t.coeff + s.coeff, expon := t.expon } x := by
  have h_prod : ∏ i : Fin n, x i ^ t.expon i = ∏ i : Fin n, x i ^ s.expon i := by
    simpa [h_exp]
  simp [evalTerm, h_prod, add_mul, push_cast]

lemma eval_insertTerm {n : ℕ} (t : Term n) (acc : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (insertTerm t acc) x = evalTerm t x + evalSparsePoly acc x := by
  induction acc generalizing t with
  | nil => simp [evalSparsePoly, insertTerm, evalTerm]
  | cons h rest ih =>
    by_cases h_eq : (t.expon == h.expon) = true
    · have hexp : t.expon = h.expon := by simpa using h_eq
      rw [insertTerm, if_pos h_eq, eval_cons]
      calc
        evalTerm { coeff := t.coeff + h.coeff, expon := h.expon } x + evalSparsePoly rest x
            = evalTerm { coeff := t.coeff + h.coeff, expon := t.expon } x + evalSparsePoly rest x := by
          rw [hexp]
        _ = (evalTerm t x + evalTerm h x) + evalSparsePoly rest x := by
          rw [evalTerm_add_same_exponent t h x hexp]
        _ = evalTerm t x + (evalTerm h x + evalSparsePoly rest x) := by ring
        _ = evalTerm t x + evalSparsePoly (h :: rest) x := by rw [eval_cons]
    · by_cases h_lt : exponentLt t.expon h.expon = true
      · -- exponentLt true: t goes before h
        have h_ne : t.expon ≠ h.expon := by
          intro heq
          apply h_eq
          simpa [heq]
        have h_eq_false' : (t.expon == h.expon) = false :=
          Bool.eq_false_of_not_eq_true (by
            intro h_eq_true
            apply h_ne
            simpa using h_eq_true)
        have h_ins : insertTerm t (h :: rest) = t :: h :: rest := by
          have h_eq_def : insertTerm t (h :: rest) =
            (if t.expon == h.expon then ⟨t.coeff + h.coeff, h.expon⟩ :: rest
             else if exponentLt t.expon h.expon then t :: h :: rest
             else h :: insertTerm t rest) := by rfl
          rw [h_eq_def, h_eq_false', h_lt]
          simp
        rw [h_ins, eval_cons]
      · -- exponentLt false: h stays before t, insert t into rest
        have h_ne : t.expon ≠ h.expon := by
          intro heq
          apply h_eq
          simpa [heq]
        have h_eq_false' : (t.expon == h.expon) = false :=
          Bool.eq_false_of_not_eq_true (by
            intro h_eq_true
            apply h_ne
            simpa using h_eq_true)
        have h_lt_false : exponentLt t.expon h.expon = false :=
          Bool.eq_false_of_not_eq_true h_lt
        have h_ins : insertTerm t (h :: rest) = h :: insertTerm t rest := by
          have h_eq_def : insertTerm t (h :: rest) =
            (if t.expon == h.expon then ⟨t.coeff + h.coeff, h.expon⟩ :: rest
             else if exponentLt t.expon h.expon then t :: h :: rest
             else h :: insertTerm t rest) := by rfl
          rw [h_eq_def, h_eq_false', h_lt_false]
          simp
        rw [h_ins]
        calc
          evalSparsePoly (h :: insertTerm t rest) x
              = evalTerm h x + evalSparsePoly (insertTerm t rest) x := by rw [eval_cons]
          _ = evalTerm h x + (evalTerm t x + evalSparsePoly rest x) := by rw [ih]
          _ = evalTerm t x + (evalTerm h x + evalSparsePoly rest x) := by ring
          _ = evalTerm t x + evalSparsePoly (h :: rest) x := by rw [eval_cons]

lemma eval_filter_nonzero_eq_eval {n : ℕ} (p : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (p.filter fun t : Term n => t.coeff != 0) x = evalSparsePoly p x := by
  induction p with
  | nil => rfl
  | cons t ts ih =>
    by_cases h : t.coeff = 0
    · calc
        evalSparsePoly (List.filter (fun t : Term n => t.coeff != 0) (t :: ts)) x
            = evalSparsePoly (List.filter (fun t : Term n => t.coeff != 0) ts) x := by
          simp [h, List.filter]
        _ = evalSparsePoly ts x := by rw [ih]
        _ = evalTerm t x + evalSparsePoly ts x := by
          simp [evalTerm, h]
        _ = evalSparsePoly (t :: ts) x := by rw [eval_cons]
    · have h' : t.coeff ≠ 0 := by
        intro hzero
        exact h hzero
      have h_bool : (t.coeff != 0) = true := by
        simp [h']
      have hfilter : List.filter (fun t : Term n => t.coeff != 0) (t :: ts) = t :: List.filter (fun t : Term n => t.coeff != 0) ts := by
        simp [List.filter, h_bool]
      calc
        evalSparsePoly (List.filter (fun t : Term n => t.coeff != 0) (t :: ts)) x
            = evalSparsePoly (t :: List.filter (fun t : Term n => t.coeff != 0) ts) x := by rw [hfilter]
        _ = evalTerm t x + evalSparsePoly (List.filter (fun t : Term n => t.coeff != 0) ts) x := by rw [eval_cons]
        _ = evalTerm t x + evalSparsePoly ts x := by rw [ih]
        _ = evalSparsePoly (t :: ts) x := by rw [eval_cons]

lemma foldl_insertTerm_eval {n : ℕ} (acc : SparsePoly n) (p : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (p.foldl (fun acc' t => insertTerm t acc') acc) x = evalSparsePoly acc x + evalSparsePoly p x := by
  induction p generalizing acc with
  | nil => simp [evalSparsePoly]
  | cons t ts ih =>
    calc
      evalSparsePoly ((t :: ts).foldl (fun acc' t => insertTerm t acc') acc) x
          = evalSparsePoly (ts.foldl (fun acc' t => insertTerm t acc') (insertTerm t acc)) x := rfl
      _ = evalSparsePoly (insertTerm t acc) x + evalSparsePoly ts x := by rw [ih (insertTerm t acc)]
      _ = (evalTerm t x + evalSparsePoly acc x) + evalSparsePoly ts x := by rw [eval_insertTerm]
      _ = evalSparsePoly acc x + (evalTerm t x + evalSparsePoly ts x) := by ring
      _ = evalSparsePoly acc x + evalSparsePoly (t :: ts) x := by rw [eval_cons]

lemma eval_normalizePoly_eq_eval {n : ℕ} (p : SparsePoly n) (x : Fin n → ℝ) :
    evalSparsePoly (normalizePoly p) x = evalSparsePoly p x := by
  unfold normalizePoly
  have hfoldl : evalSparsePoly (p.foldl (fun acc' t => insertTerm t acc') []) x = evalSparsePoly p x := by
    simpa [evalSparsePoly] using foldl_insertTerm_eval [] p x
  have hfilter : evalSparsePoly ((p.foldl (fun acc' t => insertTerm t acc') []).filter
      fun t : Term n => t.coeff != 0) x = evalSparsePoly (p.foldl (fun acc' t => insertTerm t acc') []) x :=
    eval_filter_nonzero_eq_eval _ x
  rw [hfilter, hfoldl]

lemma and_eq_true_iff (a b : Bool) : (a && b) = true ↔ a = true ∧ b = true := by
  constructor
  · intro h
    have ha : a = true := by
      cases a
      · simp at h
      · rfl
    have hb : b = true := by
      rw [ha] at h
      simp at h
      exact h
    exact ⟨ha, hb⟩
  · intro ⟨ha, hb⟩; simp [ha, hb]

lemma polyEqNormalized_eq {n : ℕ} (p q : List (Term n)) (h : polyEqNormalized p q = true) : p = q := by
  induction p generalizing q with
  | nil =>
    cases q
    · rfl
    · simp [polyEqNormalized] at h
  | cons hp rp ih =>
    cases q
    · simp [polyEqNormalized] at h
    · rename_i hq rq
      simp [polyEqNormalized] at h
      rcases h with ⟨⟨hexp, hcoeff⟩, hrest⟩
      have hrp_eq_rq : rp = rq := ih rq hrest
      have hhp_eq_hq : hp = hq := by
        cases hp; cases hq
        dsimp at hcoeff hexp
        subst hcoeff; subst hexp; rfl
      calc
        hp :: rp = hq :: rp := by rw [hhp_eq_hq]
        _ = hq :: rq := by rw [hrp_eq_rq]

lemma polyEqNormalized_eval_eq {n : ℕ} (p q : List (Term n)) (h : polyEqNormalized p q = true) (x : Fin n → ℝ) :
    evalSparsePoly p x = evalSparsePoly q x := by
  have h_eq : p = q := polyEqNormalized_eq p q h
  subst h_eq; rfl

lemma polyEq_eval_eq {n : ℕ} (p q : SparsePoly n) (h : polyEq p q = true) (x : Fin n → ℝ) :
    evalSparsePoly p x = evalSparsePoly q x := by
  have h_norm_eq : polyEqNormalized (normalizePoly p) (normalizePoly q) = true := h
  have h_eval_norm_eq : evalSparsePoly (normalizePoly p) x = evalSparsePoly (normalizePoly q) x :=
    polyEqNormalized_eval_eq _ _ h_norm_eq x
  have h_eval_p_norm : evalSparsePoly (normalizePoly p) x = evalSparsePoly p x := eval_normalizePoly_eq_eval p x
  have h_eval_q_norm : evalSparsePoly (normalizePoly q) x = evalSparsePoly q x := eval_normalizePoly_eq_eval q x
  rw [← h_eval_p_norm, h_eval_norm_eq, h_eval_q_norm]

theorem verifyCertificate_sound {n : ℕ} (cert : SDPCertificate n)
    (x : Fin n → ℝ)
    (h_verify : verifyCertificate cert = true)
    (h_weight_sos : ∀ pair ∈ cert.weighted_pairs,
      evalSparsePoly pair.1 x ≥ 0)
    (h_constraints : ∀ pair ∈ cert.weighted_pairs,
      evalSparsePoly pair.2 x ≥ 0) :
    evalSparsePoly cert.target x ≥ 0 := by
  have hpoly_eq : polyEq (addPoly (sumSqPoly cert.sos_components) (weightedSumPoly cert.weighted_pairs)) cert.target = true := h_verify
  have heval_eq : evalSparsePoly (addPoly (sumSqPoly cert.sos_components) (weightedSumPoly cert.weighted_pairs)) x = evalSparsePoly cert.target x :=
    polyEq_eval_eq _ _ hpoly_eq x
  rw [← heval_eq]
  have hsos_nonneg : evalSparsePoly (sumSqPoly cert.sos_components) x ≥ 0 := by
    rw [eval_sumSqPoly]
    refine List.sum_nonneg ?_
    intro y hy
    rcases List.mem_map.mp hy with ⟨q, hq, rfl⟩
    exact pow_two_nonneg _
  have hweighted_nonneg : evalSparsePoly (weightedSumPoly cert.weighted_pairs) x ≥ 0 := by
    rw [eval_weightedSumPoly]
    refine List.sum_nonneg ?_
    intro y hy
    rcases List.mem_map.mp hy with ⟨⟨s, g⟩, hpair, rfl⟩
    have hs_nonneg : evalSparsePoly s x ≥ 0 := h_weight_sos ⟨s, g⟩ hpair
    have hg_nonneg : evalSparsePoly g x ≥ 0 := h_constraints ⟨s, g⟩ hpair
    nlinarith
  have h_add : evalSparsePoly (addPoly (sumSqPoly cert.sos_components) (weightedSumPoly cert.weighted_pairs)) x =
    evalSparsePoly (sumSqPoly cert.sos_components) x + evalSparsePoly (weightedSumPoly cert.weighted_pairs) x := by
    simp [evalSparsePoly_append, addPoly]
  rw [h_add]
  nlinarith

end Soundness

-- ============================================================
-- §7  CONVENIENCE CONSTRUCTORS (for certificate data files)
-- ============================================================

section Constructors

/-- Build a SparsePoly from a list of (coefficient, exponent-list) pairs.
    The exponent list is padded/truncated to length n.
    Example: mkPoly 4 [(3, [2,0,0,0]), (1, [0,0,1,0])] = 3x₀² + x₂ -/
def mkPoly (n : ℕ) (terms : List (ℚ × List ℕ)) : SparsePoly n :=
  terms.map fun (c, es) =>
    { coeff := c
      expon := fun i =>
        if h : i.val < es.length then es[i.val]'h else 0 }

/-- Build a certificate from raw data (as output by the Python shim). -/
def mkCertificate (n : ℕ)
    (sos_data : List (List (ℚ × List ℕ)))
    (weighted_data : List (List (ℚ × List ℕ) × List (ℚ × List ℕ)))
    (target_data : List (ℚ × List ℕ))
    (degree level : ℕ) : SDPCertificate n :=
  { sos_components := sos_data.map (mkPoly n)
    weighted_pairs := weighted_data.map fun (s, g) => (mkPoly n s, mkPoly n g)
    target := mkPoly n target_data
    degree := degree
    level := level }

end Constructors

-- ============================================================
-- §8  SIMPLE TEST CASES
-- ============================================================

section Tests

/-- Test: x₀² + x₁² ≥ 0.
    SOS certificate: q₀ = x₀, q₁ = x₁.
    Σ qᵢ² = x₀² + x₁² = p. Trivial. -/
def testCertSimple : SDPCertificate 2 :=
  mkCertificate 2
    -- SOS components: [x₀, x₁]
    [ [(1, [1, 0])],   -- q₀ = x₀
      [(1, [0, 1])] ]  -- q₁ = x₁
    -- No weighted pairs
    []
    -- Target: x₀² + x₁²
    [(1, [2, 0]), (1, [0, 2])]
    -- degree = 2, level = 0
    2 0

-- Verify the simple test case.
#eval! verifyCertificate testCertSimple  -- Expected: true

/-- Test: (x₀ + x₁)² = x₀² + 2x₀x₁ + x₁².
    SOS certificate: q₀ = x₀ + x₁.
    q₀² = x₀² + 2x₀x₁ + x₁² = p. -/
def testCertBinomial : SDPCertificate 2 :=
  mkCertificate 2
    -- SOS components: [x₀ + x₁]
    [ [(1, [1, 0]), (1, [0, 1])] ]  -- q₀ = x₀ + x₁
    -- No weighted pairs
    []
    -- Target: x₀² + 2x₀x₁ + x₁²
    [(1, [2, 0]), (2, [1, 1]), (1, [0, 2])]
    -- degree = 2, level = 0
    2 0

#eval! verifyCertificate testCertBinomial  -- Expected: true

/-- Test: x₀² + x₁² + 1 ≥ 0.
    SOS certificate: q₀ = x₀, q₁ = x₁, q₂ = 1.
    Σ qᵢ² = x₀² + x₁² + 1 = p. -/
def testCertWithConstant : SDPCertificate 2 :=
  mkCertificate 2
    [ [(1, [1, 0])],   -- q₀ = x₀
      [(1, [0, 1])],   -- q₁ = x₁
      [(1, [0, 0])] ]  -- q₂ = 1
    []
    [(1, [2, 0]), (1, [0, 2]), (1, [0, 0])]
    2 0

#eval! verifyCertificate testCertWithConstant  -- Expected: true

/-- Test with weighted constraint: p = x₀² + x₀ ≥ 0 on K = {x₀ ≥ 0}.
    Certificate: p = x₀² + x₀ · 1  (where g₀ = x₀, s₀ = 1)
    So: sos_components = [], weighted = [(1, x₀)]
    But x₀² needs an SOS component too.
    Actually: p = x₀² + x₀ = x₀² + 1·g₀ where g₀ = x₀.
    SOS components: [x₀] (for x₀²), weighted: [([1], [x₀])] (for x₀). -/
def testCertWeighted : SDPCertificate 1 :=
  mkCertificate 1
    [ [(1, [1])] ]          -- q₀ = x₀ → q₀² = x₀²
    [ ([(1, [0])],          -- s₀ = 1 (constant, SOS-compatible)
       [(1, [1])]) ]        -- g₀ = x₀ (constraint)
    [(1, [2]), (1, [1])]    -- p = x₀² + x₀
    2 1

#eval! verifyCertificate testCertWeighted  -- Expected: true

/-- Negative test: wrong certificate should return false. -/
def testCertWrong : SDPCertificate 2 :=
  mkCertificate 2
    [ [(1, [1, 0])] ]  -- q₀ = x₀ → q₀² = x₀² (missing x₁²)
    []
    [(1, [2, 0]), (1, [0, 2])]  -- p = x₀² + x₁²
    2 0

#eval! verifyCertificate testCertWrong  -- Expected: false

end Tests

end Semantics.SDPVerify