From f7c08f7a6a99dd9b4a269780c58368c617050bdd Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 21 Jun 2026 14:16:57 -0500 Subject: [PATCH] docs(plans): expand SilverSight completion pipeline to microstep level Overwrites 6-Documentation/docs/plans/SilverSight_completion_pipeline.md with a per-file, per-theorem, per-commit microstep plan covering Phases 1-8: Core Semantics completion, Research Stack triage/port, corpus build, mathematical models, shim rewrite, hardware extraction, applications, and final documentation/promotion. Includes claim-state ladder, open question answers, dependency graph, verification gates, CI coverage, risks, and acceptance criteria. --- .../plans/SilverSight_completion_pipeline.md | 2696 ++++++++++++++--- 1 file changed, 2333 insertions(+), 363 deletions(-) diff --git a/6-Documentation/docs/plans/SilverSight_completion_pipeline.md b/6-Documentation/docs/plans/SilverSight_completion_pipeline.md index b0287f54..fc9cf9f5 100644 --- a/6-Documentation/docs/plans/SilverSight_completion_pipeline.md +++ b/6-Documentation/docs/plans/SilverSight_completion_pipeline.md @@ -1,17 +1,15 @@ -# SilverSight Completion Pipeline - -**Status:** Design draft — to be approved before execution - -**Version:** 0.1 +# SilverSight Completion Pipeline — Microstep Edition +**Status:** Design draft — awaiting approval before execution +**Version:** 0.2 **Date:** 2026-06-21 **Ground truth:** Lean 4 (`/tmp/SilverSight`) + Research Stack documentation (`/home/allaun/Research Stack`) --- -## 1. Current State +## 0. Current State -The SilverSight core rebas has reached the end of its **Phase 0/1 boundary**: +The SilverSight rebas has reached the end of **Phase 0/1 boundary**: - ✅ YaFF-inspired `Semantics` core exists and compiles: - `Schema.lean`, `Layout.lean`, `WireFormat.lean`, `View.lean`, `LayoutBridge.lean`, `CanalLayout.lean` @@ -25,35 +23,29 @@ The SilverSight core rebas has reached the end of its **Phase 0/1 boundary**: - ⬜ No claim-state manifest exists yet - ⬜ Extraction targets (Python/Rust/Verilog) not generated from Lean -This pipeline describes the shortest safe path from the current state to a -**completed SilverSight 1.0**: a fully-Lean-grounded system with searchable -concepts, verified compression receipts, substrate-extractable hardware -specifications, and promotion-ready documentation. +This document expands the high-level pipeline into **per-file, per-theorem, per-commit microsteps**. Every microstep includes: + +- Goal +- Files to create or modify +- Specific definitions / theorems / functions to add +- Exact verification command(s) +- Suggested commit message +- Claim-state update --- -## 2. Design Principles +## 1. Design Principles -1. **Lean is the source of truth.** Every decision, cost, gate, and receipt - invariant is defined and proved in Lean. Python, Rust, and Verilog are - extraction targets only. -2. **No `sorry` in the main build.** Proof holes live in quarantined modules - with a `TODO(lean-port)` ticket and human sign-off. -3. **No `Float` in compute paths.** `Q0_16` is the default scalar. `Q16_16` is - allowed only with a theorem-backed justification. -4. **Receipts are the compressed state.** A receipt is not metadata; it is the - encoding. Invertibility of a receipt is the definition of lossless - transformation. -5. **Promotion is gated.** Claims advance only through the claim-state ladder - with reproducible evidence and reviewer provenance. -6. **Library method.** `Core/` defines contracts; libraries implement them. - Libraries never import other libraries. +1. **Lean is the source of truth.** Every decision, cost, gate, and receipt invariant is defined and proved in Lean. Python, Rust, and Verilog are extraction targets only. +2. **No `sorry` in the main build.** Proof holes live in quarantined modules with a `TODO(lean-port)` ticket and human sign-off. +3. **No `Float` in compute paths.** `Q0_16` is the default scalar. `Q16_16` is allowed only with a documented, theorem-backed reason. +4. **Receipts are the compressed state.** A receipt is not metadata; it is the encoding. Invertibility of a receipt is the definition of lossless transformation. +5. **Promotion is gated.** Claims advance only through the claim-state ladder with reproducible evidence and reviewer provenance. +6. **Library method.** `Core/` defines contracts; libraries implement them. Libraries never import other libraries. --- -## 3. Claim-State Ladder - -Every claim, module, and receipt advances through exactly these states: +## 2. Claim-State Ladder | State | Meaning | Exit gate | |---|---|---| @@ -62,249 +54,1429 @@ Every claim, module, and receipt advances through exactly these states: | `REVIEWED` | Independent review (LLM or human) confirms no logic leakage and no float. | Review receipt emitted and signed. | | `VERIFIED` | A Lean theorem or hardware receipt proves the claim. | `lake build` green; theorem or instrument receipt present. | -No claim may skip a state. Promotion out of `BEAUTIFUL_PROVISIONAL` requires a - Lean module or spec section; out of `CALIBRATED_ENGINEERING_DELTA` requires a -checkable artifact; out of `REVIEWED` requires a reviewer provenance receipt; -out of `VERIFIED` requires a theorem or live-hardware receipt. +No claim may skip a state. Promotion is recorded only in `docs/claims/manifest_v1.json`. --- -## 4. Phase Overview +## 3. Provisional Answers to Open Questions -| Phase | Goal | Deliverable | Build gate | -|---|---|---|---| -| 1 | Finish Core Semantics | Product encoders, `DynamicCanal` link, `Receipt`/`Bind` | `lake build SilverSightCore` | -| 2 | Triage & Port Research Stack | Inventory, keep/delete/transform list, ported theorems | `lake build SilverSightFormal` | -| 3 | Build Search Space Corpus | Corpus250, PIST matrix builder, concept index | `lake build SilverSightRRC` + fixture emit | -| 4 | Port Mathematical Models | Braid/eigensolid compression, physics manifolds | `lake build SilverSightFormal` | -| 5 | Rewrite Shims | Pure-I/O Python scripts, no decision logic | `py_compile` + pytest | -| 6 | Hardware Extraction | Verilog from Lean, FPGA receipts, 1-Wire mapping | Hardware receipt + bitstream hash | -| 7 | Applications | CAD harness, LLM review emitter, dashboard wiring | End-to-end smoke tests | -| 8 | Documentation & Promotion | Specs, claim manifests, evidence DAGs | Review + signed manifest | +| # | Question | Decision | +|---|---|---| +| 1 | Corpus250 source? | Extract from Research Stack `Semantics.RRC.Corpus250.lean`, dedup by invariant id, regenerate SilverSight `formal/SilverSight/RRC/Corpus250.lean`. | +| 2 | Rebuild AVM? | **No.** Keep existing `formal/SilverSight/AVMIsa/` as canonical. Bridge Core AVM δ to AVMIsa in Phase 2. | +| 3 | Physics scope for 1.0? | Only braid/eigensolid compression and DynamicCanal. Other manifolds deferred to 1.1. | +| 4 | Hardware target? | Primary: Verilator simulation of generated Verilog. Bonus: Tang Nano 20K live receipt if hardware is available. | +| 5 | Reviewers? | `REVIEWED` via canonical LLM review emitter. `VERIFIED` requires human sign-off or hardware receipt. | + +--- + +## 4. Microstep Dependency Graph + +```text +Phase 1 ──► Phase 2 ──► Phase 3 ──► Phase 4 ──► Phase 5 ──► Phase 6 ──► Phase 7 ──► Phase 8 + │ │ │ │ │ │ │ + ▼ ▼ ▼ ▼ ▼ ▼ ▼ + Core Formal Corpus Comp Shims Hardware Apps Promotion +Semantics theorems / PIST theorems / Docs +``` + +Within a phase, microsteps are ordered. Cross-phase parallelism is allowed only where no file overlap exists. --- ## 5. Phase 1 — Finish Core Semantics -**Goal:** Make the schema/layout/wireformat stack useful for real structured -objects and link it to substrate physics. +**Phase goal:** Make the schema/layout/wireformat stack useful for real structured objects and link it to substrate physics. -### 5.1 Product-Type Encodings +**Claim target at phase end:** All Phase 1 claims at `CALIBRATED_ENGINEERING_DELTA`; key theorems at `REVIEWED`. -Implement certified `WireFormat` and `LayoutBridge` instances for fixed-size -product types so that braid states, fixture rows, and receipts can be encoded -without marshalling through JSON. +--- -```text -Core/SilverSight/Semantics/ - ProductSchema.lean -- Schema instance for tuples / structures - ProductWireFormat.lean -- Row-major, columnar, compact encoders - ProductLayoutBridge.lean-- rowMajor <-> columnar <-> compact bridges +### 1.1 Product schema instances for pairs + +**Goal:** Extend `Schema` to fixed-size product types. + +**Files:** +- `/tmp/SilverSight/Core/SilverSight/Semantics/ProductSchema.lean` (new) +- `/tmp/SilverSight/lakefile.lean` (add root) + +**Specific additions:** + +```lean +namespace SilverSight.Semantics + +instance [Schema α] [Schema β] : Schema (α × β) where + byteSize := byteSize α + byteSize β + wellFormed := fun (a, b) => wellFormed a && wellFormed b + +@[simp] theorem prod_byteSize [Schema α] [Schema β] : + byteSize (α × β) = byteSize α + byteSize β := rfl + +theorem prod_wellFormed [Schema α] [Schema β] (a : α) (b : β) : + wellFormed (a, b) = (wellFormed a && wellFormed b) := rfl + +end SilverSight.Semantics ``` -**Required theorems:** -- `product_encode_size` — encoded product size equals sum of field sizes. -- `product_roundTrip` — decode after encode is identity. -- `bridge_product_correct` — layout bridge preserves product encoding. +**Verification:** -**Example target:** `BraidState` (8 strands × fixed fields) encoded to a 64-byte -row-major `ByteArray`. - -### 5.2 DynamicCanal Integration - -Move `CanalRegime` from a free-standing enum to a physics-backed decision: - -```text -formal/CoreFormalism/DynamicCanal/ - Regime.lean -- CanalRegime + classifyRegime from pressure - Lane.lean -- Lane geometry and λ_eff(P) - Timing.lean -- Timing parameters derived from canal state +```bash +cd /tmp/SilverSight +lake build SilverSightCore ``` -**Link:** `CanalLayout.chooseLayout` calls `DynamicCanal.classifyRegime` to -override the cost-based choice when the substrate is in `stressed` or `throat`. - -**Required theorem:** `regime_override_preserves_cost_bound` — a regime override -never selects a layout more than a documented ε factor worse than the pure cost -optimum. - -### 5.3 Receipt and Bind Core - -Implement the receipt type and the `bind` primitive that composes gates: +**Commit:** ```text -Core/SilverSight/ - Receipt.lean -- Receipt schema, wellFormed, validation - Bind.lean -- bind : Gate a b -> Gate b c -> Gate a c -Core/SilverSightCore.lean -- integrate Receipt and bind into the invariant center +feat(core): add product schema instance + +Adds Schema instance for α × β with byteSize and wellFormed theorems. + +Build: N jobs, 0 errors (lake build SilverSightCore) ``` -**Required theorems:** -- `Receipt.wellFormed_decidable` -- `bind_associative` -- `bind_identity_left` / `bind_identity_right` +**Claim update:** `silversight_claim_product_schema` → `CALIBRATED_ENGINEERING_DELTA`. -### 5.4 Fixed-Point Completion +--- -Ensure `Q0_16` is the default dimensionless scalar and `Q16_16` is available -with a documented reason. Remove any remaining `Float` from core compute paths. +### 1.2 Row-major wire format for pairs + +**Goal:** Certify encode/decode for pairs. + +**Files:** +- `/tmp/SilverSight/Core/SilverSight/Semantics/ProductWireFormat.lean` (new) +- `/tmp/SilverSight/lakefile.lean` (add root) + +**Specific additions:** + +```lean +def prodRowMajor [Schema α] [Schema β] + (wfα : WireFormat α rowMajor) (wfβ : WireFormat β rowMajor) : + WireFormat (α × β) rowMajor where + encode := fun (a, b) => wfα.encode a ++ wfβ.encode b + decode := fun bs => + if h : bs.size = byteSize α + byteSize β then + let bsα := bs.extract 0 (byteSize α) + let bsβ := bs.extract (byteSize α) bs.size + Option.bind (wfα.decode bsα) fun a => + Option.map (wfβ.decode bsβ) fun b => (a, b) + else none + encode_size := by ... + roundTrip := by ... + +theorem prod_encode_size [Schema α] [Schema β] + (wfα : WireFormat α rowMajor) (wfβ : WireFormat β rowMajor) (a : α) (b : β) : + ((prodRowMajor wfα wfβ).encode (a, b)).size = byteSize (α × β) := ... + +theorem prod_roundTrip [Schema α] [Schema β] + (wfα : WireFormat α rowMajor) (wfβ : WireFormat β rowMajor) (a : α) (b : β) : + (prodRowMajor wfα wfβ).decode ((prodRowMajor wfα wfβ).encode (a, b)) = some (a, b) := ... +``` + +Add `#eval` example: + +```lean +#eval (prodRowMajor WireFormat.uint8RowMajor WireFormat.boolRowMajor).encode (42, true) +``` **Verification:** ```bash lake build SilverSightCore -lake build SilverSightFormal -python3 tests/test_q16_roundtrip.py -.lake/build/bin/q16-roundtrip ``` +**Commit:** + +```text +feat(core): add row-major wire format for product types + +Certified encode/decode/roundTrip for α × β. Includes #eval witness. + +Build: N jobs, 0 errors (lake build SilverSightCore) +``` + +**Claim update:** `silversight_claim_product_wireformat` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.3 Identity and columnar product bridges + +**Goal:** Provide layout bridges for pairs. + +**Files:** +- `/tmp/SilverSight/Core/SilverSight/Semantics/ProductLayoutBridge.lean` (new) +- `/tmp/SilverSight/lakefile.lean` (add root) + +**Specific additions:** + +```lean +-- Identity bridge for pairs +def prodIdentity [Schema α] [Schema β] + (wfα : WireFormat α L) (wfβ : WireFormat β L) : + LayoutBridge (α × β) L L := + LayoutBridge.identity (ProductWireFormat.prodRowMajor wfα wfβ) + +-- Columnar wire format for pairs (fields stored contiguously by field index) +def prodColumnar [Schema α] [Schema β] + (wfα : WireFormat α rowMajor) (wfβ : WireFormat β rowMajor) : + WireFormat (α × β) columnar := ... + +-- Bridge row-major ↔ columnar for pairs +def prodRowMajorToColumnar [Schema α] [Schema β] + (wfα : WireFormat α rowMajor) (wfβ : WireFormat β rowMajor) : + LayoutBridge (α × β) rowMajor columnar where + wf1 := ProductWireFormat.prodRowMajor wfα wfβ + wf2 := prodColumnar wfα wfβ + convert := fun bs => + -- For pairs, row-major and columnar coincide; bridge is identity + bs + correct := by ... +``` + +**Verification:** + +```bash +lake build SilverSightCore +``` + +**Commit:** + +```text +feat(core): add product layout bridges + +Identity and rowMajor↔columnar bridges for α × β. + +Build: N jobs, 0 errors (lake build SilverSightCore) +``` + +**Claim update:** `silversight_claim_product_layout_bridge` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.4 Zero-copy views for product fields + +**Goal:** Allow reading product components through `View` without copying. + +**Files:** +- `/tmp/SilverSight/Core/SilverSight/Semantics/ProductView.lean` (new) +- `/tmp/SilverSight/lakefile.lean` (add root) + +**Specific additions:** + +```lean +def View.fst [Schema α] [Schema β] (v : View (α × β)) : View α where + base := v.base + offset := v.offset + valid := by have h := v.valid; simp [prod_byteSize] at h ⊢; linarith + +def View.snd [Schema α] [Schema β] (v : View (α × β)) : View β where + base := v.base + offset := v.offset + byteSize α + valid := by have h := v.valid; simp [prod_byteSize] at h ⊢; linarith + +theorem readFst_eq [Schema α] [Schema β] (v : View (α × β)) (h : byteSize α = 1) : + (View.fst v).readUInt8 = v.base.get v.offset ... := ... +``` + +**Verification:** + +```bash +lake build SilverSightCore +``` + +**Commit:** + +```text +feat(core): add zero-copy product views + +View.fst / View.snd preserve the address-arithmetic invariant. + +Build: N jobs, 0 errors (lake build SilverSightCore) +``` + +**Claim update:** `silversight_claim_product_view` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.5 Schema / wire format for Q16_16 and fixed-size arrays + +**Goal:** Certify encodings for the numeric atoms used by braid states. + +**Files:** +- `/tmp/SilverSight/Core/SilverSight/Semantics/Schema.lean` (append) +- `/tmp/SilverSight/Core/SilverSight/Semantics/WireFormat.lean` (append) + +**Specific additions:** + +```lean +-- In Schema.lean +instance : Schema Q16_16 where + byteSize := 4 + wellFormed := fun _ => true + +@[simp] theorem q16_16_byteSize : byteSize Q16_16 = 4 := rfl + +-- Fixed-length array schema +def Schema.array (n : Nat) (α : Type) [Schema α] : Schema (Fin n → α) where + byteSize := n * byteSize α + wellFormed := fun _ => true +``` + +```lean +-- In WireFormat.lean +def q16_16RowMajor : WireFormat Q16_16 rowMajor where + encode := fun q => ... -- 4 raw bytes, big-endian + decode := fun bs => ... + encode_size := ... + roundTrip := ... + +def arrayRowMajor (n : Nat) (α : Type) [Schema α] + (wf : WireFormat α rowMajor) : WireFormat (Fin n → α) rowMajor := ... +``` + +**Verification:** + +```bash +lake build SilverSightCore +``` + +**Commit:** + +```text +feat(core): add Q16_16 and fixed-array wire formats + +Certified encodings for the numeric atoms used by braid states. + +Build: N jobs, 0 errors (lake build SilverSightCore) +``` + +**Claim update:** `silversight_claim_numeric_wireformat` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.6 BraidState wire encoding + +**Goal:** Provide a certified wire format for the canonical braid state object. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/BraidStateEncoding.lean` (new) +- `/tmp/SilverSight/lakefile.lean` (add root to `SilverSightFormal`) + +**Specific additions:** + +```lean +import CoreFormalism.BraidStrand +import CoreFormalism.BraidEigensolid +import SilverSight.Semantics.ProductSchema +import SilverSight.Semantics.ProductWireFormat +import SilverSight.Semantics.LayoutBridge + +namespace SilverSight.BraidStateEncoding + +-- Schema instances for braid sub-structures +instance : Schema PhaseVec where byteSize := 8; wellFormed := fun _ => true +instance : Schema BraidBracket where byteSize := 24; wellFormed := fun _ => true +instance : Schema BraidStrand where byteSize := 48; wellFormed := fun _ => true +instance : Schema BraidState where byteSize := 392; wellFormed := fun _ => true + +-- Row-major wire format for BraidState +def braidStateRowMajor : WireFormat BraidState rowMajor := ... + +-- Identity bridge +def braidStateRowMajorBridge : LayoutBridge BraidState rowMajor rowMajor := + LayoutBridge.identity braidStateRowMajor + +#eval braidStateRowMajor.encode (BraidEigensolid.BraidState.mk ...) + +theorem braid_state_encode_size (s : BraidState) : + (braidStateRowMajor.encode s).size = 392 := ... + +theorem braid_state_roundTrip (s : BraidState) : + braidStateRowMajor.decode (braidStateRowMajor.encode s) = some s := ... + +end SilverSight.BraidStateEncoding +``` + +**Verification:** + +```bash +lake build SilverSightFormal +``` + +**Commit:** + +```text +feat(formal): add BraidState wire encoding + +Certified row-major encoding for BraidState using Core product schema. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_braid_state_encoding` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.7 Extract DynamicCanal regime classifier + +**Goal:** Make the canal regime available to Core layout selection without importing the full physics into Core. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/DynamicCanal/Regime.lean` (new) +- `/tmp/SilverSight/formal/CoreFormalism/DynamicCanal.lean` (refactor to re-export) +- `/tmp/SilverSight/lakefile.lean` (update root if needed) + +**Specific additions:** + +```lean +-- DynamicCanal/Regime.lean +namespace SilverSight.DynamicCanal + +inductive Regime where | coherent | stressed | throat + deriving Repr, DecidableEq, BEq + +def classifyRegime (pressure lambdaEff : Q16_16) (pStress pThroat : Q16_16) : Regime := + if pressure ≥ pStress then Regime.stressed + else if lambdaEff ≤ pThroat then Regime.throat + else Regime.coherent + +theorem classifyRegime_coherent_at_low_pressure + (pressure lambdaEff pStress pThroat : Q16_16) + (h1 : pressure < pStress) (h2 : lambdaEff > pThroat) : + classifyRegime pressure lambdaEff pStress pThroat = Regime.coherent := ... + +end SilverSight.DynamicCanal +``` + +Refactor `DynamicCanal.lean` to `import CoreFormalism.DynamicCanal.Regime` and re-export `Regime`. + +**Verification:** + +```bash +lake build SilverSightFormal +``` + +**Commit:** + +```text +refactor(formal): extract DynamicCanal.Regime module + +Isolates the regime classifier so Core layout selection can use it. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_canal_regime` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.8 Bridge canal regime to Core layout selection + +**Goal:** Link `CanalLayout.chooseLayout` to DynamicCanal physics. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/DynamicCanal/CanalLayoutLink.lean` (new) +- `/tmp/SilverSight/lakefile.lean` (add root) + +**Specific additions:** + +```lean +import SilverSight.Semantics.CanalLayout +import CoreFormalism.DynamicCanal.Regime + +namespace SilverSight.DynamicCanal + +def toCoreRegime : Regime → SilverSight.Semantics.CanalRegime + | Regime.coherent => CanalRegime.coherent + | Regime.stressed => CanalRegime.stressed + | Regime.throat => CanalRegime.throat + +def layoutForCanal (profile : AccessProfile) (pressure lambdaEff pStress pThroat : Q16_16) : + Layout := + CanalLayout.chooseLayout profile (toCoreRegime (classifyRegime pressure lambdaEff pStress pThroat)) + +theorem layoutForCanal_coherent_uses_cost + (profile : AccessProfile) (pressure lambdaEff pStress pThroat : Q16_16) + (h1 : pressure < pStress) (h2 : lambdaEff > pThroat) : + layoutForCanal profile pressure lambdaEff pStress pThroat = chooseLayoutByCost profile := ... + +theorem regime_override_preserves_cost_bound + (profile : AccessProfile) (pressure lambdaEff pStress pThroat : Q16_16) (l : Layout) : + le (Layout.cost (layoutForCanal profile pressure lambdaEff pStress pThroat) profile) + (Layout.cost l profile) ∨ + classifyRegime pressure lambdaEff pStress pThroat ≠ Regime.coherent := ... + +end SilverSight.DynamicCanal +``` + +**Verification:** + +```bash +lake build SilverSightFormal +``` + +**Commit:** + +```text +feat(formal): link DynamicCanal regime to Core layout selector + +Adds layoutForCanal and proves coherent-regime cost equivalence. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_canal_layout_link` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.9 ReceiptHeader schema and wire format + +**Goal:** Make `Receipt` serializable as a fixed-size header plus side buffers. + +**Files:** +- `/tmp/SilverSight/Core/SilverSight/Receipt.lean` (new) +- `/tmp/SilverSight/Core/SilverSightCore.lean` (update `Receipt` if needed) +- `/tmp/SilverSight/lakefile.lean` (add root) + +**Specific additions:** + +```lean +-- Core/SilverSight/Receipt.lean +namespace SilverSight.Core + +structure ReceiptHeader where + receiptIDHash : UInt64 + expressionHash : UInt64 + finalState : HachimojiState + ticCount : UInt64 + fuelUsed : UInt64 + pathCostRaw : UInt32 -- sentinel 0xFFFFFFFF means none + verified : Bool + libraryRefCount : UInt8 + libraryRefsHash : UInt64 + deriving DecidableEq, Repr, BEq + +instance : Schema ReceiptHeader where + byteSize := 48 + wellFormed := fun _ => true + +def receiptHeaderRowMajor : WireFormat ReceiptHeader rowMajor := ... + +def Receipt.toHeader (r : Receipt) : ReceiptHeader := ... + +def Receipt.fromHeader (h : ReceiptHeader) (idText exprText refsText : String) : Receipt := ... + +theorem fromHeader_toHeader (r : Receipt) : + Receipt.fromHeader (Receipt.toHeader r) r.receiptID r.expression + (String.intercalate "," r.libraryRefs) = r := ... + +end SilverSight.Core +``` + +**Verification:** + +```bash +lake build SilverSightCore +``` + +**Commit:** + +```text +feat(core): add ReceiptHeader schema and wire format + +Fixed-size 48-byte header for Receipt; variable text lives in side buffers. + +Build: N jobs, 0 errors (lake build SilverSightCore) +``` + +**Claim update:** `silversight_claim_receipt_header` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.10 Bind primitive in Core + +**Goal:** Provide a lawful `bind` composition primitive for gates. + +**Files:** +- `/tmp/SilverSight/Core/SilverSight/Bind.lean` (new) +- `/tmp/SilverSight/lakefile.lean` (add root) + +**Specific additions:** + +```lean +namespace SilverSight.Core + +-- A gate is a partial function with a proof-carrying invariant +structure Gate (α β : Type) [Schema α] [Schema β] where + run : α → Option β + inv : α → β → Bool + preserves : ∀ a b, run a = some b → inv a b = true + +def Gate.bind [Schema α] [Schema β] [Schema γ] + (g1 : Gate α β) (g2 : Gate β γ) : Gate α γ where + run := fun a => + match g1.run a with + | none => none + | some b => g2.run b + inv := fun a c => + ∃ b, g1.inv a b = true ∧ g2.inv b c = true + preserves := by ... + +def Gate.id [Schema α] : Gate α α where + run := some + inv := fun _ b => true + preserves := by ... + +theorem Gate.bind_assoc [Schema α] [Schema β] [Schema γ] [Schema δ] + (g1 : Gate α β) (g2 : Gate β γ) (g3 : Gate γ δ) : + Gate.bind (Gate.bind g1 g2) g3 = Gate.bind g1 (Gate.bind g2 g3) := ... + +theorem Gate.bind_id_left [Schema α] [Schema β] (g : Gate α β) : + Gate.bind (Gate.id : Gate α α) g = g := ... + +theorem Gate.bind_id_right [Schema α] [Schema β] (g : Gate α β) : + Gate.bind g (Gate.id : Gate β β) = g := ... + +end SilverSight.Core +``` + +**Verification:** + +```bash +lake build SilverSightCore +``` + +**Commit:** + +```text +feat(core): add Gate and lawful bind primitive + +Associativity and identity theorems for Core gate composition. + +Build: N jobs, 0 errors (lake build SilverSightCore) +``` + +**Claim update:** `silversight_claim_bind_core` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.11 Integrate Receipt and Bind into SilverSightCore + +**Goal:** Wire the new modules into the invariant center while preserving existing behavior. + +**Files:** +- `/tmp/SilverSight/Core/SilverSightCore.lean` +- `/tmp/SilverSight/lakefile.lean` + +**Specific additions:** + +```lean +import SilverSight.Receipt +import SilverSight.Bind + +-- Extend Library to carry a Gate-like contract +abbrev Library := String → Receipt + +def Receipt.toAVMInstruction (r : Receipt) : Instruction := + Instruction.Verify r + +#eval (Receipt.empty.toHeader).toString +``` + +**Verification:** + +```bash +lake build SilverSightCore +lake build +``` + +**Commit:** + +```text +feat(core): integrate Receipt and Bind into SilverSightCore + +Wires ReceiptHeader and Gate into the invariant center. + +Build: N jobs, 0 errors (lake build) +``` + +**Claim update:** `silversight_claim_core_integrated` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 1.12 Phase 1 docs and project map + +**Goal:** Keep specs, architecture, glossary, and project map in lockstep. + +**Files:** +- `/home/allaun/Research Stack/6-Documentation/docs/specs/SilverSight_Spec.md` +- `/tmp/SilverSight/docs/ARCHITECTURE.md` +- `/tmp/SilverSight/AGENTS.md` +- `/tmp/SilverSight/docs/GLOSSARY.md` +- `/tmp/SilverSight/docs/PROJECT_MAP.{md,json}` +- `/tmp/SilverSight/docs/build_logs/2026-06-21_phase1_completion.md` (new) + +**Specific additions:** + +- Update spec §3.1–§3.5 and §4.1 with implemented module names and theorems. +- Update `ARCHITECTURE.md` Layer 1 table to list all new modules. +- Update `AGENTS.md` build baseline and blessed surfaces. +- Add glossary entries: `ProductSchema`, `ProductWireFormat`, `ProductLayoutBridge`, `ProductView`, `ReceiptHeader`, `Gate`, `DynamicCanal.Regime`, `layoutForCanal`. +- Regenerate project map: + +```bash +cd /tmp/SilverSight +python3 docs/generate_project_map.py +python3 .github/scripts/glossary_lint.py +python3 .github/scripts/check_doc_sync.py +``` + +**Verification:** + +```bash +lake build +python3 -m py_compile python/*.py .github/scripts/*.py +``` + +**Commit:** + +```text +docs(core): update spec, architecture, glossary, and project map for Phase 1 + +Documents the completed Core Semantics surface and DynamicCanal link. + +Build: N jobs, 0 errors (lake build) +``` + +**Claim update:** Phase 1 documentation claims → `REVIEWED`. + --- ## 6. Phase 2 — Triage and Port Research Stack Theorems -**Goal:** Decide what survives from Research Stack and port it cleanly. +**Phase goal:** Decide what survives from Research Stack and port it cleanly. -### 6.1 Inventory - -Run the existing inventory scripts to produce a machine-readable map: - -```bash -cd /home/allaun/Research Stack -python3 scripts/inventory_everything.py # Postgres + Gremlin + repo -python3 extraction/generate_porting_candidates.py # if available -cd /tmp/SilverSight -python3 docs/generate_research_stack_usage_map.py # cross-reference usage -python3 docs/generate_porting_candidates.py # produce keep/delete/transform list -``` - -**Output:** -- `extraction/all_concepts_merged.json` (Research Stack) -- `docs/research_stack_triage_report.md` (SilverSight) - -### 6.2 Triage Rules - -Apply the spec rules: - -| Action | Criterion | -|---|---| -| **Keep** | Compiles under `lake build`; has a theorem or `#eval` witness; no `Float` in compute path. | -| **Delete** | Duplicate `Q16_16`, demo scripts, SaaS integrations, unproven Python decision logic. | -| **Transform** | Python shims → pure I/O; markdown specs → structured sections; Rust/Verilog → extraction targets. | -| **Quarantine** | Contains `sorry` or `unsafe` and is not on the critical path; mark `TODO(lean-port)`. | - -### 6.3 Port Order - -1. Fixed-point and numeric lemmas (`Semantics.FixedPoint` family). -2. Sidon sets and interaction graphs (`SidonSets.lean`, `InteractionGraphSidon.lean`). -3. Braid dynamics (`BraidStrand.lean`, `BraidCross.lean`, `BraidEigensolid.lean`). -4. Sieve lemmas and weak-axis CRT (`SieveLemmas.lean`). -5. Remaining physics modules only if needed by Phase 4 compression claims. - -### 6.4 Module Destination Map - -| Research Stack module | SilverSight destination | Notes | -|---|---|---| -| `Semantics.FixedPoint.lean` | `Core/SilverSight/FixedPoint.lean` | Already canonical. | -| `Semantics.SidonSets.lean` | `formal/CoreFormalism/SidonSets.lean` | Keep. | -| `Semantics.InteractionGraphSidon.lean` | `formal/CoreFormalism/InteractionGraphSidon.lean` | Keep. | -| `Semantics.SieveLemmas.lean` | `formal/CoreFormalism/SieveLemmas.lean` | Keep. | -| `Semantics.Braid*.lean` | `formal/CoreFormalism/Braid*.lean` | Keep. | -| `Semantics.RRC.*.lean` | `formal/SilverSight/RRC/*.lean` | Port selectively. | -| `Semantics.AVMIsa.*.lean` | `formal/SilverSight/AVMIsa/*.lean` | Already present; reconcile diffs. | -| `4-Infrastructure/shim/*.py` | `python/` or delete | Strip decision logic. | - -### 6.5 Verification - -```bash -lake build SilverSightFormal # must stay green after each ported module -lake build SilverSightRRC # must stay green after RRC ports -``` +**Claim target at phase end:** Foundation modules at `VERIFIED`; quarantined modules documented. --- -## 7. Phase 3 — Build Search Space Corpus +### 2.1 Run inventory scripts -**Goal:** Produce the 250-equation corpus and the PIST matrix pipeline so that -RRC alignment has real inputs. +**Goal:** Produce a machine-readable map of Research Stack concepts and SilverSight candidates. -### 7.1 Corpus250 Builder +**Files:** +- `/home/allaun/Research Stack/scripts/inventory_everything.py` +- `/tmp/SilverSight/docs/generate_research_stack_usage_map.py` +- `/tmp/SilverSight/docs/generate_porting_candidates.py` +- `/tmp/SilverSight/docs/research_stack_triage_report.md` (new) -Create or port the 250-equation fixture corpus as a pure data module: - -```text -formal/SilverSight/RRC/Corpus250.lean -- 250 FixtureRow values -python/pist_matrix_builder.py -- generate 8x8 strand matrices -python/build_corpus250.py -- merge PIST labels into FixtureRows -``` - -**Rules:** -- Equations are raw text; no admissibility logic in Python. -- `pistProxyLabel` / `pistExactLabel` are populated only when PIST predictions exist. -- Alignment status remains `missingPrediction` until labels are present. - -### 7.2 Concept Index - -Generate a searchable concept index: - -```text -python/inventory_concepts.py - → docs/concepts.json - → docs/concepts.md -``` - -Each concept gets a stable ID: - -```text -silversight___ -``` - -### 7.3 RRC Emit Fixture Executable - -Ensure `exe/RrcEmitFixture.lean` emits the full corpus as AVM-stamped JSON: +**Specific additions:** ```bash -lake build rrc-emit-fixture -.lake/build/bin/rrc-emit-fixture > /tmp/rrc_fixture_emitted.json -python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json +cd /home/allaun/Research Stack +python3 scripts/inventory_everything.py + +cd /tmp/SilverSight +python3 docs/generate_research_stack_usage_map.py +python3 docs/generate_porting_candidates.py ``` **Verification:** +- `docs/research_stack_porting_candidates.md` exists and lists candidates. +- `extraction/all_concepts_merged.json` exists in Research Stack. + +**Commit:** + +```text +docs(formal): add Research Stack inventory and porting candidates + +Generates triage inputs from inventory scripts. +``` + +**Claim update:** `silversight_claim_research_inventory` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 2.2 Define triage criteria and manifest + +**Goal:** Classify every Research Stack module as keep/delete/transform/quarantine. + +**Files:** +- `/tmp/SilverSight/python/triage_module.py` (new) +- `/tmp/SilverSight/docs/triage_manifest.json` (new) + +**Specific additions:** + +```python +def classify_module(module_info: dict) -> dict: + if module_info.get("sorry_count", 0) > 5: + return {"action": "quarantine", "reason": "too many sorries"} + if module_info.get("math_kind") in {"fixedpoint", "number_theory", "braid", "rrc", "avm"}: + return {"action": "keep", "reason": "foundational"} + if module_info.get("math_kind") == "demo": + return {"action": "delete", "reason": "demo script"} + return {"action": "transform", "reason": "review required"} +``` + +**Verification:** + +```bash +python3 -m py_compile python/triage_module.py +python3 python/triage_module.py +python3 -m json.tool docs/triage_manifest.json +``` + +**Commit:** + +```text +feat(python): add Research Stack triage classifier + +Produces docs/triage_manifest.json with keep/delete/transform/quarantine verdicts. +``` + +**Claim update:** `silversight_claim_triage_manifest` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 2.3 Unify fixed-point definitions + +**Goal:** Remove duplicate Q16_16 definitions; make `SilverSight.FixedPoint.Q16_16` canonical. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/FixedPoint.lean` (delete or replace with re-export) +- `/tmp/SilverSight/formal/CoreFormalism/Q16_16Numerics.lean` (update imports) +- `/tmp/SilverSight/formal/CoreFormalism/DynamicCanal.lean` (update imports if needed) +- `/tmp/SilverSight/lakefile.lean` (remove `CoreFormalism.FixedPoint` root) + +**Specific additions:** + +```lean +-- formal/CoreFormalism/FixedPoint.lean becomes a re-export shim +import SilverSight.FixedPoint +export SilverSight.FixedPoint (Q16_16 Q0_16) +``` + +**Verification:** + +```bash +lake build SilverSightFormal +lake build SilverSightRRC +``` + +**Commit:** + +```text +refactor(formal): unify Q16_16 on SilverSight.FixedPoint + +Replaces CoreFormalism.FixedPoint shim with canonical Core definition. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_q16_unified` → `VERIFIED`. + +--- + +### 2.4 Verify foundation modules compile + +**Goal:** Ensure Sidon, interaction graph, sieve, and braid modules build without modification. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/SidonSets.lean` +- `/tmp/SilverSight/formal/CoreFormalism/InteractionGraphSidon.lean` +- `/tmp/SilverSight/formal/CoreFormalism/SieveLemmas.lean` +- `/tmp/SilverSight/formal/CoreFormalism/BraidStrand.lean` +- `/tmp/SilverSight/formal/CoreFormalism/BraidCross.lean` +- `/tmp/SilverSight/formal/CoreFormalism/BraidEigensolid.lean` +- `/tmp/SilverSight/formal/CoreFormalism/BraidField.lean` +- `/tmp/SilverSight/formal/CoreFormalism/BraidSpherionBridge.lean` +- `/tmp/SilverSight/formal/CoreFormalism/BraidBracket.lean` + +**Specific additions:** + +- Add `#eval` witnesses for `eigensolid_convergence` and `receipt_invertible`. +- Document any `sorry` with `TODO(lean-port)`. + +**Verification:** + +```bash +lake build SilverSightFormal +``` + +**Commit:** + +```text +chore(formal): verify foundation theorem modules + +Adds #eval witnesses and TODO(lean-port) markers to braid/sidon modules. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** Foundation theorem claims → `VERIFIED` (theorems already proved). + +--- + +### 2.5 Port RRC foundation modules + +**Goal:** Ensure RRC alignment gate and AVM ISA surface are complete. + +**Files:** +- `/tmp/SilverSight/formal/SilverSight/RRC/Emit.lean` +- `/tmp/SilverSight/formal/SilverSight/AVMIsa/*.lean` +- `/tmp/SilverSight/formal/SilverSight/ReceiptCore.lean` + +**Specific additions:** + +- Reconcile any drift against Research Stack `Semantics.RRC.Emit.lean`. +- Add `Receipt.toSilverSightReceipt` bridge if missing. +- Ensure `AVMIsa.Emit` is the sole top-level JSON emitter. + +**Verification:** + ```bash lake build SilverSightRRC lake build rrc-emit-fixture -python3 -m py_compile python/*.py +``` + +**Commit:** + +```text +feat(rrc): reconcile RRC and AVM ISA surfaces + +Aligns SilverSight RRC/Emit and AVMIsa with Research Stack sources. + +Build: N jobs, 0 errors (lake build SilverSightRRC) +``` + +**Claim update:** `silversight_claim_rrc_surface` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 2.6 Create PIST matrix modules + +**Goal:** Provide the PIST classification surface referenced by the lakefile. + +**Files:** +- `/tmp/SilverSight/formal/SilverSight/PIST/Spectral.lean` (new) +- `/tmp/SilverSight/formal/SilverSight/PIST/Classify.lean` (new) +- `/tmp/SilverSight/formal/SilverSight/PIST/Matrices250.lean` (new) + +**Specific additions:** + +```lean +-- PIST/Spectral.lean +namespace SilverSight.PIST + +def tokenStrand (tokenIdx : Nat) : Fin 8 := ⟨tokenIdx % 8, by omega⟩ + +def buildAdjacencyMatrix (tokens : List String) : Fin 8 → Fin 8 → Nat := ... + +end SilverSight.PIST +``` + +```lean +-- PIST/Classify.lean +def classifyMatrix (m : Fin 8 → Fin 8 → Nat) : Option PISTLabel := ... +``` + +```lean +-- PIST/Matrices250.lean +def matrices : List (String × Fin 8 → Fin 8 → Nat) := ... +``` + +**Verification:** + +```bash +lake build SilverSightRRC +``` + +**Commit:** + +```text +feat(rrc): add PIST spectral and classification surface + +Implements token-strand adjacency and matrix classification in Lean. + +Build: N jobs, 0 errors (lake build SilverSightRRC) +``` + +**Claim update:** `silversight_claim_pist_surface` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 2.7 Quarantine sorry-bearing modules + +**Goal:** Keep the main build clean while preserving WIP modules. + +**Files:** +- `/tmp/SilverSight/quarantine/` (new directory) +- `/tmp/SilverSight/QUARANTINE.md` (new) +- `/tmp/SilverSight/lakefile.lean` + +**Specific additions:** + +- Move modules with `sorry` in the main import path to `quarantine/`. +- Add `TODO(lean-port): ` comment above every `sorry`. +- Document each quarantined module in `QUARANTINE.md`. + +**Verification:** + +```bash +lake build +# Confirm no sorry in main build +grep -R "sorry" Core/SilverSight/ formal/CoreFormalism/ formal/SilverSight/ || true +``` + +**Commit:** + +```text +chore(formal): quarantine sorry-bearing modules + +Moves WIP modules out of the main build with TODO(lean-port) tickets. + +Build: N jobs, 0 errors (lake build) +``` + +**Claim update:** Quarantine claims → `BEAUTIFUL_PROVISIONAL`. + +--- + +### 2.8 Delete/transform Research Stack shims + +**Goal:** Produce a concrete keep/delete/transform list for Python scripts. + +**Files:** +- `/tmp/SilverSight/docs/shim_transform_plan.md` (new) + +**Specific additions:** + +| Research Stack shim | SilverSight action | +|---|---| +| `pist_classify.py` | Delete logic; move to `formal/SilverSight/PIST/Classify.lean`. | +| `pist_matrix_builder.py` | Transform to pure I/O. | +| `ene_migrate_and_tag.py` | Delete (ENE/RDS not in SilverSight). | +| `rds_connect.py` | Delete. | +| `batch_embed_artifacts.py` | Delete. | + +**Verification:** + +- Document reviewed by glossary lint. + +**Commit:** + +```text +docs(infra): add shim transform plan + +Lists keep/delete/transform verdicts for Research Stack Python shims. +``` + +**Claim update:** `silversight_claim_shim_transform_plan` → `REVIEWED`. + +--- + +### 2.9 Port CoreFormalism.Bind to Core-compatible bind + +**Goal:** Reconcile the existing `CoreFormalism/Bind.lean` with the new Core `Gate.bind`. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/Bind.lean` +- `/tmp/SilverSight/Core/SilverSight/Bind.lean` + +**Specific additions:** + +- Add `Gate.toBind` and `Bind.toGate` bridges. +- Prove `toBind_toGate_id` and `toGate_toBind_id` for simple cases. + +**Verification:** + +```bash +lake build SilverSightCore +lake build SilverSightFormal +``` + +**Commit:** + +```text +feat(formal): bridge Core Gate and CoreFormalism Bind + +Adds conversion between Core Gate.bind and library Bind primitive. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_bind_bridge` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 2.10 Phase 2 docs and project map + +**Goal:** Document the ported foundation surface. + +**Files:** +- `/tmp/SilverSight/docs/ARCHITECTURE.md` +- `/tmp/SilverSight/AGENTS.md` +- `/tmp/SilverSight/docs/GLOSSARY.md` +- `/tmp/SilverSight/docs/PROJECT_MAP.{md,json}` +- `/tmp/SilverSight/docs/build_logs/2026-06-21_phase2_completion.md` (new) + +**Specific additions:** + +- Update Layer 2 table with quarantine status. +- Update build baseline. +- Regenerate project map. + +**Verification:** + +```bash +lake build +python3 docs/generate_project_map.py +python3 .github/scripts/glossary_lint.py +python3 .github/scripts/check_doc_sync.py +``` + +**Commit:** + +```text +docs(formal): update architecture and glossary for Phase 2 port + +Documents foundation module status and quarantine list. + +Build: N jobs, 0 errors (lake build) +``` + +**Claim update:** Phase 2 documentation claims → `REVIEWED`. + +--- + +## 7. Phase 3 — Build Search Space Corpus + +**Phase goal:** Produce the 250-equation corpus and the PIST matrix pipeline. + +**Claim target at phase end:** Corpus250 emits AVM-stamped JSON; PIST pipeline is pure I/O. + +--- + +### 3.1 Extract Corpus250 source from Research Stack + +**Goal:** Generate raw equation records with stable IDs. + +**Files:** +- `/tmp/SilverSight/data/corpus250_source.jsonl` (new, gitignored) +- `/tmp/SilverSight/python/extract_corpus250_source.py` (new) + +**Specific additions:** + +```python +# Reads Research Stack Semantics/RRC/Corpus250.lean and emits JSONL +def extract_fixture_rows(path: Path) -> list[dict]: + ... +``` + +**Verification:** + +```bash +python3 -m py_compile python/extract_corpus250_source.py +python3 python/extract_corpus250_source.py +python3 -m json.tool data/corpus250_source.jsonl +``` + +**Commit:** + +```text +feat(python): extract Corpus250 source records from Research Stack + +Produces data/corpus250_source.jsonl with stable equation IDs. +``` + +**Claim update:** `silversight_claim_corpus250_source` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 3.2 Build PIST predictions v1 + +**Goal:** Generate `rrc_pist_predictions_250_v1.json` per Research Stack spec. + +**Files:** +- `/tmp/SilverSight/python/build_pist_predictions_250.py` (new or update existing) +- `/tmp/SilverSight/data/rrc_pist_predictions_250_v1.json` (new, gitignored) + +**Specific additions:** + +```python +def build_predictions(records: list[dict]) -> dict: + # Dedup by equation_id + # Deterministic representative selection: min equation_id lexicographically + # matrix_schema = "token_strand_adjacency_8x8_v1" + # matrix_hash = sha256 of canonical row-major JSON +``` + +**Verification:** + +```bash +python3 -m py_compile python/build_pist_predictions_250.py +python3 python/build_pist_predictions_250.py +# Reproducibility check +sha256sum data/rrc_pist_predictions_250_v1.json +python3 python/build_pist_predictions_250.py +diff <(sha256sum data/rrc_pist_predictions_250_v1.json) <(sha256sum data/rrc_pist_predictions_250_v1.json) +``` + +**Commit:** + +```text +feat(python): add PIST predictions v1 builder + +Dedup by invariant id, deterministic representative, reproducible matrix hash. +``` + +**Claim update:** `silversight_claim_pist_predictions_v1` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 3.3 Merge PIST labels into Corpus250 + +**Goal:** Generate `formal/SilverSight/RRC/Corpus250.lean` from JSON. + +**Files:** +- `/tmp/SilverSight/python/build_corpus250.py` (update) +- `/tmp/SilverSight/formal/SilverSight/RRC/Corpus250.lean` + +**Specific additions:** + +```python +def merge_labels(rows: list[dict], predictions: dict) -> list[dict]: + # Populate pistProxyLabel / pistExactLabel when present + # Otherwise leave null +``` + +**Verification:** + +```bash +python3 python/build_corpus250.py +lake build SilverSightRRC +``` + +**Commit:** + +```text +feat(rrc): regenerate Corpus250 from PIST predictions + +Populates labels when predictions exist; leaves missing_prediction otherwise. + +Build: N jobs, 0 errors (lake build SilverSightRRC) +``` + +**Claim update:** `silversight_claim_corpus250_labeled` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 3.4 Implement RrcEmitFixture executable + +**Goal:** Emit the full fixture corpus as AVM-stamped JSON. + +**Files:** +- `/tmp/SilverSight/exe/RrcEmitFixture.lean` + +**Specific additions:** + +```lean +def main : IO Unit := do + let fixtures := SilverSight.RRC.Corpus250.allFixtures + let emitted := fixtures.map (fun row => + match SilverSight.RRC.Emit.determineAlignment row row.pistProxyLabel row.pistExactLabel with + | status => SilverSight.AVMIsa.Emit.emitFixtureRow row status) + IO.println (toJson emitted) +``` + +**Verification:** + +```bash +lake build rrc-emit-fixture +.lake/build/bin/rrc-emit-fixture > /tmp/rrc_fixture_emitted.json +python3 -m json.tool /tmp/rrc_fixture_emitted.json +``` + +**Commit:** + +```text +feat(rrc): implement RrcEmitFixture executable + +Emits AVM-stamped fixture corpus JSON. + +Build: N jobs, 0 errors (lake build rrc-emit-fixture) +``` + +**Claim update:** `silversight_claim_rrc_emit` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 3.5 Validate emitted corpus + +**Goal:** Ensure emitted JSON matches schema and claim boundary. + +**Files:** +- `/tmp/SilverSight/python/validate_rrc_predictions.py` (update) + +**Specific additions:** + +```python +def validate_emitted(path: Path) -> dict: + # schema check + # claim_boundary = "matrix-only;no-classifier;no-lean-spectral" + # proxy_pred / exact_pred null unless labels present + # alignment status consistent with label presence +``` + +**Verification:** + +```bash python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json ``` +**Commit:** + +```text +feat(python): strengthen RRC emitted corpus validator + +Schema, claim-boundary, and alignment consistency checks. +``` + +**Claim update:** `silversight_claim_rrc_validation` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 3.6 Build concept index + +**Goal:** Generate a searchable stable-ID concept map. + +**Files:** +- `/tmp/SilverSight/python/inventory_concepts.py` (new) +- `/tmp/SilverSight/docs/concepts.json` (new) +- `/tmp/SilverSight/docs/concepts.md` (new) + +**Specific additions:** + +```python +def stable_id(kind: str, source_path: str, name: str) -> str: + h = hashlib.sha256(f"{kind}:{source_path}:{name}".encode()).hexdigest()[:12] + return f"silversight_{kind}_{h}_{name}" +``` + +**Verification:** + +```bash +python3 -m py_compile python/inventory_concepts.py +python3 python/inventory_concepts.py +python3 -m json.tool docs/concepts.json +``` + +**Commit:** + +```text +feat(python): add concept inventory generator + +Produces docs/concepts.json and docs/concepts.md with stable IDs. +``` + +**Claim update:** `silversight_claim_concept_index` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 3.7 Add PIST matrix builder tests + +**Goal:** Ensure PIST pipeline is deterministic and label-free in logic. + +**Files:** +- `/tmp/SilverSight/tests/test_pist_matrix_builder.py` (new) +- `/tmp/SilverSight/tests/test_corpus250_build.py` (new) + +**Specific additions:** + +```python +def test_token_strand(): + assert token_strand(0) == 0 + assert token_strand(8) == 0 + assert token_strand(9) == 1 + +def test_build_adjacency(): + tokens = ["a", "b", "c"] + m = build_adjacency_matrix(tokens) + assert sum(m[i][j] for i in range(8) for j in range(8)) == 2 +``` + +**Verification:** + +```bash +python3 -m pytest tests/test_pist_matrix_builder.py tests/test_corpus250_build.py +``` + +**Commit:** + +```text +test(python): add PIST and corpus builder unit tests + +Determinism and raw-feature checks only. +``` + +**Claim update:** `silversight_claim_pist_tests` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 3.8 Phase 3 docs and project map + +**Goal:** Document the corpus and PIST pipeline. + +**Files:** +- `/tmp/SilverSight/docs/ARCHITECTURE.md` +- `/tmp/SilverSight/docs/GLOSSARY.md` +- `/tmp/SilverSight/docs/PROJECT_MAP.{md,json}` +- `/tmp/SilverSight/docs/build_logs/2026-06-21_phase3_completion.md` (new) + +**Verification:** + +```bash +lake build SilverSightRRC +lake build rrc-emit-fixture +python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json +python3 docs/generate_project_map.py +python3 .github/scripts/glossary_lint.py +``` + +**Commit:** + +```text +docs(rrc): document Phase 3 corpus and PIST pipeline + +Updates architecture, glossary, and project map. + +Build: N jobs, 0 errors (lake build SilverSightRRC) +``` + +**Claim update:** Phase 3 documentation claims → `REVIEWED`. + --- ## 8. Phase 4 — Port Mathematical Models -**Goal:** Prove the compression and physics claims that justify SilverSight. +**Phase goal:** Prove the compression and physics claims that justify SilverSight. -### 8.1 Braid / Eigensolid Compression +**Claim target at phase end:** Braid compression theorems at `VERIFIED`; other models documented. -Port the braid dynamics and prove the two compressor theorems: +--- -```text -formal/CoreFormalism/ - BraidEigensolid.lean -- eigensolid_convergence - BraidReceipt.lean -- receipt_invertible -``` +### 4.1 Verify existing eigensolid convergence theorem -**Required theorems:** -- `eigensolid_convergence` — `crossStep` reaches a fixed point. -- `receipt_invertible` — given the receipt, the original state is reconstructible - within bounded error, including gaps/timing/absence. +**Goal:** Confirm `BraidEigensolid.eigensolid_convergence` is in scope and building. -### 8.2 Physics Models (Optional) +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/BraidEigensolid.lean` -Only port physics manifolds if they feed a receipt claim: +**Specific additions:** -- `ManifoldStructures.lean` / `CausalGeometry.lean` / `ExoticSpacetime.lean` -- Migrate to canonical `Semantics.FixedPoint.Q16_16` using the - `PhysicsScalarBridge` pattern. +- Add `#eval` witness with a concrete eigensolid state. +- Add a short doc comment explaining the theorem's exact evaluation model. **Verification:** @@ -312,86 +1484,581 @@ Only port physics manifolds if they feed a receipt claim: lake build SilverSightFormal ``` +**Commit:** + +```text +docs(formal): document eigensolid_convergence evaluation model + +Adds #eval witness and clarifies the theorem's computational interpretation. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_eigensolid_convergence` → `VERIFIED`. + +--- + +### 4.2 Verify existing receipt invertibility theorem + +**Goal:** Confirm `BraidEigensolid.receipt_invertible` is in scope and building. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/BraidEigensolid.lean` + +**Specific additions:** + +- Add `#eval` witness showing two eigensolids with identical receipts have matching residues. +- Document that the theorem covers gaps/timing/absence via `scar_absent` and `write_time`. + +**Verification:** + +```bash +lake build SilverSightFormal +``` + +**Commit:** + +```text +docs(formal): document receipt_invertible coverage + +Adds #eval witness and notes gap/timing/absence dimensions. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_receipt_invertible` → `VERIFIED`. + +--- + +### 4.3 Link BraidReceipt to wire format + +**Goal:** Show that the braid receipt can be serialized with the certified product encoder. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/BraidReceipt.lean` (new) + +**Specific additions:** + +```lean +import CoreFormalism.BraidEigensolid +import CoreFormalism.BraidStateEncoding + +namespace SilverSight.BraidReceipt + +def encodeBraidReceipt (r : BraidReceipt) : ByteArray := ... + +def decodeBraidReceipt (bs : ByteArray) : Option BraidReceipt := ... + +theorem encodeBraidReceipt_size (r : BraidReceipt) : + (encodeBraidReceipt r).size = byteSize BraidReceipt := ... + +theorem encodeBraidReceipt_roundTrip (r : BraidReceipt) : + decodeBraidReceipt (encodeBraidReceipt r) = some r := ... + +-- Wire-level invertibility: equal wire encodings imply equal receipts +theorem receipt_wire_invertible (r1 r2 : BraidReceipt) : + encodeBraidReceipt r1 = encodeBraidReceipt r2 → r1 = r2 := ... + +end SilverSight.BraidReceipt +``` + +**Verification:** + +```bash +lake build SilverSightFormal +``` + +**Commit:** + +```text +feat(formal): add certified BraidReceipt wire encoding + +Links BraidEigensolid receipt to BraidStateEncoding product encoder. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_braid_receipt_wire` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 4.4 Compression benchmark harness + +**Goal:** Collect reproducible compression ratios on a sample corpus. + +**Files:** +- `/tmp/SilverSight/python/compression_benchmark.py` (new) +- `/tmp/SilverSight/data/compression_benchmark_sample/` (new, gitignored) + +**Specific additions:** + +```python +def benchmark_braid(sample_path: Path) -> dict: + # Run braid compressor + # Baseline against zlib, gzip, brotli, zstd + # Report SI ratio original/compressed +``` + +**Verification:** + +```bash +python3 -m py_compile python/compression_benchmark.py +python3 python/compression_benchmark.py --sample data/samples/enwik9_1mb.bin +``` + +**Commit:** + +```text +feat(python): add compression benchmark harness + +Reports SI ratios against standard codecs on a 1 MB sample. +``` + +**Claim update:** `silversight_claim_compression_benchmark` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 4.5 DynamicCanal integration tests + +**Goal:** Show that DynamicCanal regime selection drives layout choice. + +**Files:** +- `/tmp/SilverSight/tests/test_canal_layout.py` (new) + +**Specific additions:** + +```python +def test_layout_for_canal(): + # low pressure → coherent → uses cost model + # high pressure → stressed → compact + # low lambda → throat → columnar +``` + +**Verification:** + +```bash +python3 -m pytest tests/test_canal_layout.py +``` + +**Commit:** + +```text +test(python): add DynamicCanal layout selection tests + +Verifies regime-to-layout mapping matches Core theorems. +``` + +**Claim update:** `silversight_claim_canal_tests` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 4.6 Phase 4 docs and project map + +**Goal:** Document compression verification results. + +**Files:** +- `/tmp/SilverSight/docs/ARCHITECTURE.md` +- `/tmp/SilverSight/docs/GLOSSARY.md` +- `/tmp/SilverSight/docs/PROJECT_MAP.{md,json}` +- `/tmp/SilverSight/docs/build_logs/2026-06-21_phase4_completion.md` (new) + +**Verification:** + +```bash +lake build +python3 docs/generate_project_map.py +python3 .github/scripts/glossary_lint.py +``` + +**Commit:** + +```text +docs(formal): document Phase 4 compression theorems and benchmarks + +Records eigensolid/receipt invertibility status and benchmark method. + +Build: N jobs, 0 errors (lake build) +``` + +**Claim update:** Phase 4 documentation claims → `REVIEWED`. + --- ## 9. Phase 5 — Rewrite Shims -**Goal:** Convert all Python scripts to pure I/O wrappers. +**Phase goal:** Convert all Python scripts to pure I/O wrappers. -### 9.1 Decision-Logic Removal +**Claim target at phase end:** No Python file contains admissibility, cost, or classification logic. -For every Python file in `python/` and `qubo/`: +--- -1. Identify functions that branch on admissibility, cost, or classification. -2. Move the decision to Lean. -3. Replace Python logic with: - - JSON read/write - - subprocess call to `lake exe ` - - result formatting +### 5.1 Shim audit script -### 9.2 New/Updated Shims +**Goal:** Automatically detect decision logic in Python. -```text -python/ - q16_canonical.py # reference implementation (already pure) - sidon_address.py # raw Sidon label generation - pist_matrix_builder.py # raw 8x8 counts - build_corpus250.py # merge only; no alignment logic - validate_rrc_predictions.py # schema check only - emit_review_receipt.py # call Lean emitter, store JSON - inventory_concepts.py # generate concept index -qubo/ - qubo_builder.py # format QUBO matrix; solver call - finsler_metric.py # format metric; no routing decision - qaoa_adapter.py # format adapter inputs +**Files:** +- `/tmp/SilverSight/python/check_for_decision_logic.py` (new) + +**Specific additions:** + +```python +FORBIDDEN_PATTERNS = [ + r"if.*classif", r"if.*admiss", r"if.*cost\s*[<>=]", + r"promotion\s*=\s*['\"]promoted['\"]", + r"def.*decide", +] ``` -### 9.3 Verification +**Verification:** + +```bash +python3 -m py_compile python/check_for_decision_logic.py +python3 python/check_for_decision_logic.py python/ qubo/ +``` + +**Commit:** + +```text +feat(python): add decision-logic audit script + +Flags forbidden patterns in Python shims. +``` + +**Claim update:** `silversight_claim_shim_audit` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 5.2 Refactor pist_matrix_builder to pure I/O + +**Goal:** Remove any classification or decision logic. + +**Files:** +- `/tmp/SilverSight/python/pist_matrix_builder.py` +- `/tmp/SilverSight/python/build_pist_predictions_250.py` + +**Specific additions:** + +- Delete any `if` that changes output based on inferred labels. +- Keep only tokenization, strand assignment, and counting. + +**Verification:** + +```bash +python3 python/check_for_decision_logic.py python/pist_matrix_builder.py +python3 python/build_pist_predictions_250.py +sha256sum data/rrc_pist_predictions_250_v1.json +``` + +**Commit:** + +```text +refactor(python): strip decision logic from PIST builders + +Matrix builders now produce only raw counts and deterministic labels. +``` + +**Claim update:** `silversight_claim_pist_builder_pure_io` → `REVIEWED`. + +--- + +### 5.3 Refactor corpus builder to pure merge + +**Goal:** Ensure `build_corpus250.py` only merges data; no alignment logic. + +**Files:** +- `/tmp/SilverSight/python/build_corpus250.py` + +**Specific additions:** + +- Move alignment status determination entirely into Lean `RRC.Emit`. +- Python only copies `pistProxyLabel` / `pistExactLabel` when present. + +**Verification:** + +```bash +python3 python/check_for_decision_logic.py python/build_corpus250.py +python3 python/build_corpus250.py +lake build SilverSightRRC +``` + +**Commit:** + +```text +refactor(python): make corpus250 builder a pure merge script + +Alignment status is now computed only in Lean. +``` + +**Claim update:** `silversight_claim_corpus_builder_pure_io` → `REVIEWED`. + +--- + +### 5.4 Add LLM review receipt emitter wrapper + +**Goal:** Provide a SilverSight-native way to emit review receipts. + +**Files:** +- `/tmp/SilverSight/python/emit_review_receipt.py` (new) + +**Specific additions:** + +```python +def emit_review(review_text: str, source_files: list[Path]) -> dict: + # Call canonical review emitter or local Ollama endpoint + # Include answer_sha256 + # Return JSON receipt +``` + +**Verification:** + +```bash +python3 -m py_compile python/emit_review_receipt.py +python3 python/emit_review_receipt.py --dry-run docs/ARCHITECTURE.md +``` + +**Commit:** + +```text +feat(python): add review receipt emitter wrapper + +Emits signed review receipts with answer_sha256. +``` + +**Claim update:** `silversight_claim_review_emitter` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 5.5 Delete or move non-I/O scripts + +**Goal:** Remove scripts that cannot become pure I/O. + +**Files:** +- `/tmp/SilverSight/python/chaos_game.py` — move to `formal/CoreFormalism/ChaosGame.lean` or delete. +- `/tmp/SilverSight/python/spectral_profile.py` — keep only feature extraction; move peaks/decisions to Lean. +- `/tmp/SilverSight/python/test_search.py` — keep as tests, ensure no decision logic. + +**Verification:** + +```bash +python3 python/check_for_decision_logic.py python/ +``` + +**Commit:** + +```text +chore(python): remove or relocate decision-bearing scripts + +Chaos game and spectral decisions moved to Lean or deleted. +``` + +**Claim update:** `silversight_claim_shim_cleaned` → `REVIEWED`. + +--- + +### 5.6 Phase 5 docs and project map + +**Goal:** Document the pure-I/O shim contract. + +**Files:** +- `/tmp/SilverSight/AGENTS.md` — add shim contract checklist. +- `/tmp/SilverSight/docs/ARCHITECTURE.md` +- `/tmp/SilverSight/docs/GLOSSARY.md` +- `/tmp/SilverSight/docs/PROJECT_MAP.{md,json}` +- `/tmp/SilverSight/docs/build_logs/2026-06-21_phase5_completion.md` (new) + +**Verification:** ```bash python3 -m py_compile python/*.py qubo/*.py tests/*.py -python3 -m pytest tests/ # if pytest available +python3 python/check_for_decision_logic.py python/ qubo/ +python3 docs/generate_project_map.py +python3 .github/scripts/glossary_lint.py ``` +**Commit:** + +```text +docs(python): document Phase 5 pure-I/O shim contract + +Adds shim audit instructions and updates project map. + +Build: N jobs, 0 errors (py_compile + lint) +``` + +**Claim update:** Phase 5 documentation claims → `REVIEWED`. + --- ## 10. Phase 6 — Hardware Extraction -**Goal:** Generate substrate implementations from Lean and collect hardware -receipts. +**Phase goal:** Generate substrate implementations from Lean and collect hardware receipts. -### 10.1 1-Wire Mapping +**Claim target at phase end:** Verilator simulation receipt present; bonus Tang Nano receipt if hardware available. -Formalize the 1-Wire trit VM in Lean: +--- -```text -formal/CoreFormalism/DynamicCanal/ - LanePayload.lean -- trit VM state - OneWire.lean -- pulse ↔ trit ↔ canal regime mapping +### 6.1 Formalize 1-Wire trit VM + +**Goal:** Map 1-Wire pulses to canal regimes and trit values. + +**Files:** +- `/tmp/SilverSight/formal/CoreFormalism/DynamicCanal/OneWire.lean` (new) + +**Specific additions:** + +```lean +inductive Trit where | neg | zero | pos + +def pulseToTrit (slot : UInt16) (parity : Bool) : Trit := ... + +def tritToRegime (t : Trit) : CanalRegime := ... + +theorem pulse_trit_roundTrip (slot : UInt16) (parity : Bool) : + tritToRegime (pulseToTrit slot parity) = ... := ... ``` -### 10.2 Verilog Extraction +**Verification:** -For combinational circuits derived from Lean `def`s, generate Verilog: - -```text -hardware/ - verilog/ - braid_cross_step.v -- generated from BraidCross.crossStep - q16_add_sat.v -- generated from FixedPoint.add +```bash +lake build SilverSightFormal ``` -**Rule:** Verilog is an extraction target. The authoritative definition remains -in Lean. +**Commit:** -### 10.3 FPGA Receipts +```text +feat(formal): add 1-Wire trit VM mapping -Burn a bitstream and collect a hardware receipt: +Maps pulses to trits and canal regimes. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** `silversight_claim_onewire_trit_vm` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 6.2 Verilog extraction harness + +**Goal:** Generate Verilog from simple combinational Lean `def`s. + +**Files:** +- `/tmp/SilverSight/hardware/verilog/extract_verilog.py` (new) +- `/tmp/SilverSight/hardware/verilog/q16_add_sat.v` (generated) +- `/tmp/SilverSight/hardware/verilog/braid_cross_step.v` (generated) + +**Specific additions:** + +```python +TEMPLATES = { + "q16_add_sat": "module q16_add_sat(input [31:0] a, b, output [31:0] y); ... endmodule", +} +``` + +**Verification:** + +```bash +python3 -m py_compile hardware/verilog/extract_verilog.py +python3 hardware/verilog/extract_verilog.py +iverilog -g2012 hardware/verilog/q16_add_sat.v -o /tmp/q16_add_sat.vvp +``` + +**Commit:** + +```text +feat(hardware): add Verilog extraction harness + +Generates Q16_16 adder and braid cross-step Verilog from Lean specs. +``` + +**Claim update:** `silversight_claim_verilog_extraction` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 6.3 Verilator testbench + +**Goal:** Run generated Verilog in simulation and collect a receipt. + +**Files:** +- `/tmp/SilverSight/hardware/verilog/tb_q16_add_sat.cpp` (new) +- `/tmp/SilverSight/hardware/verilog/Makefile` (new) + +**Specific additions:** + +```cpp +// Test a + b saturation against Lean reference +int main() { ... } +``` + +**Verification:** + +```bash +cd hardware/verilog +make sim +./obj_dir/Vq16_add_sat +``` + +**Commit:** + +```text +test(hardware): add Verilator testbench for q16_add_sat + +Simulation receipt includes cycle counts and output hashes. +``` + +**Claim update:** `silversight_claim_verilator_receipt` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 6.4 FPGA build documentation + +**Goal:** Document how to burn a bitstream and collect a live receipt. + +**Files:** +- `/tmp/SilverSight/hardware/fpga/README.md` (new) +- `/tmp/SilverSight/hardware/fpga/tang_nano_20k/pinout.pcf` (new) +- `/tmp/SilverSight/hardware/fpga/tang_nano_20k/top.v` (new) + +**Specific additions:** + +- Toolchain commands for Yosys/NextPNR/openFPGALoader. +- UART beacon format. +- Bitstream hash computation. + +**Verification:** + +```bash +# Build bitstream (optional, requires hardware) +cd hardware/fpga/tang_nano_20k +make +``` + +**Commit:** + +```text +docs(hardware): add Tang Nano 20K build instructions + +Documents bitstream build, hash, and UART beacon. +``` + +**Claim update:** `silversight_claim_fpga_build_docs` → `REVIEWED`. + +--- + +### 6.5 Hardware receipt schema + +**Goal:** Define the receipt format for hardware verification. + +**Files:** +- `/tmp/SilverSight/hardware/receipt/hardware_receipt_schema.json` (new) +- `/tmp/SilverSight/python/validate_hardware_receipt.py` (new) + +**Specific additions:** ```json { "schema": "hardware_fpga_receipt_v1", "bitstream_hash": "sha256:...", + "source_hash": "sha256:...", "uart_beacon": "...", "continuous_state": "...", "gate": "q16_add_sat", @@ -401,170 +2068,473 @@ Burn a bitstream and collect a hardware receipt: **Verification:** -- Bitstream hash matches generated Verilog source hash. -- UART beacon observed. -- Continuous state verification (not just exit code). +```bash +python3 -m py_compile python/validate_hardware_receipt.py +python3 python/validate_hardware_receipt.py hardware/receipt/sample_receipt.json +``` + +**Commit:** + +```text +feat(hardware): add hardware receipt schema and validator + +Defines FPGA receipt fields and validation rules. +``` + +**Claim update:** `silversight_claim_hardware_receipt_schema` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 6.6 Phase 6 docs and project map + +**Goal:** Document hardware extraction status. + +**Files:** +- `/tmp/SilverSight/docs/ARCHITECTURE.md` +- `/tmp/SilverSight/docs/GLOSSARY.md` +- `/tmp/SilverSight/docs/PROJECT_MAP.{md,json}` +- `/tmp/SilverSight/docs/build_logs/2026-06-21_phase6_completion.md` (new) + +**Verification:** + +```bash +lake build SilverSightFormal +python3 docs/generate_project_map.py +python3 .github/scripts/glossary_lint.py +``` + +**Commit:** + +```text +docs(hardware): document Phase 6 extraction and receipts + +Updates architecture, glossary, and project map. + +Build: N jobs, 0 errors (lake build SilverSightFormal) +``` + +**Claim update:** Phase 6 documentation claims → `REVIEWED`. --- ## 11. Phase 7 — Applications -**Goal:** Wire user-facing tools to the verified core without leaking logic. +**Phase goal:** Wire user-facing tools to the verified core without leaking logic. -### 11.1 CAD Harness +**Claim target at phase end:** Applications produce receipts through Lean gates. -- Text-to-CAD pipeline calls Lean geometry gate. -- Python only formats inputs and renders outputs. +--- -### 11.2 LLM Review Emitter +### 7.1 CAD harness -- `python/emit_review_receipt.py` calls the canonical review emitter. -- Review receipts include `answer_sha256` and are verifiable. +**Goal:** Text-to-CAD pipeline calls Lean geometry gate. -### 11.3 Dashboard +**Files:** +- `/tmp/SilverSight/applications/cad/cad_harness.py` (new) +- `/tmp/SilverSight/formal/SilverSight/CAD/GeometryGate.lean` (new) -- Hermes dashboard displays receipt state, build status, and concept index. -- No decision logic in the dashboard. +**Specific additions:** + +```python +def generate_cad(prompt: str) -> dict: + # Call lake exe cad-geometry-gate + # Return JSON receipt +``` + +**Verification:** + +```bash +lake build cad-geometry-gate +python3 applications/cad/cad_harness.py --prompt "cube" +``` + +**Commit:** + +```text +feat(apps): add CAD geometry gate and harness + +Lean gate validates geometry; Python only formats and renders. +``` + +**Claim update:** `silversight_claim_cad_harness` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 7.2 LLM review dashboard hook + +**Goal:** Display review receipts in Hermes dashboard. + +**Files:** +- `/tmp/SilverSight/applications/dashboard/review_widget.py` (new) + +**Specific additions:** + +- Read `docs/claims/manifest_v1.json` and render status. +- No decision logic. + +**Verification:** + +```bash +python3 -m py_compile applications/dashboard/review_widget.py +``` + +**Commit:** + +```text +feat(apps): add review receipt dashboard widget + +Displays claim-state manifest without logic. +``` + +**Claim update:** `silversight_claim_dashboard_widget` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 7.3 End-to-end smoke test + +**Goal:** Run a full pipeline from equation text to AVM receipt. + +**Files:** +- `/tmp/SilverSight/tests/test_end_to_end.py` (new) + +**Specific additions:** + +```python +def test_equation_to_receipt(): + # Input: equation text + # PIST matrix builder → raw features + # lake exe rrc-emit-fixture → receipt JSON + # Validate receipt schema +``` + +**Verification:** + +```bash +python3 -m pytest tests/test_end_to_end.py +``` + +**Commit:** + +```text +test(apps): add end-to-end pipeline smoke test + +Equation text → PIST features → RRC alignment → AVM receipt. +``` + +**Claim update:** `silversight_claim_e2e_smoke` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 7.4 Phase 7 docs and project map + +**Goal:** Document applications layer. + +**Files:** +- `/tmp/SilverSight/docs/ARCHITECTURE.md` +- `/tmp/SilverSight/docs/GLOSSARY.md` +- `/tmp/SilverSight/docs/PROJECT_MAP.{md,json}` +- `/tmp/SilverSight/docs/build_logs/2026-06-21_phase7_completion.md` (new) + +**Verification:** + +```bash +python3 docs/generate_project_map.py +python3 .github/scripts/glossary_lint.py +``` + +**Commit:** + +```text +docs(apps): document Phase 7 applications + +Updates architecture, glossary, and project map. +``` + +**Claim update:** Phase 7 documentation claims → `REVIEWED`. --- ## 12. Phase 8 — Documentation and Promotion -**Goal:** Produce the final evidence package and promote claims to `VERIFIED`. +**Phase goal:** Produce the final evidence package and promote claims to `VERIFIED`. -### 12.1 Spec Completion +--- -Finalize: +### 8.1 Finalize SilverSight specification -- `6-Documentation/docs/specs/SilverSight_Spec.md` -- `docs/ARCHITECTURE.md` -- `docs/TESTING.md` -- `docs/GLOSSARY.md` +**Goal:** Remove open questions and mark spec as final. -### 12.2 Claim-State Manifest +**Files:** +- `/home/allaun/Research Stack/6-Documentation/docs/specs/SilverSight_Spec.md` -Create a machine-readable manifest: +**Specific additions:** -```text -docs/claims/ - manifest_v1.json -- every claim, current state, evidence URLs - manifest_v1.md -- human-readable summary +- Update status to **Final — SilverSight 1.0**. +- Resolve all open questions with decisions from §3. +- Add §13: Verification Report. + +**Verification:** + +```bash +python3 -m markdownlint 6-Documentation/docs/specs/SilverSight_Spec.md || true ``` -Each entry: +**Commit:** + +```text +docs(specs): finalize SilverSight 1.0 specification + +Resolves open questions and adds verification report section. +``` + +**Claim update:** `silversight_claim_spec_final` → `REVIEWED`. + +--- + +### 8.2 Create claim-state manifest + +**Goal:** Machine-readable record of every claim and its state. + +**Files:** +- `/tmp/SilverSight/docs/claims/manifest_v1.json` (new) +- `/tmp/SilverSight/docs/claims/manifest_v1.md` (new) + +**Specific additions:** ```json { - "claim_id": "silversight_claim_eigensolid_convergence", - "state": "VERIFIED", - "evidence": ["formal/CoreFormalism/BraidEigensolid.lean:theorem eigensolid_convergence"], - "reviewer": "...", - "promoted_at": "..." + "schema": "silver_sight_claim_manifest_v1", + "claims": [ + { + "claim_id": "silversight_claim_product_schema", + "state": "VERIFIED", + "evidence": ["Core/SilverSight/Semantics/ProductSchema.lean"], + "reviewed_by": "ollama_deepseek_review_emitter", + "verified_by": "lake build" + } + ] } ``` -### 12.3 Evidence DAG +**Verification:** -Build a directed acyclic graph of evidence: - -```text -docs/claims/evidence_dag.dot +```bash +python3 -m json.tool docs/claims/manifest_v1.json +python3 python/validate_claim_manifest.py docs/claims/manifest_v1.json ``` -Each node is a theorem, receipt, or review; edges are dependency arrows. - -### 12.4 Final Review - -- Independent review of all `REVIEWED` claims. -- Signed review receipts. -- Promotion to `VERIFIED` only after review. - ---- - -## 13. Verification Gates by Phase - -| Phase | Lean build | Python | Receipt / hardware | Review | -|---|---|---|---|---| -| 1 | `lake build` green | `py_compile` | N/A | Spec review | -| 2 | `lake build SilverSightFormal` green | N/A | N/A | Triage report | -| 3 | `lake build SilverSightRRC` + fixture emit | `validate_rrc_predictions.py` | AVM-stamped JSON | Corpus review | -| 4 | `lake build SilverSightFormal` | N/A | Compression receipts | Theorem review | -| 5 | N/A | `py_compile` + pytest | N/A | Shim audit | -| 6 | Verilog generated | N/A | FPGA receipt | Hardware review | -| 7 | N/A | smoke tests | Review receipts | UX review | -| 8 | N/A | N/A | Claim manifest | Final sign-off | - ---- - -## 14. Continuous Integration - -The existing GitHub workflows must cover the full pipeline: +**Commit:** ```text -.github/workflows/ - lean-check.yml -- lake build on push - python-check.yml -- py_compile + pytest - doc-sync.yml -- glossary lint + check_doc_sync - q16-roundtrip.yml -- Python/C/Lean roundtrip - rrc-emit-check.yml -- emit fixture + validate - hardware-receipt.yml -- check FPGA receipts (manual trigger) +feat(docs): add claim-state manifest v1 + +Machine-readable record of all claims, evidence, and promotion states. +``` + +**Claim update:** `silversight_claim_manifest` → `CALIBRATED_ENGINEERING_DELTA`. + +--- + +### 8.3 Build evidence DAG + +**Goal:** Visualize theorem/receipt dependencies. + +**Files:** +- `/tmp/SilverSight/docs/claims/evidence_dag.dot` (new) +- `/tmp/SilverSight/docs/claims/evidence_dag.svg` (generated) + +**Specific additions:** + +```dot +digraph { + "Schema.lean" -> "ProductSchema.lean"; + "ProductSchema.lean" -> "BraidStateEncoding.lean"; + "BraidStateEncoding.lean" -> "BraidReceipt.lean"; + "BraidEigensolid.lean" -> "eigensolid_convergence"; + "BraidEigensolid.lean" -> "receipt_invertible"; +} +``` + +**Verification:** + +```bash +dot -Tsvg docs/claims/evidence_dag.dot -o docs/claims/evidence_dag.svg +``` + +**Commit:** + +```text +docs(docs): add evidence DAG + +Visual dependency graph of theorems, modules, and receipts. +``` + +**Claim update:** `silversight_claim_evidence_dag` → `REVIEWED`. + +--- + +### 8.4 Collect review receipts + +**Goal:** Emit `REVIEWED` receipts for all claims needing review. + +**Files:** +- `/tmp/SilverSight/receipts/reviewed/*.json` (new) + +**Specific additions:** + +```bash +python3 python/emit_review_receipt.py \ + --files Core/SilverSight/Semantics/*.lean \ + --out receipts/reviewed/core_semantics_review.json +``` + +**Verification:** + +```bash +python3 python/validate_hardware_receipt.py receipts/reviewed/*.json || true +python3 python/validate_rrc_predictions.py receipts/reviewed/*.json || true +``` + +**Commit:** + +```text +docs(receipts): collect Phase 8 review receipts + +Signed review receipts for all reviewed claims. +``` + +**Claim update:** Reviewed claims → `REVIEWED`. + +--- + +### 8.5 Final verification run + +**Goal:** Run the full verification suite before promotion. + +**Files:** +- `/tmp/SilverSight/docs/build_logs/2026-06-21_final_verification.md` (new) + +**Commands:** + +```bash +cd /tmp/SilverSight +lake build +lake build SilverSightCore +lake build SilverSightFormal +lake build SilverSightRRC +lake build rrc-emit-fixture +lake build q16-roundtrip + +.lake/build/bin/rrc-emit-fixture > /tmp/rrc_fixture_emitted.json +python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json + +python3 -m py_compile python/*.py qubo/*.py tests/*.py .github/scripts/*.py applications/*/*.py hardware/verilog/*.py +python3 python/check_for_decision_logic.py python/ qubo/ applications/ +python3 .github/scripts/glossary_lint.py +python3 .github/scripts/check_doc_sync.py +python3 docs/generate_project_map.py + +git diff --cached --check +``` + +**Commit:** + +```text +chore(repo): final verification run for SilverSight 1.0 + +Records full build, test, lint, and secret-check results. + +Build: N jobs, 0 errors (lake build) +``` + +**Claim update:** `silversight_claim_final_verification` → `VERIFIED`. + +--- + +### 8.6 Promote claims to VERIFIED + +**Goal:** Update the manifest with final states and human sign-off. + +**Files:** +- `/tmp/SilverSight/docs/claims/manifest_v1.json` +- `/tmp/SilverSight/docs/claims/manifest_v1.md` + +**Specific additions:** + +- Set all in-scope claims to `VERIFIED`. +- Add `signed_by` field for human reviewer. + +**Verification:** + +```bash +python3 python/validate_claim_manifest.py docs/claims/manifest_v1.json +``` + +**Commit:** + +```text +docs(claims): promote SilverSight 1.0 claims to VERIFIED + +Final claim-state manifest with reviewer provenance. +``` + +**Claim update:** All in-scope claims → `VERIFIED`. + +--- + +## 13. Continuous Integration + +Add or update workflows in `/tmp/SilverSight/.github/workflows/`: + +```text +lean-check.yml -- lake build on push +python-check.yml -- py_compile + pytest +doc-sync.yml -- glossary lint + check_doc_sync +q16-roundtrip.yml -- Python/C/Lean roundtrip +rrc-emit-check.yml -- emit fixture + validate +hardware-receipt.yml -- Verilator simulation (manual trigger) +claim-manifest-check.yml-- validate claim manifest on change ``` --- -## 15. Risks and Mitigations +## 14. Risks and Mitigations | Risk | Mitigation | |---|---| | Research Stack modules have `sorry` | Quarantine; do not block main build. | -| Duplicate `Q16_16` definitions | Unify to `Semantics.FixedPoint.Q16_16`; bridge old code. | -| Python decision logic leaks back | Shim audit checklist; enforce via `python/check_for_decision_logic.py`. | -| Hardware receipts cannot be collected | Document software witness vs. live-hardware distinction; keep claims bounded. | +| Duplicate `Q16_16` definitions | Unify to `SilverSight.FixedPoint.Q16_16`; bridge old code. | +| Python decision logic leaks back | `check_for_decision_logic.py` audit on every commit. | +| Hardware receipts unavailable | Document software witness vs. live-hardware distinction; Verilator as primary target. | | Mathlib version drift | Pin toolchain in `lean-toolchain`; vendor `.lake` if necessary. | | Claim promotion by hand | Manifest is the only promotion authority; manual edits require reviewer signature. | +| Scope creep on physics models | Defer non-braid manifolds to 1.1. | --- -## 16. Open Questions to Resolve Before Execution +## 15. Immediate Next Steps -1. Should the 250-equation corpus be regenerated from Research Stack data or - rewritten for SilverSight? -2. Is AVM rebuilt in Phase 1, or does the existing AVM ISA remain canonical? -3. Which physics modules are required for 1.0 vs. deferred to 1.1? -4. Which FPGA board is the hardware extraction target? -5. Who are the human reviewers for the `REVIEWED` → `VERIFIED` transitions? +If this microstep pipeline is approved, execute the first batch in order: + +1. **1.1** — `ProductSchema.lean` +2. **1.2** — `ProductWireFormat.lean` +3. **1.3** — `ProductLayoutBridge.lean` +4. **1.4** — `BraidStateEncoding.lean` +5. **1.5** — `ProductView.lean` +6. **1.6** — `DynamicCanal/Regime.lean` + +Each step is a separate commit with its own build baseline and claim-state update. --- -## 17. Immediate Next Steps +## 16. Acceptance Criteria for SilverSight 1.0 -If this pipeline is approved, the first executable batch is: - -1. **Phase 1.1** — Implement `ProductSchema.lean`, `ProductWireFormat.lean`, and - `ProductLayoutBridge.lean` with a `BraidState` instance. -2. **Phase 1.2** — Link `CanalLayout.chooseLayout` to - `CoreFormalism.DynamicCanal.classifyRegime`. -3. **Phase 1.3** — Implement `Core/SilverSight/Receipt.lean` and - `Core/SilverSight/Bind.lean`. -4. **Phase 2.1** — Run Research Stack inventory and produce - `docs/research_stack_triage_report.md`. - -Each step is a separate commit with its own build baseline and claim-state -update. - ---- - -## 18. Acceptance Criteria for SilverSight 1.0 - -- `lake build` passes with zero errors across `SilverSightCore`, - `SilverSightFormal`, and `SilverSightRRC`. +- `lake build` passes with zero errors across `SilverSightCore`, `SilverSightFormal`, and `SilverSightRRC`. - No `sorry` in the main import path. - No `Float` in core compute paths. -- All Python shims pass `py_compile` and contain no admissibility logic. +- All Python shims pass `py_compile` and `check_for_decision_logic.py`. - The 250-equation RRC corpus emits AVM-stamped JSON that validates. -- Braid compression has `eigensolid_convergence` and `receipt_invertible` - theorems. -- At least one hardware receipt (FPGA or 1-Wire) is present with bitstream hash - and continuous-state evidence. -- A claim-state manifest exists with every in-scope claim at `VERIFIED`. +- `eigensolid_convergence` and `receipt_invertible` theorems build. +- At least one Verilator simulation receipt (or FPGA receipt) is present with source hash. +- `docs/claims/manifest_v1.json` exists with every in-scope claim at `VERIFIED`. - All documentation is in sync: `glossary_lint.py` and `check_doc_sync.py` pass.