19492eb9b8
fix: add orphaned files to lakefile + document remaining sorry
...
Added to SilverSightRRC lakefile:
- SilverSight.PIST.SpectralWitness (49 lines, 0 sorries)
- SilverSight.ProductSchema (48 lines, 0 sorries)
- SilverSight.ProductWireFormat (67 lines, 0 sorries)
- RRCLib.RRCEmit (435 lines, 0 sorries)
Documented section4_rrc_kernel.lean sorry:
- Requires Matveev's theorem + LLL formalization
- Formula-first: verified by adversarial review
Remaining: PVGS_DQ_Bridge Q16_16 unification (5 duplicates)
and 8 PVGS_DQ_Bridge files not in lakefile (research scaffolding).
Build: 3307 jobs, 0 errors.
2026-06-23 06:11:54 -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
c42aa0de23
docs(silversight): document λ(p) bosonic estimator results
...
Add BMCTE, ContinuousInterpolation, EntropyInvarianceHypothesis terms to GLOSSARY.
Document bosonic_continuous experiment showing smooth estimator family without regime boundary.
See ChatGPT analysis: λ(p)=exp(-p²/N) eliminates p≥5 distinguishability cutoff.
Build: 2987 jobs, 0 errors
2026-06-22 01:33:59 -05:00
3504bca392
feat(lean): add SilverSight Semantics core modules (Schema, Layout, WireFormat, View, LayoutBridge, CanalLayout)
...
Implements the YaFF-inspired separation of schema, layout, and access pattern
in Core/SilverSight/Semantics/:
- Schema.lean: fixed-size Schema typeclass with byteSize and wellFormed.
- Layout.lean: Layout enum, AccessProfile cost model, and cost-based selector
with an ε-suboptimality theorem.
- WireFormat.lean: certified encode/decode/roundTrip/encode_size structure.
- View.lean: zero-copy View with address-arithmetic invariant.
- LayoutBridge.lean: certified layout-conversion structure and identity bridges.
- CanalLayout.lean: CanalRegime enum and regime-aware layout selection.
Also updates:
- lakefile.lean: adds SilverSight.Semantics.* roots to SilverSightCore.
- docs/ARCHITECTURE.md, RRC_REFACTOR_READINESS.md, PROJECT_MAP.{md,json},
build_logs/2026-06-21_session_build_baseline.md, and GLOSSARY.md.
- AGENTS.md: build baseline, blessed surfaces, and pending proof work.
Build: 2987 jobs, 0 errors (lake build)
Tests: Python 21/21, Lean/C 35/35
2026-06-21 14:00:56 -05:00
fec200205e
feat(rrc): port ReceiptDensity, PolyFactorIdentity, EntropyCandidates and add Q16_16 roundtrip test
...
Ports three Research Stack RRC gates into formal/SilverSight/RRC/ using the existing CoreFormalism braid and Q16_16 surfaces.
Adds a Lean ↔ C ↔ Python Q16_16 roundtrip test:
- c/q16_canonical.c: canonical saturating Q16_16 C library
- exe/Q16_16Roundtrip.lean: Lake extern_lib linked executable
- tests/test_q16_roundtrip.py: Python ↔ C harness (revived from quarantine)
Updates lakefile.lean with q16-roundtrip executable and extern_lib q16_canonical.
Build: lake build SilverSightRRC 3006 jobs, 0 errors; q16-roundtrip 5949 jobs, 0 errors
2026-06-21 10:39:18 -05:00
fbb71cffc9
feat(rrc): generate full 250-equation Corpus250 and wire into AVM emit
...
- Add python/build_corpus250.py generator (deterministic, uses classifier
receipt + PIST matrices, computes labels via SilverSight.PIST.Classify).
- Generate formal/SilverSight/RRC/Corpus250.lean with 250 FixtureRows.
- Register SilverSight.RRC.Corpus250 in lakefile.lean.
- Add AVMIsa.Emit.emitCorpus250 and update rrc-emit-fixture to emit it.
- Regenerate PROJECT_MAP.md/json.
Verification:
- lake build: 2981 jobs, 0 errors
- lake build SilverSightRRC: 2995 jobs, 0 errors
- rrc-emit-fixture | validate_rrc_predictions.py: OK 250 rows, avm_rrc_corpus250_v1
2026-06-21 10:03:02 -05:00
569c16088a
feat(pist): port minimal PIST classifier surface to SilverSight
...
- Add SilverSight.PIST.Spectral with isqrt, powerIteration, SpectralProfile,
and computeSpectral (pure Int + Q16_16; no Float, no photonic extras).
- Add SilverSight.PIST.Classify with Matrix8, hashMatrix, classifyProxy,
classifyExact, spectral-radius color gate, and blend rules.
- Add SilverSight.PIST.Matrices250 auto-generated from Research Stack
rrc_pist_predictions_250_v1.json (250 entries).
- Add python/build_pist_matrices_250.py generator with deterministic ordering
and content-hash comment.
- Register PIST modules under SilverSightRRC in lakefile.lean.
- Regenerate PROJECT_MAP.md/json.
Build: 2981 jobs, 0 errors (lake build); SilverSightRRC: 2994 jobs, 0 errors.
2026-06-21 09:46:09 -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
