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.

⚠️ Ephemeral Build Runner

neon-64gb (100.92.88.64) is an ephemeral build unit with NO permanent access rights. It may vanish mid-session. Never store data, configs, or credentials on it. Never assume it will be reachable. All build dispatch must handle neon failure gracefully — fall back to local or provider-nixos.

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 (all languages). This applies to Rust, Julia, R, Coq, and any other implementation in this repo — not just Lean. Q0_16 or Q16_16 fixed-point arithmetic is the canonical form. Float is permitted ONLY at the external boundary (JSON parsing, sensor data, hardware registers) and ONLY when no practical fixed-point alternative exists. Each float usage must:

   • Be bracketed: of_float / to_float calls at the module boundary, never in the core loop
   • Be documented in the commit message explaining why Q16_16 couldn't work
   • Be cross-validated by at least one other language port that uses pure 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.

Fraction Construction Rules

The SilverSight FixedPoint module provides Q16_16 fixed-point arithmetic. Use only these canonical constructors:

1. Use canonical constructors only

   Q16_16.ofNat n      -- for integers
   Q16_16.ofRatio a b  -- for rational numbers
   Q16_16.ofRawInt x   -- for already-scaled integers
   

2. Never use ofFloat in compute paths

   • Allowed only at external boundary (JSON parsing, sensor input)
   • Must be immediately bracketed: ofFloat x |> toFixedPoint |> compute

3. Bridge pattern for legacy code (Research Stack migration path)

   import Semantics.PhysicsScalarBridge
   -- Use PhysicsScalarBridge.add, .gt, etc.
   -- Constants: PhysicsScalarBridge.one, .two, .three, .half, .quarter
   

Fraction Comparison Pattern

-- WRONG: direct comparison with Float
if x > 0.5 then ...

-- RIGHT: fixed-point comparison
if x > Q16_16.half then ...

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
CoreFormalism/CRTSidon.lean	Complete (CRT Torus preserves Sidon under vecAdd)	0
CoreFormalism/StrandCapacityBound.lean	Trivial (	F(A)
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
CacheSieve.lean	Complete (2026-07-05 maintenance: evictVictim inline fix)	0
Blitter6502OISC.lean	Complete (2026-07-05: execSUBLEQ inline fix)	0
BlockCoprimeDensity.lean	Complete (C(n) Euler product, saturation partition, C(0)=1)	0
ColdReviewer.lean	Complete (2026-07-05: dec_trivial → native_decide)	0
GoldenSpiral.lean	Complete (2026-07-05: MulLeftMono → induction)	0
PIST/CharPoly.lean	Complete (2026-07-05: Horner Newton 3-bug fix)	0
PIST/CMYKColoringCore.lean	Complete (2026-07-05: decodeColoring roundtrip)	0
PIST/SidonAdapter.lean	Complete (2026-07-05: Nat.find → iterative loop)	0
PIST/WeightCandidateGen.lean	Complete (2026-07-05: fuel termination)	0
PIST/UnitDistCandidateGen.lean	Complete (2026-07-05: fuel termination, n≥3)	0
PIST/ManifoldShortcut.lean	Complete (2026-07-05: Unicode→line comments)	0
Rollup.lean	Complete (circulant-block compression theorem, totalCrossingMultCost=8)	0
YangMillsPerformance.lean	Complete (2026-07-05: compression_overhead_bounded → Rollup.totalCrossingMultCost)	0
ChiralClockModel.lean	Stub (copied from experimental, 4 sorries from experimental)	4

† 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

Gauge Theory Research Program

Gauge theory is the most rigorous framework for mapping out math because it forces explicit distinctions between theorems, conjectures, and empirical observations. Use it as a probe, not as a claim.

What Gauge Theory Demands

1. Proven vs Conjectural

   • If you claim a correspondence, you must prove it or label it an ansatz
   • Empirical correlations (r=0.41, r=-0.33, n=13, p>0.05) are data, not theorems
   • Gauge theory requires: "Is this a theorem or an ansatz?"

2. Dimensional Honesty

   • AT model is 2D; gauge confinement requires 3+1D (or 2+1D for compact U(1))
   • Confinement in 2D gauge theory is trivial — this is a theorem
   • Dimensional mismatches must be explicitly addressed, not papered over

3. Category/Type Correctness

   • Frustration is boolean/Z₂
   • Wilson loop is real-valued (trace of holonomy)
   • Curvature is Lie-algebra-valued
   • Confusing these categories is a type error

What Gauge Theory Does NOT Give You

1. Derivation for Free — The Baker-Hopf coupling is an ansatz, not derived from gauge principles
2. Uniqueness — Other connections (arctan, Li₂, etc.) could satisfy similar constraints
3. Predictive Power — Correlations computed because the hypothesis suggested them

Success Criteria

Success is NOT "SilverSight IS gauge theory."

Success IS: "We attempted to derive SilverSight structures from gauge theory. We succeeded for X, failed for Y, and learned Z."

Specifically:

• Attempt derivation for Baker-Hopf coupling — proves it's gauge-theoretic or reveals it's something else
• Attempt derivation for frustration = Wilson loop — proves the correspondence or reveals it's just a correlation
• Attempt derivation for Baker Λ = field strength — proves the formal resemblance or reveals it's just a resemblance

Failure Mode

Failure is NOT "correspondences don't hold."

Failure IS: "We didn't attempt the derivation, so we don't know what the structures actually are."

Recommended Framing

Use gauge theory as a research program:

"We investigate whether SilverSight can be derived from lattice gauge theory.
We have proven X, observed Y empirically, and conjecture Z.
Here are the falsification criteria."

Never claim:

"SilverSight IS gauge theory"

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	✅ Active (check_determinism.py)
1: Cross-validation	Single-LLM blind spots	Multi-model Lean	🔶 Not wired (scripts/cross_validate.py exists but requires manual invocation)
2: Mutation testing	Verifier that passes bad proofs	scripts/qc-flag/	🔶 Not wired (generator + mutations exist but runner is manual)
3: CAS/SMT grounding	Vacuous/tautological proofs	SymPy	✅ Active (verify_with_sympy.py in entry gate)
4: Build + emission	Compilation errors, receipt validity	lake build + verify_receipt.py	✅ Active (CI + entry gate)
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)

Cross-Domain Signature Mining

The miner at infra/sigs/rydberg_miner.py searches arXiv + CORE API for 1/n-scaling residual papers across 5 domains (Rydberg, superconductor, energy storage, EM, epigenetic). The pipeline works end-to-end: paper search → keyword filter → signature extraction → significance test.

Current status: Pipeline is functional but numerical signature values are hash-derived placeholders (the miner finds real papers but can't extract actual measurements from abstracts alone).

To make it scientifically valid: Wire an LLM extraction step that reads each paper's full text and extracts real numerical values (quantum defects, H*/Hc2 ratios, breakdown fields, etc.). This is a standalone tool that takes the paper list from the miner and produces genuine signature values. Relevant papers are identified and stored with DOIs for easy lookup.

Files:

• infra/sigs/rydberg_miner.py — arXiv + CORE search → paper dedup → keyword filter → signature generation
• scripts/cross_domain_significance.py — statistical significance test (≥6σ)
• signatures/cross_domain_signatures.json — extracted signatures
• signatures/cross_domain_significance.json — per-phase σ levels

Build Infrastructure

neon-64gb — Ephemeral Build Runner ⚠️

neon-64gb has NO permanent access rights. It is an ARM64 compilation worker that may be taken offline at any time without notice. All build dispatch must handle failure gracefully — if neon is unreachable, fall back to local build or provider-nixos immediately.

Property	Value
Hostname	neon-64gb (Tailscale 100.92.88.64)
CPU	18-core ARM64
RAM	64 GiB
Role	Ephemeral lake build runner & Postgres host
SSH	ssh allaun@100.92.88.64
Access guarantee	None. May disappear without notice.
Persistent data	None. Assume any data on it is lost.

For build dispatchers: If lake build on neon fails or times out, build locally on qfox-1 or remotely on provider-nixos. Never block on neon.

For LLM agents: Do not assume neon persists between sessions. Do not store configs, credentials, or artifacts on it. Treat it as a throwaway builder.

provider-nixos (neon-rs1000) — Migration Target

Property	Value
Hostname	v2202606349345477168.happysrv.de / 100.79.14.103
CPU	4 vCPUs (AMD EPYC 9645)
RAM	8192 MiB
Disk	256 GiB (HDD)
OS	Debian 13 (Trixie)
Role	FreeLLMAPI, OpenCode server, lean-copilot, Postgres
Status	Active — lake build, Postgres, scripts
SSH	ssh root@159.195.136.129 (config: ~/.ssh/config.d/projectserver)

Host mapping

Service	Primary	Fallback
lake build (ARM64)	neon-64gb (ephemeral)	qfox-1 / provider-nixos
lake build (AMD64)	provider-nixos	qfox-1
LLM inference	qfox-1 (Qwen, RTX 4070)	FreeLLMAPI → any provider
FreeLLMAPI proxy	provider-nixos	—
k3s cluster	cupfox	—
Public reverse proxy	racknerd (Caddy)	—