mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
- CRTSidon.lean: full proof of sidon_preserved_mod (matches Python CRT-reconstructed mod-M check). Uses Bezout via Nat.gcdA/Nat.gcdB for CRT injectivity. 0 sorries. - BraidEigensolid.lean/GoldenSpiral.lean: fix golden centering constant (40560->40504, 0.14% relative error) - AGENTS.md: flag StrandCapacityBound triviality, add CRTSidon status - CITATION.cff: add Elsasser(1946) toroidal/poloidal prior art - SLOS receipt: add classical-simulation disclaimer - sidon_preservation_creation.md: mark creation theorem unformalized - autoresearch: containerized via runpod/autoresearch base image (silver-autoproof:latest), systemd service created - LeanCopilotFill.lean: updated for new CRTSidon API Build: 3297 jobs, 0 errors (lake build CoreFormalism.CRTSidon)
510 lines
24 KiB
Markdown
510 lines
24 KiB
Markdown
# 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 (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.
|
||
|
||
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)| ≤ min(|A|, L₁·L₂) — cardinality only, no Sidon info) | 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`:
|
||
```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].
|
||
|
||
```bash
|
||
# 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:
|
||
|
||
```bash
|
||
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
|
||
|
||
## ProjectServer (2026-06-30)
|
||
|
||
New x86_64 server for eventual pod migration from neon-64gb.
|
||
|
||
| Property | Value |
|
||
|----------|-------|
|
||
| Hostname | `v2202606349345477168.happysrv.de` |
|
||
| IP | `159.195.136.129` |
|
||
| SSH | `ssh root@159.195.136.129` |
|
||
| CPU | 4 vCPUs (AMD EPYC 9645, AMD64 — good for compilation) |
|
||
| RAM | 8192 MiB |
|
||
| Disk | 256 GiB (HDD) |
|
||
| OS | Debian 13 (Trixie) |
|
||
| Role | Eventual migration target for neon pods |
|
||
| Status | Bare OS — no Docker/Podman yet |
|
||
| SSH config | `~/.ssh/config.d/projectserver` |
|
||
|