docs(plans): add SilverSight completion pipeline design

Adds 6-Documentation/docs/plans/SilverSight_completion_pipeline.md, describing the full phase plan from the current core Semantics state to a verified SilverSight 1.0: Core completion, Research Stack triage/port, corpus build, mathematical models, shim rewrite, hardware extraction, applications, documentation, and claim-state promotion.
2026-07-31 03:05:21 +00:00 · 2026-06-21 14:08:05 -05:00 · 2026-06-21 14:08:05 -05:00 · 37d05d1a77
commit 37d05d1a77
parent 7098ee0d64
1 changed files with 570 additions and 0 deletions
--- a/6-Documentation/docs/plans/SilverSight_completion_pipeline.md
+++ b/6-Documentation/docs/plans/SilverSight_completion_pipeline.md
@ -0,0 +1,570 @@
+# SilverSight Completion Pipeline
+
+**Status:** Design draft — to be approved before execution
+
+**Version:** 0.1
+
+**Date:** 2026-06-21
+**Ground truth:** Lean 4 (`/tmp/SilverSight`) + Research Stack documentation (`/home/allaun/Research Stack`)
+
+---
+
+## 1. Current State
+
+The SilverSight core rebas has reached the end of its **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 pipeline describes the shortest safe path from the current state to a
+**completed SilverSight 1.0**: a fully-Lean-grounded system with searchable
+concepts, verified compression receipts, substrate-extractable hardware
+specifications, and promotion-ready documentation.
+
+---
+
+## 2. Design Principles
+
+1. **Lean is the source of truth.** Every decision, cost, gate, and receipt
+   invariant is defined and proved in Lean. Python, Rust, and Verilog are
+   extraction targets only.
+2. **No `sorry` in the main build.** Proof holes live in quarantined modules
+   with a `TODO(lean-port)` ticket and human sign-off.
+3. **No `Float` in compute paths.** `Q0_16` is the default scalar. `Q16_16` is
+   allowed only with a theorem-backed justification.
+4. **Receipts are the compressed state.** A receipt is not metadata; it is the
+   encoding. Invertibility of a receipt is the definition of lossless
+   transformation.
+5. **Promotion is gated.** Claims advance only through the claim-state ladder
+   with reproducible evidence and reviewer provenance.
+6. **Library method.** `Core/` defines contracts; libraries implement them.
+   Libraries never import other libraries.
+
+---
+
+## 3. Claim-State Ladder
+
+Every claim, module, and receipt advances through exactly these states:
+
+| 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 out of `BEAUTIFUL_PROVISIONAL` requires a
+ Lean module or spec section; out of `CALIBRATED_ENGINEERING_DELTA` requires a
+checkable artifact; out of `REVIEWED` requires a reviewer provenance receipt;
+out of `VERIFIED` requires a theorem or live-hardware receipt.
+
+---
+
+## 4. Phase Overview
+
+| Phase | Goal | Deliverable | Build gate |
+|---|---|---|---|
+| 1 | Finish Core Semantics | Product encoders, `DynamicCanal` link, `Receipt`/`Bind` | `lake build SilverSightCore` |
+| 2 | Triage & Port Research Stack | Inventory, keep/delete/transform list, ported theorems | `lake build SilverSightFormal` |
+| 3 | Build Search Space Corpus | Corpus250, PIST matrix builder, concept index | `lake build SilverSightRRC` + fixture emit |
+| 4 | Port Mathematical Models | Braid/eigensolid compression, physics manifolds | `lake build SilverSightFormal` |
+| 5 | Rewrite Shims | Pure-I/O Python scripts, no decision logic | `py_compile` + pytest |
+| 6 | Hardware Extraction | Verilog from Lean, FPGA receipts, 1-Wire mapping | Hardware receipt + bitstream hash |
+| 7 | Applications | CAD harness, LLM review emitter, dashboard wiring | End-to-end smoke tests |
+| 8 | Documentation & Promotion | Specs, claim manifests, evidence DAGs | Review + signed manifest |
+
+---
+
+## 5. Phase 1 — Finish Core Semantics
+
+**Goal:** Make the schema/layout/wireformat stack useful for real structured
+objects and link it to substrate physics.
+
+### 5.1 Product-Type Encodings
+
+Implement certified `WireFormat` and `LayoutBridge` instances for fixed-size
+product types so that braid states, fixture rows, and receipts can be encoded
+without marshalling through JSON.
+
+```text
+Core/SilverSight/Semantics/
+  ProductSchema.lean      -- Schema instance for tuples / structures
+  ProductWireFormat.lean  -- Row-major, columnar, compact encoders
+  ProductLayoutBridge.lean-- rowMajor <-> columnar <-> compact bridges
+```
+
+**Required theorems:**
+- `product_encode_size` — encoded product size equals sum of field sizes.
+- `product_roundTrip` — decode after encode is identity.
+- `bridge_product_correct` — layout bridge preserves product encoding.
+
+**Example target:** `BraidState` (8 strands × fixed fields) encoded to a 64-byte
+row-major `ByteArray`.
+
+### 5.2 DynamicCanal Integration
+
+Move `CanalRegime` from a free-standing enum to a physics-backed decision:
+
+```text
+formal/CoreFormalism/DynamicCanal/
+  Regime.lean       -- CanalRegime + classifyRegime from pressure
+  Lane.lean         -- Lane geometry and λ_eff(P)
+  Timing.lean       -- Timing parameters derived from canal state
+```
+
+**Link:** `CanalLayout.chooseLayout` calls `DynamicCanal.classifyRegime` to
+override the cost-based choice when the substrate is in `stressed` or `throat`.
+
+**Required theorem:** `regime_override_preserves_cost_bound` — a regime override
+never selects a layout more than a documented ε factor worse than the pure cost
+optimum.
+
+### 5.3 Receipt and Bind Core
+
+Implement the receipt type and the `bind` primitive that composes gates:
+
+```text
+Core/SilverSight/
+  Receipt.lean      -- Receipt schema, wellFormed, validation
+  Bind.lean         -- bind : Gate a b -> Gate b c -> Gate a c
+Core/SilverSightCore.lean  -- integrate Receipt and bind into the invariant center
+```
+
+**Required theorems:**
+- `Receipt.wellFormed_decidable`
+- `bind_associative`
+- `bind_identity_left` / `bind_identity_right`
+
+### 5.4 Fixed-Point Completion
+
+Ensure `Q0_16` is the default dimensionless scalar and `Q16_16` is available
+with a documented reason. Remove any remaining `Float` from core compute paths.
+
+**Verification:**
+
+```bash
+lake build SilverSightCore
+lake build SilverSightFormal
+python3 tests/test_q16_roundtrip.py
+.lake/build/bin/q16-roundtrip
+```
+
+---
+
+## 6. Phase 2 — Triage and Port Research Stack Theorems
+
+**Goal:** Decide what survives from Research Stack and port it cleanly.
+
+### 6.1 Inventory
+
+Run the existing inventory scripts to produce a machine-readable map:
+
+```bash
+cd /home/allaun/Research Stack
+python3 scripts/inventory_everything.py              # Postgres + Gremlin + repo
+python3 extraction/generate_porting_candidates.py    # if available
+cd /tmp/SilverSight
+python3 docs/generate_research_stack_usage_map.py    # cross-reference usage
+python3 docs/generate_porting_candidates.py          # produce keep/delete/transform list
+```
+
+**Output:**
+- `extraction/all_concepts_merged.json` (Research Stack)
+- `docs/research_stack_triage_report.md` (SilverSight)
+
+### 6.2 Triage Rules
+
+Apply the spec rules:
+
+| Action | Criterion |
+|---|---|
+| **Keep** | Compiles under `lake build`; has a theorem or `#eval` witness; no `Float` in compute path. |
+| **Delete** | Duplicate `Q16_16`, demo scripts, SaaS integrations, unproven Python decision logic. |
+| **Transform** | Python shims → pure I/O; markdown specs → structured sections; Rust/Verilog → extraction targets. |
+| **Quarantine** | Contains `sorry` or `unsafe` and is not on the critical path; mark `TODO(lean-port)`. |
+
+### 6.3 Port Order
+
+1. Fixed-point and numeric lemmas (`Semantics.FixedPoint` family).
+2. Sidon sets and interaction graphs (`SidonSets.lean`, `InteractionGraphSidon.lean`).
+3. Braid dynamics (`BraidStrand.lean`, `BraidCross.lean`, `BraidEigensolid.lean`).
+4. Sieve lemmas and weak-axis CRT (`SieveLemmas.lean`).
+5. Remaining physics modules only if needed by Phase 4 compression claims.
+
+### 6.4 Module Destination Map
+
+| Research Stack module | SilverSight destination | Notes |
+|---|---|---|
+| `Semantics.FixedPoint.lean` | `Core/SilverSight/FixedPoint.lean` | Already canonical. |
+| `Semantics.SidonSets.lean` | `formal/CoreFormalism/SidonSets.lean` | Keep. |
+| `Semantics.InteractionGraphSidon.lean` | `formal/CoreFormalism/InteractionGraphSidon.lean` | Keep. |
+| `Semantics.SieveLemmas.lean` | `formal/CoreFormalism/SieveLemmas.lean` | Keep. |
+| `Semantics.Braid*.lean` | `formal/CoreFormalism/Braid*.lean` | Keep. |
+| `Semantics.RRC.*.lean` | `formal/SilverSight/RRC/*.lean` | Port selectively. |
+| `Semantics.AVMIsa.*.lean` | `formal/SilverSight/AVMIsa/*.lean` | Already present; reconcile diffs. |
+| `4-Infrastructure/shim/*.py` | `python/` or delete | Strip decision logic. |
+
+### 6.5 Verification
+
+```bash
+lake build SilverSightFormal   # must stay green after each ported module
+lake build SilverSightRRC      # must stay green after RRC ports
+```
+
+---
+
+## 7. Phase 3 — Build Search Space Corpus
+
+**Goal:** Produce the 250-equation corpus and the PIST matrix pipeline so that
+RRC alignment has real inputs.
+
+### 7.1 Corpus250 Builder
+
+Create or port the 250-equation fixture corpus as a pure data module:
+
+```text
+formal/SilverSight/RRC/Corpus250.lean   -- 250 FixtureRow values
+python/pist_matrix_builder.py           -- generate 8x8 strand matrices
+python/build_corpus250.py               -- merge PIST labels into FixtureRows
+```
+
+**Rules:**
+- Equations are raw text; no admissibility logic in Python.
+- `pistProxyLabel` / `pistExactLabel` are populated only when PIST predictions exist.
+- Alignment status remains `missingPrediction` until labels are present.
+
+### 7.2 Concept Index
+
+Generate a searchable concept index:
+
+```text
+python/inventory_concepts.py
+  → docs/concepts.json
+  → docs/concepts.md
+```
+
+Each concept gets a stable ID:
+
+```text
+silversight_<type>_<source_hash>_<name_hash>
+```
+
+### 7.3 RRC Emit Fixture Executable
+
+Ensure `exe/RrcEmitFixture.lean` emits the full corpus as AVM-stamped JSON:
+
+```bash
+lake build rrc-emit-fixture
+.lake/build/bin/rrc-emit-fixture > /tmp/rrc_fixture_emitted.json
+python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json
+```
+
+**Verification:**
+
+```bash
+lake build SilverSightRRC
+lake build rrc-emit-fixture
+python3 -m py_compile python/*.py
+python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json
+```
+
+---
+
+## 8. Phase 4 — Port Mathematical Models
+
+**Goal:** Prove the compression and physics claims that justify SilverSight.
+
+### 8.1 Braid / Eigensolid Compression
+
+Port the braid dynamics and prove the two compressor theorems:
+
+```text
+formal/CoreFormalism/
+  BraidEigensolid.lean      -- eigensolid_convergence
+  BraidReceipt.lean         -- receipt_invertible
+```
+
+**Required theorems:**
+- `eigensolid_convergence` — `crossStep` reaches a fixed point.
+- `receipt_invertible` — given the receipt, the original state is reconstructible
+  within bounded error, including gaps/timing/absence.
+
+### 8.2 Physics Models (Optional)
+
+Only port physics manifolds if they feed a receipt claim:
+
+- `ManifoldStructures.lean` / `CausalGeometry.lean` / `ExoticSpacetime.lean`
+- Migrate to canonical `Semantics.FixedPoint.Q16_16` using the
+  `PhysicsScalarBridge` pattern.
+
+**Verification:**
+
+```bash
+lake build SilverSightFormal
+```
+
+---
+
+## 9. Phase 5 — Rewrite Shims
+
+**Goal:** Convert all Python scripts to pure I/O wrappers.
+
+### 9.1 Decision-Logic Removal
+
+For every Python file in `python/` and `qubo/`:
+
+1. Identify functions that branch on admissibility, cost, or classification.
+2. Move the decision to Lean.
+3. Replace Python logic with:
+   - JSON read/write
+   - subprocess call to `lake exe <gate>`
+   - result formatting
+
+### 9.2 New/Updated Shims
+
+```text
+python/
+  q16_canonical.py              # reference implementation (already pure)
+  sidon_address.py              # raw Sidon label generation
+  pist_matrix_builder.py        # raw 8x8 counts
+  build_corpus250.py            # merge only; no alignment logic
+  validate_rrc_predictions.py   # schema check only
+  emit_review_receipt.py        # call Lean emitter, store JSON
+  inventory_concepts.py         # generate concept index
+qubo/
+  qubo_builder.py               # format QUBO matrix; solver call
+  finsler_metric.py             # format metric; no routing decision
+  qaoa_adapter.py               # format adapter inputs
+```
+
+### 9.3 Verification
+
+```bash
+python3 -m py_compile python/*.py qubo/*.py tests/*.py
+python3 -m pytest tests/          # if pytest available
+```
+
+---
+
+## 10. Phase 6 — Hardware Extraction
+
+**Goal:** Generate substrate implementations from Lean and collect hardware
+receipts.
+
+### 10.1 1-Wire Mapping
+
+Formalize the 1-Wire trit VM in Lean:
+
+```text
+formal/CoreFormalism/DynamicCanal/
+  LanePayload.lean      -- trit VM state
+  OneWire.lean          -- pulse ↔ trit ↔ canal regime mapping
+```
+
+### 10.2 Verilog Extraction
+
+For combinational circuits derived from Lean `def`s, generate Verilog:
+
+```text
+hardware/
+  verilog/
+    braid_cross_step.v    -- generated from BraidCross.crossStep
+    q16_add_sat.v         -- generated from FixedPoint.add
+```
+
+**Rule:** Verilog is an extraction target. The authoritative definition remains
+in Lean.
+
+### 10.3 FPGA Receipts
+
+Burn a bitstream and collect a hardware receipt:
+
+```json
+{
+  "schema": "hardware_fpga_receipt_v1",
+  "bitstream_hash": "sha256:...",
+  "uart_beacon": "...",
+  "continuous_state": "...",
+  "gate": "q16_add_sat",
+  "result": "passed"
+}
+```
+
+**Verification:**
+
+- Bitstream hash matches generated Verilog source hash.
+- UART beacon observed.
+- Continuous state verification (not just exit code).
+
+---
+
+## 11. Phase 7 — Applications
+
+**Goal:** Wire user-facing tools to the verified core without leaking logic.
+
+### 11.1 CAD Harness
+
+- Text-to-CAD pipeline calls Lean geometry gate.
+- Python only formats inputs and renders outputs.
+
+### 11.2 LLM Review Emitter
+
+- `python/emit_review_receipt.py` calls the canonical review emitter.
+- Review receipts include `answer_sha256` and are verifiable.
+
+### 11.3 Dashboard
+
+- Hermes dashboard displays receipt state, build status, and concept index.
+- No decision logic in the dashboard.
+
+---
+
+## 12. Phase 8 — Documentation and Promotion
+
+**Goal:** Produce the final evidence package and promote claims to `VERIFIED`.
+
+### 12.1 Spec Completion
+
+Finalize:
+
+- `6-Documentation/docs/specs/SilverSight_Spec.md`
+- `docs/ARCHITECTURE.md`
+- `docs/TESTING.md`
+- `docs/GLOSSARY.md`
+
+### 12.2 Claim-State Manifest
+
+Create a machine-readable manifest:
+
+```text
+docs/claims/
+  manifest_v1.json       -- every claim, current state, evidence URLs
+  manifest_v1.md         -- human-readable summary
+```
+
+Each entry:
+
+```json
+{
+  "claim_id": "silversight_claim_eigensolid_convergence",
+  "state": "VERIFIED",
+  "evidence": ["formal/CoreFormalism/BraidEigensolid.lean:theorem eigensolid_convergence"],
+  "reviewer": "...",
+  "promoted_at": "..."
+}
+```
+
+### 12.3 Evidence DAG
+
+Build a directed acyclic graph of evidence:
+
+```text
+docs/claims/evidence_dag.dot
+```
+
+Each node is a theorem, receipt, or review; edges are dependency arrows.
+
+### 12.4 Final Review
+
+- Independent review of all `REVIEWED` claims.
+- Signed review receipts.
+- Promotion to `VERIFIED` only after review.
+
+---
+
+## 13. Verification Gates by Phase
+
+| Phase | Lean build | Python | Receipt / hardware | Review |
+|---|---|---|---|---|
+| 1 | `lake build` green | `py_compile` | N/A | Spec review |
+| 2 | `lake build SilverSightFormal` green | N/A | N/A | Triage report |
+| 3 | `lake build SilverSightRRC` + fixture emit | `validate_rrc_predictions.py` | AVM-stamped JSON | Corpus review |
+| 4 | `lake build SilverSightFormal` | N/A | Compression receipts | Theorem review |
+| 5 | N/A | `py_compile` + pytest | N/A | Shim audit |
+| 6 | Verilog generated | N/A | FPGA receipt | Hardware review |
+| 7 | N/A | smoke tests | Review receipts | UX review |
+| 8 | N/A | N/A | Claim manifest | Final sign-off |
+
+---
+
+## 14. Continuous Integration
+
+The existing GitHub workflows must cover the full pipeline:
+
+```text
+.github/workflows/
+  lean-check.yml          -- lake build on push
+  python-check.yml        -- py_compile + pytest
+  doc-sync.yml            -- glossary lint + check_doc_sync
+  q16-roundtrip.yml       -- Python/C/Lean roundtrip
+  rrc-emit-check.yml      -- emit fixture + validate
+  hardware-receipt.yml    -- check FPGA receipts (manual trigger)
+```
+
+---
+
+## 15. Risks and Mitigations
+
+| Risk | Mitigation |
+|---|---|
+| Research Stack modules have `sorry` | Quarantine; do not block main build. |
+| Duplicate `Q16_16` definitions | Unify to `Semantics.FixedPoint.Q16_16`; bridge old code. |
+| Python decision logic leaks back | Shim audit checklist; enforce via `python/check_for_decision_logic.py`. |
+| Hardware receipts cannot be collected | Document software witness vs. live-hardware distinction; keep claims bounded. |
+| 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. |
+
+---
+
+## 16. Open Questions to Resolve Before Execution
+
+1. Should the 250-equation corpus be regenerated from Research Stack data or
+   rewritten for SilverSight?
+2. Is AVM rebuilt in Phase 1, or does the existing AVM ISA remain canonical?
+3. Which physics modules are required for 1.0 vs. deferred to 1.1?
+4. Which FPGA board is the hardware extraction target?
+5. Who are the human reviewers for the `REVIEWED` → `VERIFIED` transitions?
+
+---
+
+## 17. Immediate Next Steps
+
+If this pipeline is approved, the first executable batch is:
+
+1. **Phase 1.1** — Implement `ProductSchema.lean`, `ProductWireFormat.lean`, and
+   `ProductLayoutBridge.lean` with a `BraidState` instance.
+2. **Phase 1.2** — Link `CanalLayout.chooseLayout` to
+   `CoreFormalism.DynamicCanal.classifyRegime`.
+3. **Phase 1.3** — Implement `Core/SilverSight/Receipt.lean` and
+   `Core/SilverSight/Bind.lean`.
+4. **Phase 2.1** — Run Research Stack inventory and produce
+   `docs/research_stack_triage_report.md`.
+
+Each step is a separate commit with its own build baseline and claim-state
+update.
+
+---
+
+## 18. Acceptance Criteria for SilverSight 1.0
+
+- `lake build` passes with zero errors across `SilverSightCore`,
+  `SilverSightFormal`, and `SilverSightRRC`.
+- No `sorry` in the main import path.
+- No `Float` in core compute paths.
+- All Python shims pass `py_compile` and contain no admissibility logic.
+- The 250-equation RRC corpus emits AVM-stamped JSON that validates.
+- Braid compression has `eigensolid_convergence` and `receipt_invertible`
+  theorems.
+- At least one hardware receipt (FPGA or 1-Wire) is present with bitstream hash
+  and continuous-state evidence.
+- A claim-state manifest exists with every in-scope claim at `VERIFIED`.
+- All documentation is in sync: `glossary_lint.py` and `check_doc_sync.py` pass.