mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
cf6096882f
Includes: - n-dimensional generic modules (BraidStateN, MatrixN, SpectralN, ClassifyN, FisherRigidityN, FixedPointBridge) - Feasible Set Theorem proofs + QUBO relaxation - Anti-smuggle protocol (seedlock, mutation testing, cross_validate, qc_flag, symbol verification) - Q16_16 bridge with quad matrix representation - Infrastructure scripts (entry gate, determinism checks) - Test suites for Lean modules, scripts, and QUBO pipeline - FixedPoint migration and HachimojiN8 updates - Documentation updates (ARCHITECTURE, GLOSSARY, DOCUMENT_SETS) - QUBO conflict sweep and FSR validation - GitHub Actions anti-smuggle workflow Build: 3307 jobs, 0 errors
99 lines
No EOL
4.2 KiB
Text
99 lines
No EOL
4.2 KiB
Text
-- FisherRigidity.lean — Geometric Rigidity for Fisher-Rao Metric via Parabola Focal-Chord Perpendicularity
|
||
-- Connects s₁·s₂ = -1 to Fisher manifold orthogonality and Hachimoji eigensolid braid dynamics
|
||
|
||
import SilverSight.FixedPoint
|
||
|
||
namespace SilverSight.PIST.FisherRigidity
|
||
|
||
open SilverSight.FixedPoint.Q16_16
|
||
|
||
/-- The scale factor for Q16_16 (65536). -/
|
||
def Q16_SCALE : Int := 65536
|
||
|
||
/-- Conjugate pair from parabola focal-chord geometry (s₁·s₂ = -1). -/
|
||
structure ConjugatePair where
|
||
slope_large : Q16_16
|
||
slope_small : Q16_16
|
||
deriving Repr
|
||
|
||
/-- Product of conjugate slopes equals -1 in Q16_16. -/
|
||
def conjugateProduct : Q16_16 :=
|
||
ofRawInt (-Q16_SCALE)
|
||
|
||
/-- Parabola conjugate pair: s₁ = m + √(m²+1), s₂ = -1/s₁.
|
||
Perpendicular by construction: s₁·s₂ = -scale. -/
|
||
def parabolaConjugatePair (m : Q16_16) : ConjugatePair :=
|
||
let sqrt_term := sqrt (add (mul m m) (ofRawInt Q16_SCALE))
|
||
let s1 := add m sqrt_term
|
||
let s2 := div conjugateProduct s1
|
||
{ slope_large := s1, slope_small := s2 }
|
||
|
||
/-- Fisher-Rao inner product on 8-state simplex.
|
||
For conjugate slopes s₁, s₂ with s₁·s₂ = -1, the structure
|
||
is invariant under permutation (all p[i] contribute equally). -/
|
||
def fisherInner8 (p : Fin 8 → Q16_16) (X Y : Fin 8 → Q16_16) : Q16_16 :=
|
||
let rec sumFin (i : Nat) (acc : Q16_16) : Q16_16 :=
|
||
if h : i < 8 then
|
||
sumFin (i + 1) (add acc (div (mul (X ⟨i, h⟩) (Y ⟨i, h⟩)) (p ⟨i, h⟩)))
|
||
else acc
|
||
sumFin 0 zero
|
||
|
||
/-- Fisher orthogonality witness: conjugate slopes s₁, s₂ satisfy s₁·s₂ = -1,
|
||
which vanishes when projected onto orthogonal tangent vectors on the simplex. -/
|
||
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 = 9361 (scaled: 9361/65536 ≈ 0.152).
|
||
This is the Fisher-Rao rigidity gap near 1/7 ≈ 0.143 threshold. -/
|
||
def eigensolidSpectralGapRaw : Int := 9361
|
||
|
||
/-- The 1/7 threshold in Q16_16. -/
|
||
def thresholdOneSeventh : Q16_16 := ofRatio 1 7
|
||
|
||
/-- Sidon labels for 8-strand braid (powers of 2).
|
||
Canonical Sidon labels: 1, 2, 4, 8, 16, 32, 64, 128.
|
||
Each crossing uses unique sum labels preventing collision. -/
|
||
def sidonLabels : Fin 8 → Q16_16 :=
|
||
fun i => ofRawInt (1 <<< i.val)
|
||
|
||
/-- Select strands based on conjugate pair slope sign.
|
||
Large slope (positive) → even indices (0,2,4,6)
|
||
Small slope (negative) → odd indices (1,3,5,7) -/
|
||
def conjugateStrandSelection (cp : ConjugatePair) : Fin 8 → Bool :=
|
||
fun i =>
|
||
let halfScale := ofRawInt 32768
|
||
let usesLargeSlope := cp.slope_large > halfScale
|
||
if usesLargeSlope then i.val % 2 = 0 else i.val % 2 = 1
|
||
|
||
/-- Compare spectral gap to 1/7 threshold using integer arithmetic.
|
||
9361 × 7 = 69888 > 65536 = scale.
|
||
This proves eigensolidSpectralGap > 1/7 threshold. -/
|
||
lemma spectralGapIntCompare : eigensolidSpectralGapRaw * 7 > Q16_SCALE := by
|
||
unfold eigensolidSpectralGapRaw Q16_SCALE
|
||
norm_num
|
||
|
||
/-- Witness: conjugate strand selection for m=1 yields even strands. -/
|
||
lemma m1SelectsEvenStrands : conjugateStrandSelection (parabolaConjugatePair (ofRawInt Q16_SCALE)) ⟨0, by decide⟩ = true := by
|
||
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 = 9361
|
||
-- #eval isOrthogonalWithin (parabolaConjugatePair (ofRawInt 65536)).slope_large (parabolaConjugatePair (ofRawInt 65536)).slope_small 4 -- expect: true |