Research-Stack/6-Documentation/docs/plans/SilverSight_completion_pipeline.md

# 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): <ticket>` 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.