mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-11 11:20:33 +00:00
016369c3ce
- AdjugateMatrix.lean — 8x8 matrix adjugate, determinant, identity - ColdReviewer.lean — unified cold-review formula (Psi_inv, Psi_gap, Psi_Sidon) with dec_trivial proofs (no native_decide) - RollupEvent.lean — Oracle rollup verifier with Prop/Bool bridge, soundness theorem, byte serialization - lakefile.lean — register new modules under SilverSightRRC - nr_bracket_validation.py — resolve merge conflict (paths + inits) All native_decide calls replaced with dec_trivial per project policy.
115 lines
5.2 KiB
Text
115 lines
5.2 KiB
Text
/-
|
|
ColdReviewer.lean — Unified Cold Reviewer Formula
|
|
-/
|
|
|
|
import CoreFormalism.FixedPoint
|
|
import SilverSight.AdjugateMatrix
|
|
|
|
set_option linter.dupNamespace false
|
|
|
|
namespace SilverSight.ColdReviewer
|
|
|
|
open SilverSight.FixedPoint
|
|
open SilverSight.FixedPoint.Q16_16
|
|
open SilverSight.AdjugateMatrix
|
|
|
|
abbrev Matrix8 := SilverSight.AdjugateMatrix.Matrix8
|
|
|
|
/-- Safe entry access (matches AdjugateMatrix.getEntry). -/
|
|
@[inline]
|
|
def getEntry (m : Array (Array Q16_16)) (i j : Nat) : Q16_16 :=
|
|
(m.getD i #[]).getD j zero
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §1 Ψ_inv
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def maxAbsEntry (m : Matrix8) : Q16_16 :=
|
|
(List.range 8).foldl (fun accI i =>
|
|
(List.range 8).foldl (fun accJ j =>
|
|
let x := getEntry m i j
|
|
let ax := if x.toInt < 0 then neg x else x
|
|
if ax.toInt > accJ.toInt then ax else accJ
|
|
) accI
|
|
) zero
|
|
|
|
def psiInversion (M adjM : Matrix8) (detM : Q16_16) : Q16_16 :=
|
|
let product := matrixMultiply M adjM
|
|
let scaledI := Array.ofFn (n := 8) fun (i : Fin 8) =>
|
|
Array.ofFn (n := 8) fun (j : Fin 8) =>
|
|
if i.val = j.val then detM else zero
|
|
let residual := Array.ofFn (n := 8) fun (i : Fin 8) =>
|
|
Array.ofFn (n := 8) fun (j : Fin 8) =>
|
|
sub (getEntry product i.val j.val) (getEntry scaledI i.val j.val)
|
|
maxAbsEntry residual
|
|
|
|
theorem psiInversion_identity : psiInversion identity8 identity8 one = zero := by
|
|
dec_trivial
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §2 Ψ_gap
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def threshold_1_7 : Q16_16 := ofRawInt 9362
|
|
|
|
def psiSpectral (sigma : Q16_16) : Q16_16 :=
|
|
if sigma.toInt < (threshold_1_7).toInt then
|
|
let diff : Int := (threshold_1_7).toInt - sigma.toInt
|
|
ofRawInt (diff * diff)
|
|
else
|
|
zero
|
|
|
|
theorem psiSpectral_above (sigma : Q16_16) (h : sigma.toInt ≥ (threshold_1_7).toInt) :
|
|
psiSpectral sigma = zero := by
|
|
unfold psiSpectral
|
|
have : ¬ sigma.toInt < (threshold_1_7).toInt := by omega
|
|
simp [this]
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §3 Ψ_Sidon
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
/-- 8-element Sidon check via `dec_trivial`-friendly explicit pair enumeration.
|
|
Checks all 36 unordered pair sums are distinct using flat comparisons. -/
|
|
def isSidonSet8 (s : Array Nat) : Bool :=
|
|
if s.size ≠ 8 then false else
|
|
-- Build array of 36 sums
|
|
let sums : Array Nat := Id.run do
|
|
let mut arr : Array Nat := #[]
|
|
for a in [0:8] do
|
|
for b in [a:8] do
|
|
arr := arr.push (s.getD a 0 + s.getD b 0)
|
|
pure arr
|
|
-- Check uniqueness by comparing every (i,j) with i < j
|
|
(List.range sums.size).all (fun i =>
|
|
(List.range i).all (fun j =>
|
|
sums.getD i 0 ≠ sums.getD j 0))
|
|
|
|
def psiSidon (s : Array Nat) : Nat :=
|
|
if isSidonSet8 s then 0 else 1
|
|
|
|
theorem psiSidon_canonical : psiSidon ((#[0,1,3,7,12,20,30,44] : Array Nat)) = 0 := by
|
|
dec_trivial
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §4 Unified Cold Reviewer Operator
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def coldReviewScore
|
|
(M adjM : Matrix8) (detM sigma : Q16_16)
|
|
(strands : Array Nat)
|
|
(wInv wGap wSidon : Q16_16) : Q16_16 :=
|
|
add (mul wInv (psiInversion M adjM detM))
|
|
(add (mul wGap (psiSpectral sigma))
|
|
(mul wSidon (ofInt (psiSidon strands : Int))))
|
|
|
|
theorem canonical_scores_zero (h_gap : sigma.toInt ≥ (threshold_1_7).toInt) :
|
|
coldReviewScore identity8 identity8 one sigma ((#[0,1,3,7,12,20,30,44] : Array Nat)) one one one = zero := by
|
|
unfold coldReviewScore
|
|
have h_inv : psiInversion identity8 identity8 one = zero := psiInversion_identity
|
|
have h_gap' : psiSpectral sigma = zero := psiSpectral_above sigma h_gap
|
|
have h_sidon : psiSidon ((#[0,1,3,7,12,20,30,44] : Array Nat)) = 0 := psiSidon_canonical
|
|
simp [h_inv, h_gap', h_sidon, mul_zero, one_mul]
|
|
dec_trivial
|
|
|
|
end SilverSight.ColdReviewer
|