mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-06 12:55:47 +00:00
allaun
8ac5ce0c6f
Replaces the spectral-radius operator norm bound (left as TODO(lean-port: operator_norm_bound)) with a computable L_infinity row-sum norm over Fin 8, discharged by dec_trivial. Key changes: - crossingMatrix: Matrix (Fin 8) (Fin 8) Q with explicit Sidon entries - maxRowSum: L_infinity row-sum norm, computed by Finset.sup - crossing_matrix_norm_bound: maxRowSum <= 1775/1792 (dec_trivial) - braid_operator_contractive: ||C*s||_oo <= r * ||s||_oo for r=1775/1792 - Removes deprecated EigensolidConvergenceHypothesis (now a theorem) - Standalone formula doc: docs/reviews/SIDON_ORTHOGONALITY_BYPASS_FORMULA.md - CONJECTURE_UPGRADE_ROADMAP.md updated (conjecture 1 resolved) - BREAKGLASS_LOG.md: entry 2 logged Sidon uniqueness (I4) guarantees at most 2 non-zero entries per row, making the row-sum a concrete rational — no spectral theory required. Build: 3307 jobs, 0 errors (lake build SilverSight)
196 lines
8.2 KiB
Markdown
196 lines
8.2 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.** 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/UnifiedCovariant.lean | Complete (L1–L2: 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 2 (J²=J+I, Sidon crossing matrix, eigensolid
|
||
convergence, Sidon-orthogonality bypass) are complete with 0 sorries.
|
||
|
||
## 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)
|