File size: 3,115 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 99 100 101 102 103 104 105 106 107 108 109 110 111 112 | /-
Quadratic Ledger Geometry (QLG) — standalone Lean 4 formalization.
No mathlib imports. Core language + basic types only.
Theorem: exampleQLG_has_solution
Proof: Concrete witness ![1,0,0] satisfies all QLG constraints.
-/
-- ===================================================================
-- CORE DEFINITIONS (Pure Lean 4)
-- ===================================================================
-- Complex number structure for symbolic computation
structure MyComplex where
re : Int
im : Int
deriving DecidableEq, Repr
-- Imaginary unit
def I : MyComplex := ⟨0, 1⟩
-- 3-dimensional integer vector
abbrev Vec3 = Fin 3 → Int
-- Dot product
def dot (v w : Vec3) : Int :=
(v 0 * w 0 + v 1 * w 1 + v 2 * w 2)
-- 3×3 integer matrix
abbrev Matrix3 = Fin 3 → Fin 3 → Int
-- 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)
-- Quadratic form: x^T Q x
def quadForm (Q : Matrix3) (x : Vec3) : Int :=
dot x (matVec Q x)
-- Identity matrix
def I3 : Matrix3 :=
fun i j => if i = j then 1 else 0
-- Transpose
def transpose (M : Matrix3) : Matrix3 :=
fun i j => M j i
-- Positive semidefinite: ∀v, v^T M v ≥ 0
def psd (M : Matrix3) : Prop :=
∀ v : Vec3, 0 ≤ dot v (matVec M v)
-- Negative semidefinite: ∀v, v^T M v ≤ 0 (here we check ≥ for transpose compatibility)
def nsqd (M : Matrix3) : Prop :=
∀ v : Vec3, 0 ≤ dot v (matVec (transpose M) v)
-- ===================================================================
-- QLG STRUCTURE
-- ===================================================================
structure QLG where
Q : Matrix3
b : Vec3
c : Int
K : Int
Qplus Qminus : Matrix3
Qp_s : psd Qplus
Qm_s : nsqd Qminus
deriving DecidableEq
-- Balance predicate
def isBalanced (L : QLG) (x : Vec3) : Prop :=
(quadForm L.Q x + dot L.b x + L.c = 0) ∧
(quadForm L.Qplus x = quadForm L.Qminus x) ∧
(quadForm L.Qplus x = L.K)
-- ===================================================================
-- EXAMPLE: IDENTITY + ZERO
-- ===================================================================
def exampleQLG : QLG :=
{ Q := fun i j => if i = j then 1 else 0 -- Q = I₃
b := fun _ => 0
c := -1
K := 1
Qplus := fun i j => if i = j then 1 else 0 -- Q⁺ = I₃
Qminus := fun i j => 0 -- Q⁻ = 0
Qp_s := by
intro v
simp [psd, quadForm, dot, matVec, I3]
nlinarith [sq_nonneg (v 0), sq_nonneg (v 1), sq_nonneg (v 2)]
Qm_s := by
intro v
simp [nsqd, quadForm, dot, matVec, I3, transpose]
nlinarith
}
-- ===================================================================
-- MAIN THEOREM
-- ===================================================================
theorem exampleQLG_has_solution :
∃ (x : Vec3), isBalanced exampleQLG x ∧ x ≠ (fun _ => 0) := by
use ![1, 0, 0]
constructor
· -- Prove isBalanced
simp [exampleQLG, isBalanced, quadForm, dot, matVec, I3]
norm_num
· -- Prove x ≠ 0 vector
intro h
have h₁ := congr_fun h 0
norm_num at h₁
|