From 86fa38a529629396a76d0c76f68b5d894441cb15 Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 28 Jun 2026 23:45:13 -0500 Subject: [PATCH] fix(lean): rewrite tdoku solver convergence proof to use List and rfl, avoiding native_decide - 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) --- formal/SilverSight/PIST/Tdoku16D.lean | 109 +++++++++++++++----------- 1 file changed, 62 insertions(+), 47 deletions(-) diff --git a/formal/SilverSight/PIST/Tdoku16D.lean b/formal/SilverSight/PIST/Tdoku16D.lean index 32350c55..ae9baad5 100644 --- a/formal/SilverSight/PIST/Tdoku16D.lean +++ b/formal/SilverSight/PIST/Tdoku16D.lean @@ -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. --- Uses compile-time evaluation (reflexivity proofs) to verify convergence and correctness. +-- Formalizes the 16D tdoku constraint propagation solver and decoders for Erdős #336 +-- using definitionally reducible List operations. This avoids native_decide. import SilverSight.FixedPoint import Mathlib.Tactic +set_option maxRecDepth 1000000 + namespace SilverSight.PIST.Tdoku16D open SilverSight.FixedPoint open SilverSight.FixedPoint.Q16_16 -- ============================================================ --- §1 STATE REPRESENTATION +-- §1 STATE REPRESENTATION & LIST HELPERS -- ============================================================ structure State16D where - L1 : Array Q16_16 - L2 : Array Q16_16 + L1 : List Q16_16 + L2 : List Q16_16 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 -- ============================================================ @@ -63,26 +83,26 @@ def getTarget (i : Nat) : Q16_16 := -- ============================================================ /-- Compute constraint violations C v - target. -/ -def computeViolations (v : Array Q16_16) : Array Q16_16 := - Array.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 +def computeViolations (v : List Q16_16) : List Q16_16 := + List.ofFn (n := 27) fun i => + 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) /-- Compute correction C^T violations. -/ -def computeCorrection (violations : Array Q16_16) : Array Q16_16 := - Array.ofFn (n := 16) fun j => - (List.range 27).foldl (fun acc i => add acc (mul (getC i j.val) (violations.getD i zero))) zero +def computeCorrection (violations : List Q16_16) : List Q16_16 := + List.ofFn (n := 16) fun j => + (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. -/ -def updateVector (v : Array Q16_16) (correction : Array Q16_16) : Array Q16_16 := - Array.ofFn (n := 16) fun j => - let corr := mul (ofRawInt 3277) (correction.getD j.val zero) -- lr = 0.05 (3277) - sub (v.getD j.val zero) corr +def updateVector (v : List Q16_16) (correction : List Q16_16) : List Q16_16 := + List.ofFn (n := 16) fun j => + let corr := mul (ofRawInt 3277) (getD correction j.val zero) -- lr = 0.05 (3277) + sub (getD v j.val zero) corr /-- Retract 16D vector back onto simplices L1 and L2. -/ -def retractToSimplex (v : Array Q16_16) : Array Q16_16 := - let L1 := Array.ofFn (n := 8) fun i => v.getD i.val zero - let L2 := Array.ofFn (n := 8) fun i => v.getD (8 + i.val) zero +def retractToSimplex (v : List Q16_16) : List Q16_16 := + let L1 := List.ofFn (n := 8) fun i => getD v 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 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 := if sumL1.toInt = 0 then - Array.replicate 8 zero + List.replicate 8 zero else L1_pos.map (fun x => div x sumL1) let L2_retracted := if sumL2.toInt = 0 then - Array.replicate 8 zero + List.replicate 8 zero else L2_pos.map (fun x => div x sumL2) L1_retracted ++ L2_retracted /-- 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 correction := computeCorrection violations let updated := updateVector v correction retractToSimplex updated /-- 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 | 0 => v | 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. -/ -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 /-- 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 if ss.toInt < 16384 then 2 -- ss < 0.25 (16384) else if ss.toInt < 32768 then 3 else 4 /-- Vector differences. -/ -def getDiff (L : Array Q16_16) : Array Int := - Array.ofFn (n := 7) fun i => - (L.getD (i.val + 1) zero).toInt - (L.getD i.val zero).toInt +def getDiff (L : List Q16_16) : List Int := + List.ofFn (n := 7) fun i => + (getD L (i.val + 1) zero).toInt - (getD L i.val zero).toInt /-- Sign of an integer. -/ def getSign (x : Int) : Int := @@ -144,17 +164,17 @@ def getSign (x : Int) : Int := else 0 /-- Count sign changes in differences. -/ -def countSignChanges (L : Array Q16_16) : Nat := +def countSignChanges (L : List Q16_16) : Nat := let diffs := getDiff L let signs := diffs.map getSign (List.range 6).foldl (fun acc i => - let s1 := signs.getD i 0 - let s2 := signs.getD (i + 1) 0 + let s1 := getDInt signs i 0 + let s2 := getDInt signs (i + 1) 0 acc + if s1 ≠ 0 ∧ s2 ≠ 0 ∧ s1 ≠ s2 then 1 else 0 ) 0 /-- 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 if sc ≥ 3 then 3 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). -/ -def initialL1 : Array Q16_16 := - #[ofRawInt 28087, zero, zero, zero, zero, ofRawInt 18724, ofRawInt 18724, zero] +def initialL1 : List Q16_16 := + [ofRawInt 28087, zero, zero, zero, zero, ofRawInt 18724, ofRawInt 18724, zero] /-- Initial L2 state for Erdős #336 basis (AAAAAAAAAAAAAAAA). -/ -def initialL2 : Array Q16_16 := - #[zero, zero, zero, zero, zero, zero, zero, zero] +def initialL2 : List Q16_16 := + [zero, zero, zero, zero, zero, zero, zero, zero] /-- Initial full 16D state. -/ -def initialV : Array 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. +def initialV : List Q16_16 := initialL1 ++ initialL2 +-- Theorems closed by decide or rfl (pure kernel reduction) theorem erdos_336_order : let v_final := cycleTdoku initialV 20 - let L1_final := Array.ofFn (n := 8) fun i => v_final.getD i.val zero - extractOrder L1_final = 2 := by native_decide + let L1_final := List.ofFn (n := 8) fun i => getD v_final i.val zero + extractOrder L1_final = 2 := by rfl theorem erdos_336_exact_order : let v_final := cycleTdoku initialV 20 - let L2_final := Array.ofFn (n := 8) fun i => v_final.getD (8 + i.val) zero - extractExactOrder L2_final = 3 := by native_decide + let L2_final := List.ofFn (n := 8) fun i => getD v_final (8 + i.val) zero + extractExactOrder L2_final = 3 := by rfl end SilverSight.PIST.Tdoku16D