SilverSight/AGENTS.md

# AGENTS.md — SilverSight

**SilverSight is the clean-slate rebase of the Research Stack.**

## Repository

**GitHub:** `https://github.com/allaunthefox/SilverSight`
**Local clone:** `/home/allaun/SilverSight`
**Formal modules:** `formal/SilverSight/`

## Research Stack

`~/Research\ Stack` is a **read-only archive**. Never write to it. It is the regression oracle — if a closed theorem there covers the same territory as new SilverSight work, the SilverSight proof must recover it as a corollary.

## Rules

1. **SilverSight is the ONLY target for new formal work.** All new Lean code goes here. Do NOT modify `~/Research\ Stack/` under any circumstances.

2. **No cross-imports from Research Stack.** SilverSight depends on Mathlib only. If something from Semantics is needed, port it cleanly.

3. **No `sorry` in committed code.**

4. **No `Float` in compute paths.** Use `Q0_16` or `Q16_16`.

5. **No `native_decide` unless it is the only tactic that closes the goal.** Use `norm_num`, `omega`, `simp`, `decide`, or explicit proof terms first. Document why `native_decide` is required when used. Exception: finitely decidable existence claims (e.g., N=8 necessity) are the canonical use case.

6. **Build gate:** `lake build SilverSight` must pass (0 errors).

7. **Every new module needs:**
   - `@[simp]` theorems for key computations
   - `#eval` witnesses with expected output in comments
   - A docstring explaining the module's purpose

8. **The claim manifest** lives at `6-Documentation/docs/claims/manifest_v1.json`.

## Rotation Protocol (SilverSight ↔ BioSight)

Every work cycle runs three passes in order:

```
1. BioSight scan:
   - Run phi.encode on the active equation batch
   - Collect (τ, δ) distribution from phi.ast_parse
   - Flag any phi.consistency ADMIT/QUARANTINE decision lacking a SilverSight receipt
     → these are rotation triggers: pending SilverSight gates

2. SilverSight pass (triggered by scan):
   - Formalize the flagged gate (≤ 10 lines from existing Schema/WireFormat/Receipt/Bind)
   - lake build must pass
   - Emit receipt JSON

3. BioSight integration:
   - phi.consistency consumes the receipt; decision is now SilverSight-backed
   - Update dag/graph.md node from ⚪ to 🟡/🟢
```

**Archive regression check (every cycle):** If Research Stack has a closed proof covering the same territory as a new gate, BioSight's instance must recover it as a corollary. Failure = framework hole.

## Anti-Drift Multi-Pass

LLM agents drift from the formal spec across sessions. Every decision — no matter how minor — must survive all four passes before it is considered settled:

| Pass | Layer | Authority |
|------|-------|-----------|
| 1 | Python (BioSight phi) | I/O encoding only — no decisions |
| 2 | Lean (SilverSight gate) | Formal authority — closes the decision |
| 3 | RRC pipeline | Cross-repo alignment check |
| 4 | Research Stack oracle | Regression — must recover closed theorems |

**Drift signal:** any Python path making an admissibility or routing decision without a corresponding SilverSight receipt is drift. File it immediately as a pending gate (Pass 2 incomplete).

**Session start protocol:** Before any new formal work, confirm `lake build SilverSight` still passes. Do not trust prior session summaries about build state.

## Root Formal Theorem: N=8 Necessity

The entire BioSight alphabet choice rests on:

```
N = 8 = min { N : Nyquist(N) ∧ Q16_16(N) ∧ DNA-subset(N) }
```

- **Nyquist(N):** N ≥ 2 × max_frequency (antialiasing lower bound)
- **Q16_16(N):** N is a power of 2 (fixed-point arithmetic requirement)
- **DNA-subset(N):** N ≤ 8 (hachimoji alphabet upper bound)

Target: `formal/SilverSight/HachimojiN8.lean` — provable by `native_decide` once the three predicates are defined. This is the root receipt that BioSight's phi.consistency depends on.

## What Belongs Here

- Schema/Layout/WireFormat core (YaFF-inspired)
- Product-type encoders
- Receipt/Bind composition primitive
- DynamicCanal physics (when ported)
- RRC corpus and PIST pipeline (when ported)
- Compression theorems (when ported)

## What Does NOT Belong Here

- Research Stack legacy modules (stay in `Semantics/Semantics/`)
- Python shims (stay in `4-Infrastructure/shim/`)
- Documentation (stay in `6-Documentation/`)
- Extraction JSONs (stay in `extraction/`)

| ID | Research Stack source | SilverSight target | Status |
|----|----------------------|--------------------|--------|
| `nuvmap-port` | `Semantics.InvariantReceipt.Instances.NUVMAP` | `formal/SilverSight/InvariantReceipt/NUVMAP.lean` | ❌ Not started |
| `lambda-threshold` | (no RS source — new theorem) | `formal/SilverSight/PIST/BmcteThreshold.lean` | ❌ Not started |
| `chentsov-core` | (ported) | `ChentsovFinite.lean` | ✅ Complete (3 axioms, 0 sorries) |
| `fisher-rigidity` | (new) | `PIST/FisherRigidity.lean` | ✅ Complete (0 sorries) |

## Current Status

| Module | Status | Sorry |
|--------|--------|-------|
| Schema.lean | Complete | 0 |
| WireFormat.lean | Complete | 0 |
| ProductSchema.lean | Complete | 0 |
| ProductWireFormat.lean | Complete | 0 |
| Receipt.lean | Complete | 0 |
| Bind.lean | Complete | 0 |
| PIST/Spectral.lean | Complete | 0 |
| PIST/FisherRigidity.lean | Complete | 0 |
| PIST/CartanConnection.lean | Complete (NR bracket MC equation) | 0 |
| PIST/YangBaxter.lean | Complete (Layer 2d) | 0 |
| PIST/UnifiedCovariant.lean | Complete (L1 + L2c: 0 sorries; L3: 7 sorries) | 7† |
| CoreFormalism/ChentsovFinite.lean | Complete (3 axioms) | 0 |

† Layer 3 sorries are geometric conjectures (Kähler on ℂℙ⁷, Cartan connection,
  holonomy SO⁰(1,6)) deferred pending Mathlib infrastructure.  Layer 1 (4
  discrete invariants) and Layer 2c (NR bracket MC equation / Yang-Baxter
  integrability) are complete with 0 sorries.

  **Layer 2/2b quarantined** (2026-06-26): goldenEndomorphism, eigensolid_convergence,
  Sidon-orthogonality bypass, and crossingMatrix sections were removed from
  UnifiedCovariant.lean due to incompatible Mathlib 4.30.0-rc2 import paths.
  Their content is preserved in git history and can be revived when Mathlib
  dependency paths stabilize. See git log of UnifiedCovariant.lean.

## CartanConnection — NR Bracket MC Equation (Gate C, Layer 2c)

**Purpose:** Proves d_CE μ = 0 (equivalently [μ,μ]_{NR} = 0) for the Sidon
crossing matrix 2-cochain μ ∈ C²(V,V).  Verified on all 7³ = 343 basis triples
by `native_decide`.  Together with YangBaxter.lean, this closes the breakglass:
`[μ,μ]_{NR}=0 ⇒ YB integrability`.

**Key theorems:**
- `Jacobiator_basis_all` — Finset filter emptiness over 343 triples
- `Jacobiator_basis_zero` — vanishes on any single basis triple

## YangBaxter — Yang-Baxter Integrability (Layer 2d)

**Purpose:** Proves that the 2×2 Sidon crossing block B = [[39/256, 1/7],
[1/7, 39/256]] generates R = B⊗B satisfying R₁₂ R₁₃ R₂₃ = R₂₃ R₁₃ R₁₂.

**Key fact:** Equality holds by alpha-equivalence (r↔s renaming).  No tactic
needed (`rfl`).

## Layer 2 Architecture

```
Layer 1 (DiscreteFoundations):   I₁–I₄ invariants, Sidon uniqueness
Layer 2c (CartanConnection):     NR bracket MC equation [μ,μ]=0          ← HERE
Layer 2d (YangBaxter):           Yang-Baxter integrability               ← HERE
Layer 2b (QUARANTINED):         Eigensolid convergence, matrix norm bound
Layer 2 (QUARANTINED):          Golden endomorphism J²=J+I
Layer 3 (GeometricConjectures):  Kähler on ℂℙ⁷, Cartan connection, holonomy
```

The Sidon crossing matrix has 4 disjoint 2×2 blocks (pairs 0↔1, 2↔3, 4↔5,
6↔7) with cross-block entries zero by Sidon address uniqueness (I₄).  This
block-diagonal structure makes all NR cross terms vanish structurally —
the operadic grafting tree is totally disconnected.

## FisherRigidity — Parabola Focal-Chord to Fisher-Rao Bridge

**Purpose:** Bridges parabola focal-chord perpendicularity (s₁·s₂ = -1) to Fisher-Rao geometric rigidity and Hachimoji eigensolid braid dynamics.

**Key structures:**
- `ConjugatePair` — slope pair encoding perpendicularity
- `isOrthogonal` — Fisher orthogonality vanishing predicate (s₁·s₂ = -1)
- `eigensolidSpectralGapRaw` — 9984 (0.152 normalized), above 1/7 threshold

**Eval witnesses:**
- `parabolaConjugatePair (ofRawInt 65536)` → { slope_large := 158217, slope_small := -27147 }
- `eigensolidSpectralGapRaw` → 9984
- Normalized: 9984/65536 ≈ 0.152 > 1/7 ≈ 0.143 (proven via `spectralGapIntCompare`)

## BMCTE Eigensolid Threshold (p/N = 1/7)

**Result:** λ = exp(-p²/N) → 0 at threshold confirms theoretical prediction

**Implementation:**
1. NUVMAP sparse rollup (`extension_v2_chunked.py`) - saves state per step
2. Spectral witness (`PIST/SpectralWitness.lean`) - computes spectral profile
3. NEON spectral driver (`nuvmap_spectral_driver.py`) - verified 9984 gap value

**Status:**
- λ(eigensolid) = 0 confirmed via formula
- Spectral gap trivially equals input matrix diagonal values (needs parametric sweep)
- TODO(lean-port): NUVMAP module not yet ported to SilverSight

**Files:**
- `experiments/bosonic_continuous/*.json` — receipts
- `formal/SilverSight/PIST/SpectralWitness.lean` — spectral witness
- `experiments/graph_erdos_renyi/*.py` and `*.png` — visualization (note: 1/n ≠ 1/7 thresholds)

## MCP Tools Available

| Tool | Module | Purpose |
|------|--------|---------|
| `gemma-lean-port.find_todo_sorries` | tools-scripts/llm/gemma_lean_port_harness.py | Find TODO(lean-port) theorems |
| `gemma-lean-port.port_theorem` | tools-scripts/llm/gemma_lean_port_harness.py | Generate + validate Lean proofs via Gemma4-12B |
| `loogle-search.loogle_search` | (planned) tools-scripts/mcp/loogle_mcp.py | Search Lean/Mathlib symbols |

## MCP Configuration

Add to `~/.config/opencode/mcp.json`:
```json
{
  "mcpServers": {
    "gemma-lean-port": {
      "command": "python3",
      "args": ["SilverSight/5-Applications/tools-scripts/llm/gemma_lean_port_harness.py"]
    }
  }
}
```

Env vars:
- `GEMMA_URL` — Gemma endpoint (default: http://127.0.0.1:8081/v1/chat/completions)
- `GEMMA_MODEL` — model name (default: gemma4-12b)

## Baker Analogue Integration

The VCN-FAMM-Sidon system is a Baker-style transcendental framework where:
- Sidon addresses = injectivity constraints
- Collapse functional Λ = ∑ wᵢⱼₖₗ log(aᵢ + aⱼ)  
- Scar energy Ω = ∑ scar.pressure
- Theorem: |Λ| ≥ ε(X) ∨ Ω > 0 (rigidity OR scar emission)