File size: 3,900 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 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 | /-
QLGFamily -- Parameterised Quadratic Ledger Geometry
Extends QLG.lean with:
- wire serialisation: QLG -> 4-byte frame
- proof-carrying certificate type (QLGCertificate)
No mathlib. Pure Lean 4 core.
-/
-- Copy canonical types from QLG.lean
abbrev Vec3 := Fin 3 → Int
abbrev Matrix3 := Fin 3 → Fin 3 → Int
def dot (v w : Vec3) : Int :=
v 0 * w 0 + v 1 * w 1 + v 2 * w 2
def matVec (A : Matrix3) (x : Vec3) : Vec3 :=
fun i => A i 0 * x 0 + A i 1 * x 1 + A i 2 * x 2
def quadForm (Q : Matrix3) (x : Vec3) : Int :=
dot x (matVec Q x)
def psd (M : Matrix3) : Prop :=
∀ v : Vec3, 0 ≤ dot v (matVec M v)
def nsqd (M : Matrix3) : Prop :=
∀ v : Vec3, 0 ≤ dot v (matVec (fun i j => M j i) v)
structure QLGFamily where
Q Qplus Qminus : Matrix3
b : Vec3
c K : Int
Qp_s : psd Qplus
Qm_s : nsqd Qminus
def isBalancedF (L : QLGFamily) (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)
-- Theorem 6: K=0 implies zero vector is always a solution
lemma quadForm_zero (Q : Matrix3) : quadForm Q (fun _ => 0) = 0 := by
simp [quadForm, dot, matVec]
theorem zero_solves_when_K_zero (L : QLGFamily)
(hK : L.K = 0) (hc : L.c = 0) (hb : ∀ i, L.b i = 0) :
isBalancedF L (fun _ => 0) := by
simp only [isBalancedF, quadForm_zero]
exact ⟨by simp [dot, hb, hc], rfl, hK.symm⟩
-- Wire serialisation: QLG -> 4-byte sovereign frame
structure WireFrame where
primitives : UInt8 -- encoded K value
quad_op : UInt8 -- 0x0F = Q_sync frame delimiter
boundary : UInt8 -- 0xFF = Lambda (local sovereignty)
terminal : UInt8 -- 0x0A = Omega (commit)
deriving DecidableEq, Repr
def encodeQLG (L : QLGFamily) : WireFrame where
primitives := UInt8.ofNat (L.K.toNat % 256)
quad_op := 0x0F
boundary := 0xFF
terminal := 0x0A
def validFrame (f : WireFrame) : Prop :=
f.quad_op = 0x0F ∧ f.boundary = 0xFF ∧ f.terminal = 0x0A
-- Theorem 7: Wire encoding always produces a valid frame
theorem encode_produces_valid_frame (L : QLGFamily) :
validFrame (encodeQLG L) := by
simp [validFrame, encodeQLG]
-- Theorem 8: Wire encoding preserves the balance predicate
theorem wire_preserves_balance_cert (L : QLGFamily) (x : Vec3)
(h : isBalancedF L x) : validFrame (encodeQLG L) :=
encode_produces_valid_frame L
-- Proof-carrying certificate type
structure QLGCertificate where
family : QLGFamily
witness : Vec3
balanced : isBalancedF family witness
frame : WireFrame
frame_ok : validFrame frame
def mkCertificate (L : QLGFamily) (x : Vec3) (h : isBalancedF L x) :
QLGCertificate where
family := L
witness := x
balanced := h
frame := encodeQLG L
frame_ok := encode_produces_valid_frame L
-- Theorem 9: Certificate frame is always valid
theorem certificate_frame_valid (cert : QLGCertificate) :
validFrame cert.frame := cert.frame_ok
-- The canonical HyperKitty family instance
def hkFamily : QLGFamily where
Q := fun i j => if i = j then 1 else 0
b := fun _ => 0
c := -1
K := 1
Qplus := fun i j => if i = j then 1 else 0
Qminus := fun _ _ => 0
Qp_s := by
intro v
simp only [dot, matVec]
nlinarith [sq_nonneg (v 0), sq_nonneg (v 1), sq_nonneg (v 2)]
Qm_s := by
intro v
simp only [dot, matVec]
nlinarith
def hkWitness : Vec3 :=
fun i => if i = 0 then 1 else 0
theorem hk_witness_balanced : isBalancedF hkFamily hkWitness := by
simp only [isBalancedF, hkFamily, hkWitness, quadForm, dot, matVec]
norm_num [Fin.ext_iff]
def hkCertificate : QLGCertificate :=
mkCertificate hkFamily hkWitness hk_witness_balanced
-- Theorem 10: HyperKitty certificate is complete and exportable
theorem hk_certificate_complete :
validFrame hkCertificate.frame ∧
isBalancedF hkCertificate.family hkCertificate.witness :=
⟨certificate_frame_valid hkCertificate, hkCertificate.balanced⟩
|