allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/6-Documentation/docs/plans/SilverSight_completion_pipeline.md
allaun 4dd0c18759 docs(plans): address review conditions on completion pipeline 
- Reorders Phase 1 next steps to dependency order.
- Adds Q16_16 / UInt64 justification notes and explicit ReceiptHeader
  56-byte layout with #eval witness.
- Redesigns Core Gate.bind as a Kleisli arrow with separate Invariant
  certificate to avoid proof holes.
- Registers SilverSight.Bind in lakefile.lean integration step.
- Removes forced Core Gate ↔ CoreFormalism Bind bridge; documents boundary.
- Clarifies Verilog extraction as static, reviewed Lean→template mapping.
- Specifies compression benchmark sample source and reproducibility.
- Fixes fixed-point comparison operators in classifyRegime.
- Adds phase/focus table to dependency graph.

Build: docs only; no Lean/Python changes
2026-06-22 01:11:17 -05:00

68 KiB
Raw Permalink Blame History

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

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:

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:

cd /tmp/SilverSight
lake build SilverSightCore

Commit:

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:

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):

#eval (prodRowMajor WireFormat.uint8RowMajor WireFormat.boolRowMajor).encode (42, true)

Verification:

lake build SilverSightCore

Commit:

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:

-- 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:

lake build SilverSightCore

Commit:

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:

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:

lake build SilverSightCore

Commit:

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:

-- 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

-- 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:

lake build SilverSightCore
#eval byteSize Q16_16
#eval byteSize UInt64

Commit:

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:

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:

lake build SilverSightFormal

Commit:

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:

-- 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:

lake build SilverSightFormal

Commit:

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:

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:

lake build SilverSightFormal

Commit:

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:

-- 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:

lake build SilverSightCore
#eval byteSize ReceiptHeader

Commit:

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:

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:

lake build SilverSightCore

Commit:

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:

-- 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,
    ...
  ]

-- 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:

lake build SilverSightCore
lake build

Commit:

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:
cd /tmp/SilverSight
python3 docs/generate_project_map.py
python3 .github/scripts/glossary_lint.py
python3 .github/scripts/check_doc_sync.py

Verification:

lake build
python3 -m py_compile python/*.py .github/scripts/*.py

Commit:

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:

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:

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:

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:

python3 -m py_compile python/triage_module.py
python3 python/triage_module.py
python3 -m json.tool docs/triage_manifest.json

Commit:

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:

-- formal/CoreFormalism/FixedPoint.lean becomes a re-export shim
import SilverSight.FixedPoint
export SilverSight.FixedPoint (Q16_16 Q0_16)

Verification:

lake build SilverSightFormal
lake build SilverSightRRC

Commit:

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:

lake build SilverSightFormal

Commit:

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:

lake build SilverSightRRC
lake build rrc-emit-fixture

Commit:

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:

-- 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

-- PIST/Classify.lean
def classifyMatrix (m : Fin 8 → Fin 8 → Nat) : Option PISTLabel := ...

-- PIST/Matrices250.lean
def matrices : List (String × Fin 8 → Fin 8 → Nat) := ...

Verification:

lake build SilverSightRRC

Commit:

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:

lake build
# Confirm no sorry in main build
grep -R "sorry" Core/SilverSight/ formal/CoreFormalism/ formal/SilverSight/ || true

Commit:

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:

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:

lake build SilverSightCore
lake build SilverSightFormal

Commit:

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:

lake build
python3 docs/generate_project_map.py
python3 .github/scripts/glossary_lint.py
python3 .github/scripts/check_doc_sync.py

Commit:

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:

# Reads Research Stack Semantics/RRC/Corpus250.lean and emits JSONL
def extract_fixture_rows(path: Path) -> list[dict]:
    ...

Verification:

python3 -m py_compile python/extract_corpus250_source.py
python3 python/extract_corpus250_source.py
python3 -m json.tool data/corpus250_source.jsonl

Commit:

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:

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:

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:

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:

def merge_labels(rows: list[dict], predictions: dict) -> list[dict]:
    # Populate pistProxyLabel / pistExactLabel when present
    # Otherwise leave null

Verification:

python3 python/build_corpus250.py
lake build SilverSightRRC

Commit:

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:

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:

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:

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:

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:

python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json

Commit:

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:

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:

python3 -m py_compile python/inventory_concepts.py
python3 python/inventory_concepts.py
python3 -m json.tool docs/concepts.json

Commit:

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:

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:

python3 -m pytest tests/test_pist_matrix_builder.py tests/test_corpus250_build.py

Commit:

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:

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:

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:

lake build SilverSightFormal

Commit:

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:

lake build SilverSightFormal

Commit:

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:

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:

lake build SilverSightFormal

Commit:

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:

# 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:

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:

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:

def test_layout_for_canal():
    # low pressure → coherent → uses cost model
    # high pressure → stressed → compact
    # low lambda → throat → columnar

Verification:

python3 -m pytest tests/test_canal_layout.py

Commit:

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:

lake build
python3 docs/generate_project_map.py
python3 .github/scripts/glossary_lint.py

Commit:

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:

FORBIDDEN_PATTERNS = [
    r"if.*classif", r"if.*admiss", r"if.*cost\s*[<>=]",
    r"promotion\s*=\s*['\"]promoted['\"]",
    r"def.*decide",
]

Verification:

python3 -m py_compile python/check_for_decision_logic.py
python3 python/check_for_decision_logic.py python/ qubo/

Commit:

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:

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:

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:

python3 python/check_for_decision_logic.py python/build_corpus250.py
python3 python/build_corpus250.py
lake build SilverSightRRC

Commit:

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:

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:

python3 -m py_compile python/emit_review_receipt.py
python3 python/emit_review_receipt.py --dry-run docs/ARCHITECTURE.md

Commit:

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:

python3 python/check_for_decision_logic.py python/

Commit:

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:

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:

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:

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:

lake build SilverSightFormal

Commit:

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 defs.

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:

// 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"
}

# 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:

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:

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:

// Test a + b saturation against Lean reference
int main() { ... }

Verification:

cd hardware/verilog
make sim
./obj_dir/Vq16_add_sat

Commit:

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:

# Build bitstream (optional, requires hardware)
cd hardware/fpga/tang_nano_20k
make

Commit:

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:

{
  "schema": "hardware_fpga_receipt_v1",
  "bitstream_hash": "sha256:...",
  "source_hash": "sha256:...",
  "uart_beacon": "...",
  "continuous_state": "...",
  "gate": "q16_add_sat",
  "result": "passed"
}

Verification:

python3 -m py_compile python/validate_hardware_receipt.py
python3 python/validate_hardware_receipt.py hardware/receipt/sample_receipt.json

Commit:

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:

lake build SilverSightFormal
python3 docs/generate_project_map.py
python3 .github/scripts/glossary_lint.py

Commit:

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:

def generate_cad(prompt: str) -> dict:
    # Call lake exe cad-geometry-gate
    # Return JSON receipt

Verification:

lake build cad-geometry-gate
python3 applications/cad/cad_harness.py --prompt "cube"

Commit:

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:

python3 -m py_compile applications/dashboard/review_widget.py

Commit:

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:

def test_equation_to_receipt():
    # Input: equation text
    # PIST matrix builder → raw features
    # lake exe rrc-emit-fixture → receipt JSON
    # Validate receipt schema

Verification:

python3 -m pytest tests/test_end_to_end.py

Commit:

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:

python3 docs/generate_project_map.py
python3 .github/scripts/glossary_lint.py

Commit:

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:

python3 -m markdownlint 6-Documentation/docs/specs/SilverSight_Spec.md || true

Commit:

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:

{
  "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:

python3 -m json.tool docs/claims/manifest_v1.json
python3 python/validate_claim_manifest.py docs/claims/manifest_v1.json

Commit:

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:

digraph {
  "Schema.lean" -> "ProductSchema.lean";
  "ProductSchema.lean" -> "BraidStateEncoding.lean";
  "BraidStateEncoding.lean" -> "BraidReceipt.lean";
  "BraidEigensolid.lean" -> "eigensolid_convergence";
  "BraidEigensolid.lean" -> "receipt_invertible";
}

Verification:

dot -Tsvg docs/claims/evidence_dag.dot -o docs/claims/evidence_dag.svg

Commit:

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:

python3 python/emit_review_receipt.py \
  --files Core/SilverSight/Semantics/*.lean \
  --out receipts/reviewed/core_semantics_review.json

Verification:

python3 python/validate_hardware_receipt.py receipts/reviewed/*.json || true
python3 python/validate_rrc_predictions.py receipts/reviewed/*.json || true

Commit:

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:

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:

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:

python3 python/validate_claim_manifest.py docs/claims/manifest_v1.json

Commit:

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/:

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.