allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-08-20 19:07:29 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lean): rewrite tdoku solver convergence proof to use List and rfl, avoiding native_decide

Browse source 
- Transitioned State16D and numerical operations from Array to List representation.
- Implemented custom definitionally-reducible List.get? helper to support transparent index lookups.
- Set maxRecDepth to 1000000 to accommodate unfolding of 20 fixed-point iterations.
- Replaced native_decide with pure kernel rfl for erdos_336_order and erdos_336_exact_order theorems.

Build: 3307 jobs, 0 errors (lake build)
This commit is contained in:
allaun 2026-06-28 23:45:13 -05:00
parent a678c21472
commit 86fa38a529
1 changed files with 62 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

109
formal/SilverSight/PIST/Tdoku16D.lean
View file

@ -1,25 +1,45 @@
-- Tdoku16D.lean — 16D tdoku Constraint Propagation and Order Decoders -- Tdoku16D.lean — 16D tdoku Constraint Propagation and Order Decoders (List-based)
-- --
-- Formalizes the 16D tdoku constraint propagation solver and decoders for Erdős #336. -- Formalizes the 16D tdoku constraint propagation solver and decoders for Erdős #336
-- Uses compile-time evaluation (reflexivity proofs) to verify convergence and correctness. -- using definitionally reducible List operations. This avoids native_decide.
import SilverSight.FixedPoint import SilverSight.FixedPoint
import Mathlib.Tactic import Mathlib.Tactic
set_option maxRecDepth 1000000
namespace SilverSight.PIST.Tdoku16D namespace SilverSight.PIST.Tdoku16D
open SilverSight.FixedPoint open SilverSight.FixedPoint
open SilverSight.FixedPoint.Q16_16 open SilverSight.FixedPoint.Q16_16
-- ============================================================ -- ============================================================
-- §1 STATE REPRESENTATION -- §1 STATE REPRESENTATION & LIST HELPERS
-- ============================================================ -- ============================================================
structure State16D where structure State16D where
L1 : Array Q16_16 L1 : List Q16_16
L2 : Array Q16_16 L2 : List Q16_16
deriving Repr, DecidableEq deriving Repr, DecidableEq
/-- Custom definitionally-reducible index lookup for List. -/
def get? {α : Type} : List α → Nat → Option α
| [], _ => none
| x :: _, 0 => some x
| _ :: xs, n + 1 => get? xs n
/-- Safely get element from list with default value. -/
def getD (l : List Q16_16) (i : Nat) (default : Q16_16) : Q16_16 :=
match get? l i with
| some x => x
| none => default
/-- Safely get element from List Int with default value. -/
def getDInt (l : List Int) (i : Nat) (default : Int) : Int :=
match get? l i with
| some x => x
| none => default
-- ============================================================ -- ============================================================
-- §2 CONSTRAINT MATRIX & TARGETS -- §2 CONSTRAINT MATRIX & TARGETS
-- ============================================================ -- ============================================================
@ -63,26 +83,26 @@ def getTarget (i : Nat) : Q16_16 :=
-- ============================================================ -- ============================================================
/-- Compute constraint violations C v - target. -/ /-- Compute constraint violations C v - target. -/
def computeViolations (v : Array Q16_16) : Array Q16_16 := def computeViolations (v : List Q16_16) : List Q16_16 :=
Array.ofFn (n := 27) fun i => List.ofFn (n := 27) fun i =>
let cv := (List.range 16).foldl (fun acc j => add acc (mul (getC i.val j) (v.getD j zero))) zero let cv := (List.range 16).foldl (fun acc j => add acc (mul (getC i.val j) (getD v j zero))) zero
sub cv (getTarget i.val) sub cv (getTarget i.val)
/-- Compute correction C^T violations. -/ /-- Compute correction C^T violations. -/
def computeCorrection (violations : Array Q16_16) : Array Q16_16 := def computeCorrection (violations : List Q16_16) : List Q16_16 :=
Array.ofFn (n := 16) fun j => List.ofFn (n := 16) fun j =>
(List.range 27).foldl (fun acc i => add acc (mul (getC i j.val) (violations.getD i zero))) zero (List.range 27).foldl (fun acc i => add acc (mul (getC i j.val) (getD violations i zero))) zero
/-- Update state vector: new_v = v - lr * correction. -/ /-- Update state vector: new_v = v - lr * correction. -/
def updateVector (v : Array Q16_16) (correction : Array Q16_16) : Array Q16_16 := def updateVector (v : List Q16_16) (correction : List Q16_16) : List Q16_16 :=
Array.ofFn (n := 16) fun j => List.ofFn (n := 16) fun j =>
let corr := mul (ofRawInt 3277) (correction.getD j.val zero) -- lr = 0.05 (3277) let corr := mul (ofRawInt 3277) (getD correction j.val zero) -- lr = 0.05 (3277)
sub (v.getD j.val zero) corr sub (getD v j.val zero) corr
/-- Retract 16D vector back onto simplices L1 and L2. -/ /-- Retract 16D vector back onto simplices L1 and L2. -/
def retractToSimplex (v : Array Q16_16) : Array Q16_16 := def retractToSimplex (v : List Q16_16) : List Q16_16 :=
let L1 := Array.ofFn (n := 8) fun i => v.getD i.val zero let L1 := List.ofFn (n := 8) fun i => getD v i.val zero
let L2 := Array.ofFn (n := 8) fun i => v.getD (8 + i.val) zero let L2 := List.ofFn (n := 8) fun i => getD v (8 + i.val) zero
let L1_pos := L1.map (fun x => if x.toInt < 0 then zero else x) let L1_pos := L1.map (fun x => if x.toInt < 0 then zero else x)
let L2_pos := L2.map (fun x => if x.toInt < 0 then zero else x) let L2_pos := L2.map (fun x => if x.toInt < 0 then zero else x)
@ -92,27 +112,27 @@ def retractToSimplex (v : Array Q16_16) : Array Q16_16 :=
let L1_retracted := let L1_retracted :=
if sumL1.toInt = 0 then if sumL1.toInt = 0 then
Array.replicate 8 zero List.replicate 8 zero
else else
L1_pos.map (fun x => div x sumL1) L1_pos.map (fun x => div x sumL1)
let L2_retracted := let L2_retracted :=
if sumL2.toInt = 0 then if sumL2.toInt = 0 then
Array.replicate 8 zero List.replicate 8 zero
else else
L2_pos.map (fun x => div x sumL2) L2_pos.map (fun x => div x sumL2)
L1_retracted ++ L2_retracted L1_retracted ++ L2_retracted
/-- One solver step. -/ /-- One solver step. -/
def stepTdoku (v : Array Q16_16) : Array Q16_16 := def stepTdoku (v : List Q16_16) : List Q16_16 :=
let violations := computeViolations v let violations := computeViolations v
let correction := computeCorrection violations let correction := computeCorrection violations
let updated := updateVector v correction let updated := updateVector v correction
retractToSimplex updated retractToSimplex updated
/-- Solver loop over Nat fuel. -/ /-- Solver loop over Nat fuel. -/
def cycleTdoku (v : Array Q16_16) (fuel : Nat) : Array Q16_16 := def cycleTdoku (v : List Q16_16) (fuel : Nat) : List Q16_16 :=
match fuel with match fuel with
| 0 => v | 0 => v
| f + 1 => cycleTdoku (stepTdoku v) f | f + 1 => cycleTdoku (stepTdoku v) f
@ -122,20 +142,20 @@ def cycleTdoku (v : Array Q16_16) (fuel : Nat) : Array Q16_16 :=
-- ============================================================ -- ============================================================
/-- Sum of squares proxy for L1 entropy. -/ /-- Sum of squares proxy for L1 entropy. -/
def sumSquares (L : Array Q16_16) : Q16_16 := def sumSquares (L : List Q16_16) : Q16_16 :=
L.foldl (fun acc x => add acc (mul x x)) zero L.foldl (fun acc x => add acc (mul x x)) zero
/-- Extract order based on L1 sum of squares. -/ /-- Extract order based on L1 sum of squares. -/
def extractOrder (L1 : Array Q16_16) : Nat := def extractOrder (L1 : List Q16_16) : Nat :=
let ss := sumSquares L1 let ss := sumSquares L1
if ss.toInt < 16384 then 2 -- ss < 0.25 (16384) if ss.toInt < 16384 then 2 -- ss < 0.25 (16384)
else if ss.toInt < 32768 then 3 else if ss.toInt < 32768 then 3
else 4 else 4
/-- Vector differences. -/ /-- Vector differences. -/
def getDiff (L : Array Q16_16) : Array Int := def getDiff (L : List Q16_16) : List Int :=
Array.ofFn (n := 7) fun i => List.ofFn (n := 7) fun i =>
(L.getD (i.val + 1) zero).toInt - (L.getD i.val zero).toInt (getD L (i.val + 1) zero).toInt - (getD L i.val zero).toInt
/-- Sign of an integer. -/ /-- Sign of an integer. -/
def getSign (x : Int) : Int := def getSign (x : Int) : Int :=
@ -144,17 +164,17 @@ def getSign (x : Int) : Int :=
else 0 else 0
/-- Count sign changes in differences. -/ /-- Count sign changes in differences. -/
def countSignChanges (L : Array Q16_16) : Nat := def countSignChanges (L : List Q16_16) : Nat :=
let diffs := getDiff L let diffs := getDiff L
let signs := diffs.map getSign let signs := diffs.map getSign
(List.range 6).foldl (fun acc i => (List.range 6).foldl (fun acc i =>
let s1 := signs.getD i 0 let s1 := getDInt signs i 0
let s2 := signs.getD (i + 1) 0 let s2 := getDInt signs (i + 1) 0
acc + if s1 ≠ 0 ∧ s2 ≠ 0 ∧ s1 ≠ s2 then 1 else 0 acc + if s1 ≠ 0 ∧ s2 ≠ 0 ∧ s1 ≠ s2 then 1 else 0
) 0 ) 0
/-- Extract exact order based on sign changes of L2. -/ /-- Extract exact order based on sign changes of L2. -/
def extractExactOrder (L2 : Array Q16_16) : Nat := def extractExactOrder (L2 : List Q16_16) : Nat :=
let sc := countSignChanges L2 let sc := countSignChanges L2
if sc ≥ 3 then 3 if sc ≥ 3 then 3
else if sc ≥ 1 then 2 else if sc ≥ 1 then 2
@ -165,30 +185,25 @@ def extractExactOrder (L2 : Array Q16_16) : Nat :=
-- ============================================================ -- ============================================================
/-- Initial L1 state for Erdős #336 basis (GAAAACCA). -/ /-- Initial L1 state for Erdős #336 basis (GAAAACCA). -/
def initialL1 : Array Q16_16 := def initialL1 : List Q16_16 :=
#[ofRawInt 28087, zero, zero, zero, zero, ofRawInt 18724, ofRawInt 18724, zero] [ofRawInt 28087, zero, zero, zero, zero, ofRawInt 18724, ofRawInt 18724, zero]
/-- Initial L2 state for Erdős #336 basis (AAAAAAAAAAAAAAAA). -/ /-- Initial L2 state for Erdős #336 basis (AAAAAAAAAAAAAAAA). -/
def initialL2 : Array Q16_16 := def initialL2 : List Q16_16 :=
#[zero, zero, zero, zero, zero, zero, zero, zero] [zero, zero, zero, zero, zero, zero, zero, zero]
/-- Initial full 16D state. -/ /-- Initial full 16D state. -/
def initialV : Array Q16_16 := initialL1 ++ initialL2 def initialV : List Q16_16 := initialL1 ++ initialL2
-- Theorems closed by reflexivity (reflexive decision loop)
-- Theorems closed by native_decide (reflexive decision loop).
-- We use native_decide because Array primitives (ofFn, getD, foldl) are native
-- FFI functions that are opaque to the kernel's term reducer, making VM-based
-- native_decide the only tactic that can reduce and close these arithmetic goals.
-- Theorems closed by decide or rfl (pure kernel reduction)
theorem erdos_336_order : theorem erdos_336_order :
let v_final := cycleTdoku initialV 20 let v_final := cycleTdoku initialV 20
let L1_final := Array.ofFn (n := 8) fun i => v_final.getD i.val zero let L1_final := List.ofFn (n := 8) fun i => getD v_final i.val zero
extractOrder L1_final = 2 := by native_decide extractOrder L1_final = 2 := by rfl
theorem erdos_336_exact_order : theorem erdos_336_exact_order :
let v_final := cycleTdoku initialV 20 let v_final := cycleTdoku initialV 20
let L2_final := Array.ofFn (n := 8) fun i => v_final.getD (8 + i.val) zero let L2_final := List.ofFn (n := 8) fun i => getD v_final (8 + i.val) zero
extractExactOrder L2_final = 3 := by native_decide extractExactOrder L2_final = 3 := by rfl
end SilverSight.PIST.Tdoku16D end SilverSight.PIST.Tdoku16D