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/CrossDomainSynthesis.lean	Complete (Rydberg defect & SC band)	0
PIST/MultiSurfacePacker.lean	Complete (Lagrangian decision logic)	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
RRC/Emit.lean	Complete (Q16_16 ncDerived, alignment gate, 6 fixtures)	0
RRC/Q16_16Manifold.lean	Complete (278 rows, Q16_16 manifold fields)	0
RRC/ReceiptDensity.lean	Complete	0
RRCLogogramProjection.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)

ncDerived Architecture (2026-06-29)

Negative Control Witness

CSV axioms (ncObserved, residualRisk, scaleBandDeclared, weakAxesNames)
    │
    ▼
ncDerived = Q16_16.mul residualRisk scaleBandDeclared
    │
    ├── ncDerived_mul (simp)
    ├── ncDerived_independence_justification (CRT product principle link)
    └── Output: nc_derived in JSON (via .toFloat at I/O boundary)

Q16_16 Values (Fixture Corpus)

Row	residualRisk	scaleBandDeclared	ncDerived (raw)	ncDerived (float)
Clf/Ssrc	47/100	2/5	12320	0.187988
Stamp_Code	11/25	1/5	5766	0.087982
Weak control	27/50	1/5	7077	0.107986

FFS Physical Analog (Pending Validation)

• arXiv:2602.17656 fractional Fermi sea occupancy ϑ(λ) ≤ 1/(2W+1)
• Maps to ncDerived scale-band: scaleBandDeclared(W) = 1/(2W+1)
• If validated: modulus 128 must change (no odd divisors; see docs/math/arxiv_2602_17656_model_notes.md)
• Validation: KS test of ncDerived vs 1/(2W+1) quantization (Step 5, Milestone 7b)

Files Ported (Research Stack → SilverSight)

File	Status	Notes
formal/SilverSight/RRC/Emit.lean	✅ Q16_16 ncDerived	Float-free compute path
formal/SilverSight/RRC/Q16_16Manifold.lean	✅ 278 rows	Q16_16 manifold fields
python/build_manifold.py	✅ Q16_16 emission	lean_q16_16() helper

Beyond Rigorous — Anti-Smuggle Protocol

LLMs produce coherent-looking outputs that are subtly wrong in non-obvious ways. Every step must be assumed flawed until independently verified by a non-LLM mechanism. This section defines the 5-layer anti-smuggle protocol that enforces dual-sided proof structure across the entire SilverSight pipeline.

Layer 0: Deterministic Reproducibility Chain

Every artifact must be independently reproducible from source. Non-determinism is the primary vector for smuggled assumptions [5].

Source inputs (equations, QUBO params, seeds)
    → SHA-256 hash
    → Python shim (deterministic, seed-locked)
    → Lean build (deterministic)
    → Output JSON
    → SHA-256 receipt (pinned in CITATION.cff)

Independent re-run on different hardware must produce identical hash chain.
If not → non-determinism detected → assumption smuggling possible.

Enforcement:

• All Python shims must accept --seed parameter (default 0)
• All random number generators must be seeded explicitly
• Lean #eval outputs must be cached and hashed
• Receipt JSON includes content_sha256 field for all generated artifacts

Layer 1: Multi-Model Cross-Validation

No single LLM output stream is trusted. Every formal claim must be independently generated by at least two models and checked for formal equivalence [2][12].

LLM A → generates Lean theorem
LLM B → generates Lean theorem (same problem, blind)
    ↓
Lean compiler verifies both independently
    ↓
Formal equivalence checker confirms both prove same statement
    ↓
If one passes and the other fails → BOTH are suspect

Enforcement:

• Critical theorems (Chentsov, FSR, ncDerived) must have dual provenance
• Cross-validation receipt records both source models + Lean build hash
• Surface-form similarity is NOT equivalence — Lean proofs can be cosmetically identical while logically different

Layer 2: Adversarial Mutation Testing

The verifier itself must be tested. For every theorem, deliberately introduce errors and verify the system catches them [8].

# Mutation suite for every theorem in the build surface
mutations/
  Emit.lean/
    001_flip_ncDerived_mul.lean    # expected: FAIL
    002_swap_residual_scale.lean   # expected: FAIL
    003_zero_ncObserved.lean       # expected: FAIL
    004_float_instead_of_q16.lean  # expected: FAIL

Enforcement:

• python3 scripts/qc-flag/ must pass on clean build AND fail on each mutation
• Mutation coverage = #mutations_that_cause_build_failure / #total_mutations
• If a mutation passes the build → the theorem is not specific enough

Layer 3: Symbolic Oracle Grounding (CAS/SMT)

Lean proofs can be vacuously true or circular. Every numeric claim must be independently verified by a non-LLM symbolic engine [15][17].

Lean computes:
    ncDerived = Q16_16.mul (Q16_16.ofRatio 47 100) (Q16_16.ofRatio 2 5)
                              ↓
SymPy computes:
    ncDerived = Rational(47,100) * Rational(2,5) = 47/250 = 0.188
                              ↓
Z3 checks:
    Assert(lean_output == sympy_output ± epsilon)

Enforcement:

• All Q16_16.ofRatio values must have a corresponding SymPy Rational verification
• All native_decide blocks must have a Z3 SMT-LIB2 equivalent
• CAS verification receipt stored alongside Lean receipt

Layer 4: Dual-Sided Proof Structure (Domain-Specific)

For the Hachimoji/QUBO pipeline, the quantum encoding must be verified against a classical ground truth. This is the "clear-box middleware" architecture.

Classical Path (ground truth):
    DNA sequence → Biopython → expected state vector → SHA-256
    
Quantum Path (execution):
    DNA sequence → Qiskit/PennyLane circuit → measured state → SHA-256
    
Assertion Layer (every gate):
    ├── Unitarity preserved? (‖U†U - I‖ < ε)
    ├── Probability distribution consistent with DNA input?
    └── State vector fidelity ≥ threshold?
    
Cross-Validation:
    ├── Classical expected == Quantum measured (within noise)
    ├── If mismatch → LogicViolation exception → data quarantined
    └── Log: every state transformation serialized to JSONL for audit

Enforcement:

• Every circuit gate has an assertion wrapper checking unitarity
• Every measurement logs: {timestamp, gate, input_state, output_state, fidelity}
• Third-party observer can reconstruct exact state at any time t from logs alone
• Full audit trail = "traceable proof"

Layer 5: Claim-State Ladder with Non-LLM Gate

Every claim in the system must occupy one of these states. Promotion requires non-LLM evidence at every rung.

State	Requirement	LLM Role	Non-LLM Gate
BEAUTIFUL_PROVISIONAL	Coherent hypothesis	Primary author	None
CALIBRATED_ENGINEERING_DELTA	CAS/SMT verification	Provide code	SymPy/Z3 check
REVIEWED	Multi-model cross-validation	Dual provenance	Lean compiler
VERIFIED	Full reproducibility + adversarial tests	Audited	Mutation suite + hash chain

Rule: No claim may promote from PROVISIONAL to DELTA without a non-LLM symbolic verification. No claim may promote to VERIFIED without a passing mutation suite.

Entry Gate for Every Commit

Before any formal work is accepted:

1. Deterministic check:    python3 scripts/check_determinism.py  # seed-locked, hash-verified
2. Cross-validation:       python3 scripts/cross_validate.py     # dual LLM provenance check
3. Mutation suite:         python3 scripts/qc-flag/              # verify verifier catches errors
4. CAS grounding:          python3 scripts/verify_with_sympy.py  # numeric ground truth
5. Build gate:             lake build SilverSight                # Lean compiler

All five must pass. If any fails, the commit is quarantined and flagged for human review.

Summary Table

Layer	What It Prevents	Tool	Current Status
0: Determinism	Non-reproducible artifacts	SHA-256, seed-lock	⚠️ Partial (corpus hashes exist)
1: Cross-validation	Single-LLM blind spots	Multi-model Lean	❌ Missing
2: Mutation testing	Verifier that passes bad proofs	scripts/qc-flag/	❌ Missing
3: CAS/SMT grounding	Vacuous/tautological proofs	SymPy, Z3	❌ Missing
4: Dual-sided proof	Smuggled quantum assumptions	PennyLane, Biopython	⚠️ Partial (QUBO exists)
5: Claim-state ladder	Unvalidated promotion	Review protocol	⚠️ Partial (AGENTS.md framework)

Post-Stability Refinements

These refinements should be incorporated after the core braid/eigensolid formalization is stable. They are cross-references and experimental testbeds — not blockers.

Turkel et al. TTG — Braid Topology in Twisted Trilayer Graphene

Turkel et al., Science 376, 193 (2022), DOI: 10.1126/science.abk1895. Supplementary materials at: supplementary/Turkel2022_TTG_SOM.pdf (externally sourced)

What it demonstrates: A physical system (3-layer graphene, two independent twist angles θTM, θBM) that undergoes a Moiré Lattice Reconstruction (MLR) producing exactly three discrete topological defect classes — plaquettes, solitons, and twistons — organized in a honeycomb network at the moiré-of-moiré scale Λ. This is a braid-word structure in a real material.

Mapping to our formalism:

TTG physical quantity	Our braid formalism
θTM, θBM (twist angles)	BraidStateN 3 inter-strand crossing parameters
MLR → AtA domains (no AtB)	Eigensolid convergence: crossStep(s) = s
Λ = a/δθ (moiré of moiré)	Sidon slack / braid word period
Plaquette (1.45°) / soliton (1.54°) / twiston (1.68°)	Scar types: stable / soliton / topological defect
GSFE energy functional (Eq. S4)	Q16_16 crossing energy (Φ_couch_to_fourier)
Relaxation displacement u_ℓ (Eq. S2)	Strand jitter + residue fields
Flat band resonance at ν~±2.4	∅_scars (scar absence → FAMM gate pass)
Disorder reduction at resonance doping	Eigensolid fixed point → uniform LDOS
Hartree-Fock correction (4 meV → 19 meV width)	Crossing energy renormalization (many-body → Q16_16)
Heterostrain ε_x on solitons (C3 breaking)	Braid word defect: non-trivial braid group element

Key insight for formalization: The MLR does not distribute twist-angle error as random noise — it bifurcates into discrete topological classes. This is exactly what a braid representation (Artin B_n) predicts: twist mismatch is absorbed as a word in the braid group, not as a continuous random field. The triple-domain structure is a braid word with exactly 3 defect letters.

When to apply:

• After BraidStateN.lean and SpectralN.lean are stable and proven
• As a test case for n=3 (current work fixes n=8; TTG provides a natural n=3 physical instance)
• The GSFE parameterization (Eq. S4) can be ported as a specific instance of our generalized stacking-fault energy functional
• The Hartree-Fock vs single-particle comparison validates our requirement for interaction-aware crossing energy (no single-particle model reproduces the 19 meV VHS width correctly)