From 523abdd4222112c8b1233af1bdaecebace65419f Mon Sep 17 00:00:00 2001 From: allaun Date: Sat, 27 Jun 2026 23:14:34 -0500 Subject: [PATCH] refactor(lean): add tolerance-based precision check secondary lemma to FisherRigidity 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) --- formal/SilverSight/PIST/FisherRigidity.lean | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/formal/SilverSight/PIST/FisherRigidity.lean b/formal/SilverSight/PIST/FisherRigidity.lean index d14cdef0..0e039950 100644 --- a/formal/SilverSight/PIST/FisherRigidity.lean +++ b/formal/SilverSight/PIST/FisherRigidity.lean @@ -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 := 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. eigensolidSpectralGapRaw = 9984 (scaled: 9984/65536 ≈ 0.152). 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 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 -- #eval Witnesses (run via `lake build` output): -- parabolaConjugatePair (ofRawInt 65536) → { slope_large := 158217, slope_small := -27147 } --- eigensolidSpectralGapRaw = 9984 \ No newline at end of file +-- eigensolidSpectralGapRaw = 9984 +-- #eval isOrthogonalWithin (parabolaConjugatePair (ofRawInt 65536)).slope_large (parabolaConjugatePair (ofRawInt 65536)).slope_small 4 -- expect: true \ No newline at end of file