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/Tdoku16D.lean	Complete (reflexive convergence 336)	0
PIST/UnifiedCovariant.lean	Complete (L1 + L2c: 0 sorries; L3: 7 sorries)	7†
CoreFormalism/ChentsovFinite.lean	Complete (3 axioms)	0
AVMIsa/Types.lean	Complete	0
AVMIsa/Value.lean	Complete	0
AVMIsa/Instr.lean	Complete	0
AVMIsa/State.lean	Complete	0
AVMIsa/Step.lean	Complete	0
AVMIsa/TypeCheck.lean	Complete	0
AVMIsa/TypeSafety.lean	Complete	0
AVMIsa/Run.lean	Complete	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:

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