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

refactor(lean): add tolerance-based precision check secondary lemma to FisherRigidity

Browse source 
Implemented isOrthogonalWithin and m1_orthogonal_within_4 lemma to verify
fixed-point conjugate slopes orthogonality within a 4 LSB tolerance bound.
This filters out the Euclidean division quantization precision gap.

Build: 3307 jobs, 0 errors (lake build)
This commit is contained in:
allaun 2026-06-27 23:14:34 -05:00
parent 1eb7a0d924
commit 523abdd422
1 changed files with 15 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
formal/SilverSight/PIST/FisherRigidity.lean
View file

@ -43,6 +43,12 @@ def fisherInner8 (p : Fin 8 → Q16_16) (X Y : Fin 8 → Q16_16) : Q16_16 :=
def isOrthogonal (s1 s2 : Q16_16) : Bool := def isOrthogonal (s1 s2 : Q16_16) : Bool :=
mul s1 s2 == ofRawInt (-Q16_SCALE) mul s1 s2 == ofRawInt (-Q16_SCALE)
/-- Orthogonality within a given tolerance ε (in raw LSB units). -/
def isOrthogonalWithin (s1 s2 : Q16_16) (tol : Nat) : Bool :=
let prod_raw := (mul s1 s2).val
let target_raw := -Q16_SCALE
decide (Int.natAbs (prod_raw - target_raw) ≤ tol)
/-- Spectral gap raw integer value. /-- Spectral gap raw integer value.
eigensolidSpectralGapRaw = 9984 (scaled: 9984/65536 ≈ 0.152). eigensolidSpectralGapRaw = 9984 (scaled: 9984/65536 ≈ 0.152).
This is the Fisher-Rao rigidity gap near 1/7 ≈ 0.143 threshold. -/ This is the Fisher-Rao rigidity gap near 1/7 ≈ 0.143 threshold. -/
@ -78,8 +84,16 @@ lemma m1SelectsEvenStrands : conjugateStrandSelection (parabolaConjugatePair (of
unfold conjugateStrandSelection parabolaConjugatePair conjugateProduct Q16_SCALE ofRawInt unfold conjugateStrandSelection parabolaConjugatePair conjugateProduct Q16_SCALE ofRawInt
decide decide
/-- Lemma: For m = 1, the parabola conjugate pair is orthogonal within 4 LSB. -/
lemma m1_orthogonal_within_4 :
let cp := parabolaConjugatePair (ofRawInt Q16_SCALE)
isOrthogonalWithin cp.slope_large cp.slope_small 4 = true := by
unfold parabolaConjugatePair isOrthogonalWithin conjugateProduct Q16_SCALE ofRawInt
decide
end SilverSight.PIST.FisherRigidity end SilverSight.PIST.FisherRigidity
-- #eval Witnesses (run via `lake build` output): -- #eval Witnesses (run via `lake build` output):
-- parabolaConjugatePair (ofRawInt 65536) → { slope_large := 158217, slope_small := -27147 } -- parabolaConjugatePair (ofRawInt 65536) → { slope_large := 158217, slope_small := -27147 }
-- eigensolidSpectralGapRaw = 9984 -- eigensolidSpectralGapRaw = 9984
-- #eval isOrthogonalWithin (parabolaConjugatePair (ofRawInt 65536)).slope_large (parabolaConjugatePair (ofRawInt 65536)).slope_small 4 -- expect: true