mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00

allaun 1a26de076d fix(lean): address vacuous rfl proofs in Chentsov theorem and close Hermite sieve proofs

- ChentsovFinite.lean: Replaced vacuous rfl proofs at uniform distribution permutation invariance, diagonal case, and off-diagonal case with explicit proof obligations and sorry.
- section2_hermite_sieve.lean: Proved repunit strict monotonicity and lower bound lemmas, closing relevant sorry placeholders.
- BindingSiteEntropy.lean: Swapped geodesicDistance placeholder with fisherRaoApprox and added counterexample sketch for fisher_implies_similar_druggability.
- FixedPoint.lean, lakefile.lean, gemma4_mcp.py: Minor fixes and enhancements.
- AGENTS.md: Tracked open Chentsov proof obligations.

Build: 2987 jobs, 0 errors (lake build)

2026-06-23 05:11:04 -05:00

5.1 KiB

Raw Blame History

AGENTS.md — SilverSight

SilverSight is the clean-slate rebase of the Research Stack.

Repository

GitHub: https://github.com/allaunthefox/SilverSight Local clone: /tmp/SilverSight (or wherever you clone it) Formal modules: formal/SilverSight/

Location (in Research Stack — for lake build integration)

0-Core-Formalism/lean/SilverSight/
  SilverSight/
    Schema.lean
    WireFormat.lean
    ProductSchema.lean
    ProductWireFormat.lean
    Receipt.lean
    Bind.lean
  SilverSight.lean          ← root import

Rules

SilverSight is the ONLY target for new formal work. Do NOT add new modules to 0-Core-Formalism/lean/Semantics/Semantics/. All new Lean code goes to the SilverSight repository.
Imports from Semantics are allowed (cross-project): import Semantics.FixedPoint, import Semantics.Spectrum, etc.
No sorry in committed code. Same rule as the Research Stack.
No Float in compute paths. Use Q0_16 or Q16_16.
Build gate: lake build SilverSight must pass (3307 jobs, 0 errors as of 2026-06-22).
Every new module needs:
- @[simp] theorems for key computations
- #eval witnesses with expected output in comments
- A docstring explaining the module's purpose
The claim manifest lives at 6-Documentation/docs/claims/manifest_v1.json (shared with Research Stack docs).

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-h9`	`ChentsovFinite.lean:~608`	same file — `h9` in `hc_pos`	⚠️ `sorry`; closable via `h_perm (Equiv.swap 1 2)` + `simp`; est. ~20 lines
`chentsov-diagonal`	`ChentsovFinite.lean:~836`	same file — diagonal `h_agree`	⚠️ `sorry`; needs Steps A–E: `h_inv` at `splitIdx=i` → `IsFunctionalEquation` → `functional_eq_unique` → `c_val/p_i`; est. ~100 lines
`chentsov-offdiag`	`ChentsovFinite.lean:~862`	same file — off-diagonal `h_agree`	⚠️ `sorry`; needs Steps A–C: `h_inv` at `splitIdx=0` → functional eq for cross term → `c_val/p_0`; est. ~80 lines

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

BMCTE Eigensolid Threshold (p/N = 1/7)

Result: λ = exp(-p²/N) → 0 at threshold confirms theoretical prediction

Implementation:

NUVMAP sparse rollup (extension_v2_chunked.py) - saves state per step
Spectral witness (PIST/SpectralWitness.lean) - computes spectral profile
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)

5.1 KiB Raw Blame History Unescape Escape