File size: 2,946 Bytes
224e773 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 | /-
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
|