# 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`) --- ## 0. Current State 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` - ✅ `lake build` green: 2987 jobs, 0 errors - ✅ Q16_16 roundtrip proven across Python, C, and Lean - ✅ Repo hygiene scripts active: glossary lint, doc sync, project map generator - ✅ Specification drafted in `6-Documentation/docs/specs/SilverSight_Spec.md` - ⬜ Product-type encoders not yet implemented - ⬜ DynamicCanal physics not linked to layout selection - ⬜ Research Stack theorems not triaged or ported - ⬜ No claim-state manifest exists yet - ⬜ Extraction targets (Python/Rust/Verilog) not generated from Lean 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 --- ## 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 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. --- ## 2. Claim-State Ladder | State | Meaning | Exit gate | |---|---|---| | `BEAUTIFUL_PROVISIONAL` | Intuition captured in a spec or stub. | Spec reviewed; module skeleton compiles. | | `CALIBRATED_ENGINEERING_DELTA` | Implementation exists with `#eval` witnesses or unit tests. | `lake build` / `py_compile` / roundtrip tests pass. | | `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 is recorded only in `docs/claims/manifest_v1.json`. --- ## 3. Provisional Answers to Open Questions | # | 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 extraction / Docs ``` | Phase | Focus | |-------|-------| | 1 | Core Semantics (schema, layout, wireformat, bind, receipt header) | | 2 | Research Stack triage and formal theorem port | | 3 | Search-space corpus and PIST pipeline | | 4 | Mathematical models / compression theorems | | 5 | Python shim rewrite to pure I/O | | 6 | Hardware extraction (Verilog / FPGA receipts) | | 7 | Applications (CAD, dashboard, review emitter) | | 8 | Documentation, claim manifest, promotion | Within a phase, microsteps are ordered. Cross-phase parallelism is allowed only where no file overlap exists. --- ## 5. Phase 1 — Finish Core Semantics **Phase goal:** Make the schema/layout/wireformat stack useful for real structured objects and link it to substrate physics. **Claim target at phase end:** All Phase 1 claims at `CALIBRATED_ENGINEERING_DELTA`; key theorems at `REVIEWED`. --- ### 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 ``` **Verification:** ```bash cd /tmp/SilverSight lake build SilverSightCore ``` **Commit:** ```text feat(core): add product schema instance Adds Schema instance for α × β with byteSize and wellFormed theorems. Build: N jobs, 0 errors (lake build SilverSightCore) ``` **Claim update:** `silversight_claim_product_schema` → `CALIBRATED_ENGINEERING_DELTA`. --- ### 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 (relies on existing `Schema UInt8` and `Schema Bool` instances in `Schema.lean`): ```lean #eval (prodRowMajor WireFormat.uint8RowMajor WireFormat.boolRowMajor).encode (42, true) ``` **Verification:** ```bash lake build SilverSightCore ``` **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 -- Q0_16 remains the default for dimensionless scalars. -- Q16_16 is used here because raw byte addresses and hardware register widths -- require 32-bit integer precision; this is the documented justification. instance : Schema Q16_16 where byteSize := 4 wellFormed := fun _ => true @[simp] theorem q16_16_byteSize : byteSize Q16_16 = 4 := rfl instance : Schema UInt64 where byteSize := 8 wellFormed := fun _ => true @[simp] theorem uint64_byteSize : byteSize UInt64 = 8 := 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 uint64RowMajor : WireFormat UInt64 rowMajor where encode := fun u => ... -- 8 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 #eval byteSize Q16_16 #eval byteSize UInt64 ``` **Commit:** ```text feat(core): add Q16_16, UInt64, and fixed-array wire formats Certified encodings for numeric atoms. Q16_16 justified by byte-address and hardware-register-width requirements; Q0_16 remains default for dimensionless scalars. 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. -- Q16_16 is justified here because phase, residue, and jitter must represent -- values outside [-1, 1] with sub-integer precision, matching the 32-bit -- hardware registers used by the braid dynamics. 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 byteSize BraidState #eval braidStateRowMajor.encode (BraidEigensolid.BraidState.mk ...) theorem braid_state_encode_size (s : BraidState) : (braidStateRowMajor.encode s).size = 392 := by -- Derives from Schema.byteSize BraidState = 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 open SilverSight.FixedPoint.Q16_16 def classifyRegime (pressure lambdaEff : Q16_16) (pStress pThroat : Q16_16) : Regime := if ge pressure pStress then Regime.stressed else if le lambdaEff pThroat then Regime.throat else Regime.coherent theorem classifyRegime_coherent_at_low_pressure (pressure lambdaEff pStress pThroat : Q16_16) (h1 : lt pressure pStress) (h2 : gt 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 -- Explicit layout (sequential, no implicit padding): -- receiptIDHash UInt64 8 -- expressionHash UInt64 8 -- finalState UInt8 1 (HachimojiState encoded as one byte) -- ticCount UInt64 8 -- fuelUsed UInt64 8 -- pathCostRaw UInt32 4 -- verified Bool 1 -- libraryRefCount UInt8 1 -- libraryRefsHash UInt64 8 -- reserved UInt8 1 (padding to 56-byte boundary) -- total = 56 bytes 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 reserved : UInt8 deriving DecidableEq, Repr, BEq instance : Schema HachimojiState where byteSize := 1 wellFormed := fun _ => true instance : Schema ReceiptHeader where byteSize := 56 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 #eval byteSize ReceiptHeader ``` **Commit:** ```text feat(core): add ReceiptHeader schema and wire format Fixed-size 56-byte header for Receipt (explicit field layout); 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 without proof holes. **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, schema-respecting computation (Kleisli arrow). -- Invariants are kept separate so that associativity/identity proofs are -- trivial and require no sorry. def Gate (α β : Type) [Schema α] [Schema β] := α → Option β namespace Gate -- Kleisli composition def bind [Schema α] [Schema β] [Schema γ] (g1 : Gate α β) (g2 : Gate β γ) : Gate α γ := fun a => Option.bind (g1 a) g2 -- Identity gate def id [Schema α] : Gate α α := some -- Invariant certificate, separate from the Gate itself. structure Invariant {α β : Type} [Schema α] [Schema β] (g : Gate α β) (inv : α → β → Prop) where preserves : ∀ a b, g a = some b → inv a b theorem bind_assoc [Schema α] [Schema β] [Schema γ] [Schema δ] (g1 : Gate α β) (g2 : Gate β γ) (g3 : Gate γ δ) : bind (bind g1 g2) g3 = bind g1 (bind g2 g3) := by funext a simp [bind, Option.bind_assoc] theorem bind_id_left [Schema α] [Schema β] (g : Gate α β) : bind (id : Gate α α) g = g := by funext a simp [bind, id] theorem bind_id_right [Schema α] [Schema β] (g : Gate α β) : bind g (id : Gate β β) = g := by funext a simp [bind, id] end Gate end SilverSight.Core ``` **Verification:** ```bash lake build SilverSightCore ``` **Commit:** ```text feat(core): add Gate as Kleisli arrow with separate invariant Lawful bind (associativity, left/right identity) proven without sorry. Invariants are optional certificates, not part of the Gate type. 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 -- In lakefile.lean, add `SilverSight.Bind` to SilverSightCore roots: lean_lib «SilverSightCore» where srcDir := "Core" roots := #[ `SilverSightCore, `SilverSight.FixedPoint, `SilverSight.Receipt, `SilverSight.Bind, `SilverSight.Semantics.Schema, ... ] ``` ```lean -- In Core/SilverSightCore.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 Registers SilverSight.Bind in lakefile and wires ReceiptHeader/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 **Phase goal:** Decide what survives from Research Stack and port it cleanly. **Claim target at phase end:** Foundation modules at `VERIFIED`; quarantined modules documented. --- ### 2.1 Run inventory scripts **Goal:** Produce a machine-readable map of Research Stack concepts and SilverSight candidates. **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) **Specific additions:** ```bash 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 ``` **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 Document Core Gate vs. CoreFormalism Bind boundary **Goal:** Avoid a forced isomorphism between two different bind concepts. **Files:** - `/tmp/SilverSight/docs/ARCHITECTURE.md` - `/tmp/SilverSight/AGENTS.md` **Specific additions:** - State that `Core/SilverSight/Bind.lean` is the minimal Kleisli surface for gate composition. - State that `formal/CoreFormalism/Bind.lean` is a library extension with metric/witness structure. - No required bridge theorem; they serve different layers. If a bridge is later needed, it will be treated as a separate, quarantined proof effort. **Verification:** ```bash lake build SilverSightCore lake build SilverSightFormal ``` **Commit:** ```text docs(formal): document Gate/Bind boundary Clarifies that Core Gate and library Bind are distinct surfaces; no forced isomorphism is required for SilverSight 1.0. Build: N jobs, 0 errors (lake build SilverSightFormal) ``` **Claim update:** `silversight_claim_bind_boundary` → `REVIEWED`. --- ### 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 **Phase goal:** Prove the compression and physics claims that justify SilverSight. **Claim target at phase end:** Braid compression theorems at `VERIFIED`; other models documented. --- ### 4.1 Verify existing eigensolid convergence theorem **Goal:** Confirm `BraidEigensolid.eigensolid_convergence` is in scope and building. **Files:** - `/tmp/SilverSight/formal/CoreFormalism/BraidEigensolid.lean` **Specific additions:** - Add `#eval` witness with a concrete eigensolid state. - Add a short doc comment explaining the theorem's exact evaluation model. **Verification:** ```bash 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/python/generate_sample.py` (new) - `/tmp/SilverSight/data/compression_benchmark_sample/` (new, gitignored) **Specific additions:** ```python # generate_sample.py # Creates reproducible 1 MB and 10 MB samples from: # - Research Stack enwik9 (if available at a configured path) # - Or deterministic pseudorandom bytes seeded by manifest hash SAMPLE_SEED = "silversight_compression_benchmark_v1" def generate_sample(size_bytes: int, out_path: Path) -> Path: ... def benchmark_braid(sample_path: Path) -> dict: # Run braid compressor via lake exe braid-compress # Baseline against zlib, gzip, brotli, zstd # Report SI ratio original/compressed and reproducibility hash ``` **Verification:** ```bash python3 -m py_compile python/compression_benchmark.py python/generate_sample.py python3 python/generate_sample.py --size 1048576 --out data/samples/enwik9_1mb.bin python3 python/compression_benchmark.py --sample data/samples/enwik9_1mb.bin sha256sum data/samples/enwik9_1mb.bin # record in build log ``` **Commit:** ```text feat(python): add compression benchmark harness Reports SI ratios against standard codecs on reproducible 1 MB/10 MB samples. Sample source is Research Stack enwik9 or deterministic seed. ``` **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 **Phase goal:** Convert all Python scripts to pure I/O wrappers. **Claim target at phase end:** No Python file contains admissibility, cost, or classification logic. --- ### 5.1 Shim audit script **Goal:** Automatically detect decision logic in Python. **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", ] ``` **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 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 **Phase goal:** Generate substrate implementations from Lean and collect hardware receipts. **Claim target at phase end:** Verilator simulation receipt present; bonus Tang Nano receipt if hardware available. --- ### 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) = ... := ... ``` **Verification:** ```bash lake build SilverSightFormal ``` **Commit:** ```text feat(formal): add 1-Wire trit VM mapping 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 by static transpilation of proven Lean `def`s. **Files:** - `/tmp/SilverSight/hardware/verilog/extract_verilog.py` (new) - `/tmp/SilverSight/hardware/verilog/lean_to_verilog_map.json` (new) - `/tmp/SilverSight/hardware/verilog/q16_add_sat.v` (generated) - `/tmp/SilverSight/hardware/verilog/braid_cross_step.v` (generated) **Specific additions:** ```json // lean_to_verilog_map.json — static, human-reviewed mapping { "SilverSight.FixedPoint.Q16_16.add": "q16_add_sat.v", "SilverSight.BraidCross.crossSlot": "braid_cross_step.v" } ``` ```python # extract_verilog.py reads the static map and writes the matching template. # It contains no decision logic; the mapping is the source of truth. TEMPLATES = { "q16_add_sat": "module q16_add_sat(input [31:0] a, b, output [31:0] y); ... endmodule", "braid_cross_step": "module braid_cross_step(...); ... endmodule", } def extract(mapping_path: Path, out_dir: Path) -> None: mapping = json.loads(mapping_path.read_text()) for lean_name, template_name in mapping.items(): (out_dir / template_name).write_text(TEMPLATES[template_name]) ``` **Verification:** ```bash python3 -m py_compile hardware/verilog/extract_verilog.py python3 hardware/verilog/extract_verilog.py sha256sum hardware/verilog/*.v iverilog -g2012 hardware/verilog/q16_add_sat.v -o /tmp/q16_add_sat.vvp ``` **Commit:** ```text feat(hardware): add static Verilog transpilation harness Python I/O reads a human-reviewed Lean→Verilog map and writes templates. No decision logic in Python; mapping is the source of truth. ``` **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", "result": "passed" } ``` **Verification:** ```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 **Phase goal:** Wire user-facing tools to the verified core without leaking logic. **Claim target at phase end:** Applications produce receipts through Lean gates. --- ### 7.1 CAD harness **Goal:** Text-to-CAD pipeline calls Lean geometry gate. **Files:** - `/tmp/SilverSight/applications/cad/cad_harness.py` (new) - `/tmp/SilverSight/formal/SilverSight/CAD/GeometryGate.lean` (new) **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 **Phase goal:** Produce the final evidence package and promote claims to `VERIFIED`. --- ### 8.1 Finalize SilverSight specification **Goal:** Remove open questions and mark spec as final. **Files:** - `/home/allaun/Research Stack/6-Documentation/docs/specs/SilverSight_Spec.md` **Specific additions:** - 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 ``` **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 { "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" } ] } ``` **Verification:** ```bash python3 -m json.tool docs/claims/manifest_v1.json python3 python/validate_claim_manifest.py docs/claims/manifest_v1.json ``` **Commit:** ```text 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 ``` --- ## 14. Risks and Mitigations | Risk | Mitigation | |---|---| | Research Stack modules have `sorry` | Quarantine; do not block main build. | | 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. | --- ## 15. Immediate Next Steps If this microstep pipeline is approved, execute the first batch in dependency order: 1. **1.1** — `ProductSchema.lean` 2. **1.2** — `ProductWireFormat.lean` 3. **1.3** — `ProductLayoutBridge.lean` 4. **1.4** — `ProductView.lean` 5. **1.5** — Q16_16 / UInt64 / fixed-array wire formats 6. **1.6** — `BraidStateEncoding.lean` 7. **1.7** — `DynamicCanal/Regime.lean` Each step is a separate commit with its own build baseline and claim-state update. --- ## 16. Acceptance Criteria for SilverSight 1.0 - `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 `check_for_decision_logic.py`. - The 250-equation RRC corpus emits AVM-stamped JSON that validates. - `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.