lean/QLG.lean

/-
  Quadratic Ledger Geometry (QLG) – Core Proof Framework
  No mathlib imports. Pure Lean 4 core.

  The routing algebra: balance equation, invariant preservation, proof gates.
-/

-- Vec3 for agent state vectors
abbrev Vec3 = Fin 3 → Int

-- Matrix3 for routing tensors and transformations
abbrev Matrix3 = Fin 3 → Fin 3 → Int

-- Dot product of two vectors
def dot (v w : Vec3) : Int :=
  (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)

-- Matrix-vector multiplication
def matVec (A : Matrix3) (x : Vec3) : Vec3 :=
  fun i =>
    (A i 0 * x 0 + A i 1 * x 1 + A i 2 * x 2)

-- Matrix transpose
def transpose (M : Matrix3) : Matrix3 :=
  fun i j => M j i

-- Matrix addition
def matAdd (A B : Matrix3) : Matrix3 :=
  fun i j => A i j + B i j

-- Scalar-matrix multiplication
def smul (c : Int) (M : Matrix3) : Matrix3 :=
  fun i j => c * M i j

-- Quadratic form: x^T Q x
def quadForm (Q : Matrix3) (x : Vec3) : Int :=
  dot x (matVec Q x)

-- Positive-semidefinite (for Q+)
def psd (M : Matrix3) : Prop :=
  ∀ v : Vec3, 0 ≤ dot v (matVec M v)

-- Negative-semidefinite (for Q-)
def nsd (M : Matrix3) : Prop :=
  ∀ v : Vec3, 0 ≤ dot v (matVec M v)

-- QLG specification
structure QLG where
  Q : Matrix3 -- symmetric routing tensor
  b : Vec3 -- linear term
  c : Int -- constant term
  K : Int -- balance invariant
  Qplus Qminus : Matrix3 -- factorization Q = Q+ - Q-
  h_psd : psd Qplus -- Q+ is PSD
  h_nsd : nsd Qminus -- Q- is NSD

-- Balance predicate: isBalanced
def isBalanced (L : QLG) (x : Vec3) : Prop :=
  (quadForm L.Q x + dot L.b x + L.c = 0) ∧ -- surface equation
  (quadForm L.Qplus x = quadForm L.Qminus x) ∧ -- invariant equation
  (quadForm L.Qplus x = L.K) -- invariant equals K

-- Concrete QLG instance: the unit sphere over integers
def unitSphereQLG : QLG :=
  { Q := fun i j => if i = j then 1 else 0 -- Q = I₃
    b := fun _ => 0 -- b = 0
    c := -1 -- constant = -1
    K := 1 -- invariant K = 1
    Qplus := fun i j => if i = j then 1 else 0 -- Q+ = I₃
    Qminus := fun i j => 0 -- Q- = 0
    h_psd := by
      intro v
      simp only [dot, matVec]
      nlinarith [sq_nonneg (v 0), sq_nonneg (v 1), sq_nonneg (v 2)]
    h_nsd := by
      intro v
      simp only [dot, matVec]
      ring_nf
  }

-- The concrete witness: x = ![1, 0, 0]
def unitWitness : Vec3 := ![1, 0, 0]

-- Theorem: the witness satisfies the QLG
theorem unitSphere_has_solution :
    isBalanced unitSphereQLG unitWitness := by
  constructor
  · -- Surface equation: 1 + 0 - 1 = 0
    simp [isBalanced, unitSphereQLG, unitWitness, quadForm, dot, matVec]
    norm_num
  constructor
  · -- Invariant equation: quadForm Q+ x = quadForm Q- x
    simp [unitSphereQLG, unitWitness, quadForm, dot, matVec]
    norm_num
  · -- Invariant equals K: quadForm Q+ x = 1
    simp [unitSphereQLG, unitWitness, quadForm, dot, matVec]
    norm_num