mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
ed08c7ff32
Connects s₁·s₂ = -1 perpendicularity to: - FisherTangent and fisherInner structures - ConjugatePair with slope_large/slope_small - eigensolidSpectralGap (9984 Q16_16 ≈ 0.152) - thresholdOneSeventh (1/7) Also fixes CoreFormalism/FixedPoint.lean import syntax. Build: 3328 jobs, 0 errors (lake build SilverSightRRC)
9 lines
No EOL
349 B
Text
9 lines
No EOL
349 B
Text
-- CoreFormalism.FixedPoint - re-export for backward compatibility
|
|
import SilverSight.FixedPoint
|
|
|
|
namespace CoreFormalism.FixedPoint
|
|
-- Type aliases for backward compatibility
|
|
abbrev Q16_16 := SilverSight.FixedPoint.Q16_16
|
|
abbrev Q0_16 := SilverSight.FixedPoint.Q0_16
|
|
abbrev Q0_64 := SilverSight.FixedPoint.Q0_64
|
|
end CoreFormalism.FixedPoint |