|
|
5da90cd1d1
|
docs: add Clebsch diagonal cubic claim + update GraphRank proof status
- Added silversight_claim_clebsch_diagonal_cubic to manifest (Phase 2 geometry witness: 42 nodes→scar-absence, 27 lines→strand topology)
- Updated cleanMerge_preservesGap theorem with crossInputGap hypothesis and documented TODO(lean-port) boundary for Q16_16↔Bool bridge
- Compiler surface unchanged (3314 jobs, 0 errors), full workspace verified (8604 jobs)
Build: 8604 jobs, 0 errors (lake build)
|
2026-06-22 13:50:59 -05:00 |
|
|
|
73db623848
|
feat(silversight): Phase 1 core + claim promotions + theorem triage
Phase 1 core (7 new Lean files, 3307 jobs, 0 errors):
- Schema.lean: Schema class with 6 type instances
- WireFormat.lean: WireFormat structure + Layout enum
- ProductSchema.lean: Schema (α × β) instance
- ProductWireFormat.lean: Row-major pair encoders with roundTrip proofs
- Receipt.lean: Receipt structure + GateType enum
- Bind.lean: bindReceipt composition + 8 theorems
- SilverSight.lean: root import module
Claim promotions (3 claims → VERIFIED):
- silversight_claim_q16_unified: FixedPoint.lean 12 theorems, 0 sorry
- silversight_claim_eigensolid_convergence: BraidEigensolid.lean:175
- silversight_claim_receipt_invertible: BraidEigensolid.lean:249
Theorem triage (3,057 theorems classified):
- TIER_1_CORE: 118 theorems (6 modules, direct port)
- TIER_2_FOUNDATION: 1,591 theorems (121 modules)
- TIER_3_EXTENSION: 1,084 theorems (291 modules)
- TIER_4_QUARANTINE: 137 theorems (15 modules)
- TIER_5_EXCLUDED: 127 theorems (18 modules)
Build: SilverSight 3307 jobs, 0 errors, 0 sorries
|
2026-06-22 13:00:29 -05:00 |
|
