|
|
ed08c7ff32
|
feat(lean): Add FisherRigidity bridge for parabola focal-chord to Fisher-Rao
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)
|
2026-06-24 10:24:54 -05:00 |
|
|
|
f7858914b7
|
docs: fix documentation gaps + add pure math description
Fixed 5 undocumented Lean files:
- PVGS_DQ_Bridge/section5_quantum_sensing.lean — quantum sensing docs
- PVGS_DQ_Bridge/section2_hermite_sieve.lean — Hermite polynomial docs
- SilverSight/RRC/ReceiptDensity.lean — receipt density scoring docs
- SilverSight/PIST/SpectralWitness.lean — spectral witness docs
- CoreFormalism/FixedPoint.lean — stub redirect docs
Added docs/PURE_MATH_DESCRIPTION.md:
- Pure mathematical description of each module (no code)
- Why each module exists (problem/insight)
- What a graph calculator would need to implement each
- 10 modules covered: SidonSets, BraidEigensolid, BraidSpherionBridge,
HachimojiLUT, ChentsovFinite, DynamicCanal, Schema, WireFormat,
Receipt, Bind
|
2026-06-23 05:21:58 -05:00 |
|
|
|
1a26de076d
|
fix(lean): address vacuous rfl proofs in Chentsov theorem and close Hermite sieve proofs
- ChentsovFinite.lean: Replaced vacuous rfl proofs at uniform distribution permutation invariance, diagonal case, and off-diagonal case with explicit proof obligations and sorry.
- section2_hermite_sieve.lean: Proved repunit strict monotonicity and lower bound lemmas, closing relevant sorry placeholders.
- BindingSiteEntropy.lean: Swapped geodesicDistance placeholder with fisherRaoApprox and added counterexample sketch for fisher_implies_similar_druggability.
- FixedPoint.lean, lakefile.lean, gemma4_mcp.py: Minor fixes and enhancements.
- AGENTS.md: Tracked open Chentsov proof obligations.
Build: 2987 jobs, 0 errors (lake build)
|
2026-06-23 05:11:04 -05:00 |
|
|
|
4490dc28a7
|
feat(rrc): bare-minimum RRC refactor into SilverSight
- Move canonical FixedPoint to Core/SilverSight/FixedPoint.lean
- Add SilverSightRRC library: RRC logogram gates, receipt bridge, AVM ISA
- Add AVMIsa.Emit as the sole top-level JSON output boundary
- Add rrc-emit-fixture executable and Python I/O shims
- Update AGENTS.md, glossary, project map, and build baseline
Build: 2981 jobs, 0 errors (lake build)
|
2026-06-21 09:08:48 -05:00 |
|
|
|
7a973a06f6
|
feat(core): harden SilverSightCore and port canonical FixedPoint
- Remove Float from Core/SilverSightCore.lean (Receipt.pathCost is now Option Nat)
- Prove TIC theorems tic_never_decreases and computation_generates_time
- Add lakefile.lean, lean-toolchain, and .gitignore for .lake/
- Port Research-Stack Semantics.FixedPoint.lean to formal/CoreFormalism/FixedPoint.lean
- Delete thin Q16_16_Spec.lean; update Python/QUBO comments and docs
- Create AGENTS.md distilled from Research Stack core bindings
- Update REBASE_RULES.md to strip legacy hacks and reference AGENTS.md
Build: 2978 jobs, 0 errors (lake build)
|
2026-06-21 06:30:12 -05:00 |
|
