allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-30 17:16:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(core): harden SilverSightCore and port canonical FixedPoint

Browse source 
- Remove Float from Core/SilverSightCore.lean (Receipt.pathCost is now Option Nat)
- Prove TIC theorems tic_never_decreases and computation_generates_time
- Add lakefile.lean, lean-toolchain, and .gitignore for .lake/
- Port Research-Stack Semantics.FixedPoint.lean to formal/CoreFormalism/FixedPoint.lean
- Delete thin Q16_16_Spec.lean; update Python/QUBO comments and docs
- Create AGENTS.md distilled from Research Stack core bindings
- Update REBASE_RULES.md to strip legacy hacks and reference AGENTS.md

Build: 2978 jobs, 0 errors (lake build)
This commit is contained in:
allaun 2026-06-21 06:30:12 -05:00
parent 1ce4093041
commit 7a973a06f6
14 changed files with 1834 additions and 336 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -9,3 +9,4 @@ __pycache__/
.mcp/
env/
venv/
.lake/

274
AGENTS.md Normal file
View file

@ -0,0 +1,274 @@
# AGENTS.md — SilverSight Operating Contract
**Principle:** *Port the contracts and the rituals, not the state.*
This file distills the surviving rules from Research Stack and rebases them onto
SilverSight's library-method architecture. Legacy deployment details, stale
benchmark tables, and repo-specific paths have been stripped. The conceptual
bindings — Lean authority, no-Float compute, receipt boundaries, and the
post-interaction ritual — remain in force.
---
## 1. Project Architecture
SilverSight is organized as a minimal invariant core plus independent libraries.
```
Core/
SilverSightCore.lean ← no imports, no Float, no library code
formal/
CoreFormalism/ ← Q16_16, Hachimoji, Chentsov, Sidon
PVGS_DQ_Bridge/ ← quantum bridge
UniversalEncoding/ ← math address space
BindingSite/ ← biological binding sketches
python/ ← I/O, feature extraction, orchestration
qubo/ ← optimization libraries
tests/ ← verification fixtures
docs/ ← architecture and placement docs
```
### Library method
- **Core defines the contract.** Libraries implement it.
- `Core/SilverSightCore.lean` imports nothing and depends on nothing.
- Every library may import `Core/` but may **not** import another library.
- The `Receipt` is the only interface between Core and libraries.
---
## 2. The No-Float Law
**No `Float` in Lean compute paths.** This is non-negotiable.
- Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofRawInt` for all core
arithmetic.
- `ofFloat` is permitted **only** at external boundaries (JSON parsing, sensor
input) and must be immediately bracketed/converted.
- `Float` is forbidden in `Core/` entirely. `Receipt.pathCost` is an `Option Nat`
(raw fixed-point integer), not `Option Float`.
- The canonical fixed-point implementation is
`formal/CoreFormalism/FixedPoint.lean`, ported from Research Stack
`Semantics.FixedPoint.lean` with boundary conversions removed from compute
paths.
---
## 3. Programming Choice Flow
Before writing or placing any new logic, run through this decision tree in order.
Stop at the first rule that applies.
```
New logic needed?
│
├── Does it make an admissibility, routing, alignment, or gating decision?
│ └── YES → Write it in Lean. No Python equivalent allowed.
│ File: formal/CoreFormalism/*.lean or a new formal/*.lean module.
│
├── Does it mint, stamp, or emit a top-level receipt or JSON bundle?
│ └── YES → It belongs in Core receipt validators or the designated emitter.
│ Python may format/store, but Lean stamps the decision.
│
├── Does it classify rows, run an alignment gate, or compute scores?
│ └── YES → Lean. Python may call it via #eval / lake exe but may not
│ replicate the logic.
│
├── Does it supply raw input features (expression text, route_hint, domain_type,
│ equation_id hashing, weak_axes count)?
│ └── YES → Python shim is acceptable. The shim must:
│ (a) produce only a raw data structure
│ (b) carry no admissibility logic
│ (c) be regenerable from source
│ (d) live in python/ or qubo/ with a TODO(lean-port) if the logic
│ could eventually move to Lean
│
├── Does it use floating-point arithmetic in a compute path?
│ └── YES → STOP. Use Q16_16.ofNat / Q16_16.ofRatio / Q16_16.ofRawInt.
│
├── Does it advance promotion status (e.g. set promotion = "promoted")?
│ └── YES → STOP. Promotion is always not_promoted until a Lean gate
│ explicitly passes. Never advance it in shim space or by hand.
│
└── Is it pure I/O (read JSON, write JSONL, call subprocess, format output)?
└── YES → Python shim is fine. Keep it in python/ or qubo/.
```
**Summary:** Lean owns all decisions. Python owns all I/O.
---
## 4. Receipt Contract
The `Receipt` is the compressed interface record. It is not metadata around a
result; it **is** the result.
```lean
structure Receipt where
receiptID : String
expression : String
finalState : HachimojiState
ticCount : Nat
fuelUsed : Nat
pathCost : Option Nat -- raw integer cost; never Float
libraryRefs : List String
verified : Bool
```
- Libraries produce receipts. The core consumes them.
- A receipt proves only the gate it actually checks.
- Receipt validation lives in `Core/SilverSightCore.lean`.
---
## 5. AVM and TIC Axiom
The Abstract Virtual Machine (AVM) is a stack machine defined in Core.
- `δ : AVMState × Instruction → AVMState` is the sole transition function.
- **TIC axiom:** TIC is derived from events, never the driver.
- `T_{n+1} = T_n + E(S_n)` where `E ≥ 0`
- `δ` never decreases TIC.
- Meaningful computation (`finalState ≠ Ζ`) implies `ticCount > 0`.
---
## 6. Verification Expectations
- For Lean changes, run the narrow target first, then `lake build` when feasible.
- For Python shims, run `python3 -m py_compile` on touched files.
- For JSON receipts, run `python3 -m json.tool`.
- Before committing, run `git diff --cached --check` and scan touched files for
secrets.
---
## 7. Post-Interaction Workflow (mandatory)
After any code, Lean, shim, receipt, or architecture change:
1. **Update the nearest scoped AGENTS.md.**
- Root or multi-subtree changes → this file.
- `Core/` changes → `Core/AGENTS.md` if one exists, otherwise this file.
- `formal/` changes → `formal/AGENTS.md` if one exists, otherwise this file.
2. **Verify the build.**
- Lean: `lake build` from the appropriate `lakefile.lean` root.
- Python: `python3 -m py_compile` on touched files.
3. **Commit.**
- Stage only explicitly touched files. **Never `git add .`.**
- Commit format:
```
<type>(<scope>): <summary>
<body — what changed and why>
Build: <N> jobs, 0 errors (lake build)
```
- Types: `feat`, `fix`, `chore`, `docs`, `refactor`.
- Scopes: `core`, `formal`, `python`, `qubo`, `docs`, `infra`.
4. **Check tree cleanliness.**
```bash
git status --branch --short --untracked-files=all
```
Untracked files that are not generated artifacts must be staged or noted as
intentionally dirty.
---
## 8. Do Not Sweep
Never run broad cleanup commands:
```bash
git add .
git checkout -- .
git clean -fdx
```
Use explicit file lists. Generated artifacts and research scratch should stay
out of Git unless they are themselves the evidence under review.
---
## 9. Git Remote Hygiene
- The active branch may not have an upstream. Inspect with
`git rev-parse --abbrev-ref --symbolic-full-name @{u}` before assuming push
state.
- Prefer the `github` remote and verify the remote head after push:
```bash
git fetch github <branch>
git rev-list --left-right --count FETCH_HEAD...HEAD
git push -u github <branch>
git ls-remote --heads github <branch>
```
---
## 10. Secrets
Secrets are runtime-only. Use environment variables (`OLLAMA_API_KEY`,
`DEEPSEEK_API_KEY`, etc.). Never paste, print, or commit literal provider keys.
---
## 11. Legacy Recovery Trigger
The phrase **`RECOVER LEGACY INFORMATION`** is the explicit retrieval trigger
for archived or quarantined concepts.
Accepted forms:
```text
RECOVER LEGACY INFORMATION: <path, commit, concept, or artifact>
Recover Legacy Information: <path, commit, concept, or artifact>
recover from cornfield: <path, commit, concept, or artifact>
```
Rules:
- Inspect the requested legacy source with read-only commands first.
- Recover only the named file, concept, commit slice, or receipt.
- Modernize the recovered material onto the current clean branch.
- Never merge, reset to, or base new work on a legacy branch unless explicitly
asked.
- Preserve the legacy branch as retrievable archive state.
Current Research Stack cornfield ref (for cross-repo lookup only):
`backup/distilled-with-vcd-history-2026-05-11`.
---
## 12. Glossary
- **Hachimoji state** — one of Φ, Λ, Ρ, Κ, Ω, Σ, Π, Ζ. The 8-state output
alphabet of the core classifier.
- **Receipt** — the machine-readable attestation record that crosses the
Core/library boundary.
- **AVM** — Abstract Virtual Machine. The stack-machine semantics defined in
`Core/SilverSightCore.lean`.
- **TIC** — Temporal Index of Computation. A monotone event counter derived from
state transitions.
- **Q16_16** — Canonical 32-bit fixed-point type (`formal/CoreFormalism/FixedPoint.lean`).
- **Library method** — Core defines contracts; libraries implement them; no
library imports another library.
- **Sidon label** — an address from a set with unique pairwise sums. Powers of
2 are canonical for 8 strands.
- **BraidStorm** — the 8-strand braid topology used in eigensolid compression.
- **eigensolid** — converged stable state of a braid crossing loop; detected
when `crossStep(s) = s`.
- **promotion** — status advance from `not_promoted` to `promoted` only after a
Lean gate passes.
---
## 13. SilverSight-Specific Boundaries
- `Core/SilverSightCore.lean` is the root authority. It contains no sorries in
the active surface.
- `formal/CoreFormalism/FixedPoint.lean` is the canonical Q16_16 source of
truth.
- The `python/` and `qubo/` directories are I/O and optimization shims only;
they may not contain admissibility logic.
- Research artifacts and scratch output should live outside the git tree unless
promoted as durable receipts.

110
Core/SilverSightCore.lean
View file

@ -29,6 +29,10 @@
License: MIT
-/
import Mathlib.Data.Fintype.Basic
import Mathlib.Tactic.DeriveFintype
import Mathlib.Tactic
namespace SilverSight.Core
-- =============================================================================
@ -50,12 +54,12 @@ namespace SilverSight.Core
-/
inductive HachimojiState
| Φ | Λ | Ρ | Κ | Ω | Σ | Π | Ζ
| Φ | Λ | Ρ | Κ | Ω | «Σ» | «Π» | Ζ
deriving DecidableEq, Repr, Fintype, BEq
def HachimojiState.toString : HachimojiState → String
| .Φ => "Φ" | .Λ => "Λ" | .Ρ => "Ρ" | .Κ => "Κ"
| .Ω => "Ω" | .Σ => "Σ" | .Π => "Π" | .Ζ => "Ζ"
| .Ω => "Ω" | .«Σ» => "Σ" | .«Π» => "Π" | .Ζ => "Ζ"
instance : ToString HachimojiState := ⟨HachimojiState.toString⟩
@ -83,10 +87,10 @@ structure Receipt where
finalState : HachimojiState
ticCount : Nat
fuelUsed : Nat
pathCost : Option Float
pathCost : Option Nat -- raw integer cost metric (Q16_16 raw value or 0); never Float
libraryRefs : List String
verified : Bool
deriving Repr, BEq
deriving DecidableEq, Repr, BEq
-- Empty receipt (no classification performed)
def Receipt.empty : Receipt :=
@ -141,7 +145,7 @@ structure AVMState where
fuel : Nat -- remaining fuel
tic : Nat -- current TIC count
history : List Instruction -- executed instructions
deriving Repr
deriving Repr, BEq
def AVMState.initial (fuel : Nat) : AVMState :=
{ stack := [], fuel := fuel, tic := 0, history := [] }
@ -212,17 +216,41 @@ lemma tic_monotone (T : Nat) (events : Nat) :
ticUpdate T events ≥ T := by
simp [ticUpdate]
-- The TIC axiom: TIC never decreases
theorem tic_never_decreases (program : List Instruction) (fuel : Nat) :
(runAVM program fuel).tic ≥ (AVMState.initial fuel).tic := by
simp [runAVM, AVMState.initial]
-- TIC starts at 0 and only increases
induction program with
-- δ never decreases TIC. When fuel > 0, it strictly increases TIC.
lemma δ_tic_monotone (s : AVMState) (i : Instruction) :
(δ s i).tic ≥ s.tic := by
simp [δ]
split_ifs with h_fuel
· -- fuel = 0: δ appends Halt and changes nothing else
simp
· -- fuel > 0: δ decrements fuel, increments tic, records instruction
cases i <;> simp
all_goals omega
-- foldl preserves the TIC lower bound
lemma foldl_tic_monotone (s : AVMState) (program : List Instruction) :
(List.foldl δ s program).tic ≥ s.tic := by
induction program generalizing s with
| nil => simp
| cons i rest ih =>
simp [List.foldl]
-- Each instruction increments TIC by at least 1
sorry -- Proof: δ always increments tic by at least 1
have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i
have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic := ih (δ s i)
exact Nat.le_trans h_step h_rest
-- The TIC axiom: TIC never decreases
theorem tic_never_decreases (program : List Instruction) (fuel : Nat) :
(runAVM program fuel).tic ≥ (AVMState.initial fuel).tic := by
simp [runAVM]
-- Invariant: foldl preserves tic ≥ starting tic
generalize AVMState.initial fuel = s
induction program generalizing s with
| nil => simp
| cons i rest ih =>
simp [List.foldl]
have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i
have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic := ih (δ s i)
exact Nat.le_trans h_step h_rest
-- =============================================================================
-- §5. LOOP INVARIANT (computation generates time)
@ -237,13 +265,61 @@ theorem tic_never_decreases (program : List Instruction) (fuel : Nat) :
(where time is measured in events, not seconds).
-/
-- If the final TIC equals the starting TIC, the stack never changed.
lemma foldl_tic_eq_start (s : AVMState) (program : List Instruction)
(h : (List.foldl δ s program).tic = s.tic) :
(List.foldl δ s program).stack = s.stack := by
induction program generalizing s with
| nil =>
simp at h ⊢
| cons i rest ih =>
simp [List.foldl] at h ⊢
have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i
have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic :=
foldl_tic_monotone (δ s i) rest
have h_eq : (δ s i).tic = s.tic := by linarith
have h_fuel0 : s.fuel = 0 := by
by_contra h_fuel
have hf : s.fuel > 0 := by omega
have h_ne : s.fuel ≠ 0 := by omega
have h_strict : (δ s i).tic > s.tic := by
simp [δ, h_ne]
cases i <;> simp
linarith
have h_stack : (δ s i).stack = s.stack := by simp [δ, h_fuel0]
have h_fuel : (δ s i).fuel = s.fuel := by simp [δ, h_fuel0]
have h_tic : (δ s i).tic = s.tic := h_eq
have h_final_eq : (List.foldl δ (δ s i) rest).tic = (δ s i).tic := by linarith
have h_final_stack : (List.foldl δ (δ s i) rest).stack = (δ s i).stack :=
ih (δ s i) h_final_eq
rw [h_stack] at h_final_stack
exact h_final_stack
-- Corollary: if the starting TIC is 0 and the final TIC is 0, the stack is empty.
lemma runAVM_tic_zero_stack_empty (program : List Instruction) (fuel : Nat)
(h : (runAVM program fuel).tic = 0) :
(runAVM program fuel).stack = [] := by
simp [runAVM] at h ⊢
have h_eq : (List.foldl δ (AVMState.initial fuel) program).tic = (AVMState.initial fuel).tic := by
simp [AVMState.initial] at h ⊢
linarith
have h_stack : (List.foldl δ (AVMState.initial fuel) program).stack = (AVMState.initial fuel).stack :=
foldl_tic_eq_start (AVMState.initial fuel) program h_eq
rw [h_stack]
simp [AVMState.initial]
theorem computation_generates_time (program : List Instruction) (fuel : Nat)
(h_nonzero : (runAVM program fuel).result ≠ .Ζ)
(h_terminates : (runAVM program fuel).fuel > 0 ∨ program.length > 0) :
(_h_terminates : (runAVM program fuel).fuel > 0 ∨ program.length > 0) :
(runAVM program fuel).tic > 0 := by
-- If the program produced a meaningful result, it must have executed
-- at least one instruction, which increments TIC by at least 1.
sorry -- Proof: δ increments tic on every instruction execution
-- Contrapositive: if final TIC is 0, the stack stayed empty, so result = Ζ.
by_contra h
have h_tic : (runAVM program fuel).tic = 0 := by omega
have h_stack : (runAVM program fuel).stack = [] :=
runAVM_tic_zero_stack_empty program fuel h_tic
have h_result : (runAVM program fuel).result = .Ζ := by
simp [AVMState.result, h_stack]
contradiction
-- =============================================================================
-- §6. LIBRARY INTERFACE

6
PORTING_MAP.md
View file

@ -74,7 +74,7 @@ The source tree is large (~9,600 objects, ~1,300 Lean files). Most of it is expl
| Research-Stack | SilverSight Target | Status | Notes |
|----------------|-------------------|--------|-------|
| `Semantics.FixedPoint.lean` | `Core/SilverSightCore.lean` / `formal/CoreFormalism/Q16_16_Spec.lean` | 🟡 PORT | The full FixedPoint module with Q0_16/Q16_16 inverse trig, clamping, and determinism theorems should replace the current thin spec. |
| `Semantics.FixedPoint.lean` | `formal/CoreFormalism/FixedPoint.lean` | ✅ PORTED | Full FixedPoint module with Q0_16/Q16_16 inverse trig, clamping, and determinism theorems. Replaced the thin `Q16_16_Spec.lean`. |
| `Semantics.SidonSets.lean` | `Core/` or `SearchLib/` | 🟡 PORT | Proven Sidon set construction, Singer theorem, Bertrand residue injectivity. Core to addressing. |
| `Semantics.InteractionGraphSidon.lean` | `SearchLib/` | 🟡 PORT | RRC weak-axis reconstruction via CRT; part of search/addressing. |
| `Semantics.SieveLemmas.lean` | `SearchLib/` or `Core/` | 🟡 PORT | Coprime-sieve reconstruction, CRT recovery theorem, executable witnesses. |
@ -218,7 +218,7 @@ Things SilverSight's architecture calls for but Research-Stack does not cleanly
| Conflict | Resolution |
|----------|------------|
| Research-Stack `Q16_16.lean` vs SilverSight `Q16_16_Spec.lean` | SilverSight spec is thin. Replace with Research-Stack `FixedPoint.lean` (canonical, proven, includes Q0_16 + inverse trig). |
| Research-Stack `Q16_16.lean` / `FixedPoint.lean` vs SilverSight `Q16_16_Spec.lean` | ✅ PORTED — `Q16_16_Spec.lean` deleted; `formal/CoreFormalism/FixedPoint.lean` is now the canonical source of truth. |
| Research-Stack `qaoa_adapter.py` (2,421 lines) vs SilverSight split `qubo/*.py` | Split adapter: Finsler/QUBO builder → MetricLib/QUBOLib; circuit generation → QUBOLib; bitstring bridge → PVGSLib. |
| Research-Stack `AGENTS.md` references many dead paths | Port rules, not state. Update path references to SilverSight equivalents. |
| SilverSight `ARCHITECTURE.md` uses 6 layers; conceptual map uses 5 | Reconcile: 5-layer conceptual map is authoritative; 6-layer doc is an older draft. Update `ARCHITECTURE.md` to match 5-layer model + library method. |
@ -227,7 +227,7 @@ Things SilverSight's architecture calls for but Research-Stack does not cleanly
## 6. Recommended Porting Order
1. **Core first** — Replace `Q16_16_Spec.lean` with full `FixedPoint.lean`. Lock down `SilverSightCore.lean`.
1. **Core first** — ✅ Replace `Q16_16_Spec.lean` with full `FixedPoint.lean`. Lock down `SilverSightCore.lean`. `SilverSightCore.lean` now builds with no sorries and no `Float`.
2. **SearchLib** — Port `SidonSets.lean`, `SieveLemmas.lean`, `InteractionGraphSidon.lean`.
3. **RRCLib** — Extract RRC gates from `PVGS_DQ_Bridge_fixed.lean` §4 into standalone library.
4. **QUBOLib + MetricLib** — Split `qaoa_adapter.py` and `qubo_highs.py` cleanly.

2
README.md
View file

@ -6,7 +6,7 @@ A deterministic equation search and classification system built on chaos game th
| Directory | Contents |
|-----------|----------|
| `formal/CoreFormalism/` | Lean 4: ChentsovFinite, HachimojiBase, HachimojiCodec, HachimojiManifoldAxiom, Q16_16_Spec |
| `formal/CoreFormalism/` | Lean 4: FixedPoint (canonical Q16_16/Q0_16), ChentsovFinite, HachimojiBase, HachimojiCodec, HachimojiManifoldAxiom |
| `formal/PVGS_DQ_Bridge/` | Lean 4: Photon-Varied Gaussian State to Dual Quaternion energy bridge (7 sections + master) |
| `formal/UniversalEncoding/` | Lean 4: 50-token math address space, 4D chirality classification |
| `formal/BindingSite/` | Lean 4: Amino acid vocabulary mapping, entropy-based bindability |

55
REBASE_RULES.md
View file

@ -1,11 +1,17 @@
# REBASE RULES — Research Stack Agent / Rules Manifest
# REBASE RULES — SilverSight Agent / Rules Manifest
**Purpose:** This file is a rebase seed. When starting a fresh project map, copy only
the files and rules listed here. Do not migrate runtime state, stale audits, or
completed assignment boards.
the files and rules listed here. Do not migrate runtime state, stale audits,
completed assignment boards, or legacy deployment hacks.
**Principle:** *Port the contracts and the rituals, not the state.*
**Status:** Research Stack contained many legacy hacks (Hermes ports, Headroom
proxy endpoints, old benchmark tables, repo-specific paths). Those have been
stripped. The core conceptual bindings — Lean authority, no-Float compute,
receipt boundaries, programming-choice flow, and the post-interaction ritual —
are preserved here and in `AGENTS.md`.
---
## 1. Core Operating Contracts (MUST PORT)
@ -15,35 +21,35 @@ They are actively maintained and cross-referenced throughout the stack.
| File | Scope |
|------|-------|
| `AGENTS.md` (root) | Master operating contract: post-interaction workflow, programming-choice flow, Q16_16 doctrine, Git hygiene, Do-Not-Sweep rules, glossary, claim boundaries. |
| `0-Core-Formalism/lean/Semantics/AGENTS.md` | Lean/Semantics local contract: blessed Compiler surface, build baselines, quarantine boundaries, proof-tactic lessons, current solidification anchors. |
| `4-Infrastructure/AGENTS.md` | Infrastructure and shim contract: storage stack, hardware-witness boundaries, ENE schema, compute dispatch pattern. |
| `6-Documentation/docs/AGENTS.md` | Strict LLM operating rules: anti-drift evidence standards, `bind` primitive, naming conventions, sigma levels, SI units, deletion criteria, PQC policy. |
| `5-Applications/text-to-cad/AGENTS.md` | CAD harness contract: generated CAD/URDF source-of-truth, viewer handoff, repo policies. |
| `scripts/qc-flag/AGENTS.md` | Lean QC protocol: 7-check inspection protocol. |
| `shared-data/artifacts/lean_expert_agent/AGENTS.md` | Lean expert agent `/inspect` protocol and output format. |
| `.github/RRC_OPERATING_CONTRACT.md` | Rainbow Raccoon Compiler gate definition: ACCEPT / HOLD / QUARANTINE. |
| `AGENTS.md` (this repo) | **SilverSight master operating contract.** Distilled from Research Stack; strips legacy deployment details and adapts rules to the library-method architecture. |
| `0-Core-Formalism/lean/Semantics/AGENTS.md` | Lean/Semantics local contract: blessed Compiler surface, build baselines, quarantine boundaries, proof-tactic lessons, current solidification anchors. **ADAPT** to `formal/AGENTS.md` in SilverSight. |
| `4-Infrastructure/AGENTS.md` | Infrastructure and shim contract: storage stack, hardware-witness boundaries, ENE schema, compute dispatch pattern. **PORT ONLY IF** infrastructure work continues; otherwise drop. |
| `6-Documentation/docs/AGENTS.md` | Strict LLM operating rules: anti-drift evidence standards, `bind` primitive, naming conventions, sigma levels, SI units, deletion criteria, PQC policy. **ADAPT** to `docs/AGENTS.md` if strict doc rules are needed. |
| `5-Applications/text-to-cad/AGENTS.md` | CAD harness contract: generated CAD/URDF source-of-truth, viewer handoff, repo policies. **PORT ONLY IF** CAD work continues. |
| `scripts/qc-flag/AGENTS.md` | Lean QC protocol: 7-check inspection protocol. **ADAPT** to `tests/qc-flag/AGENTS.md` if the protocol is adopted. |
| `shared-data/artifacts/lean_expert_agent/AGENTS.md` | Lean expert agent `/inspect` protocol and output format. **ADAPT** if a formal reviewer agent is wired up. |
| `.github/RRC_OPERATING_CONTRACT.md` | Rainbow Raccoon Compiler gate definition: ACCEPT / HOLD / QUARANTINE. **ADAPT** to SilverSight's receipt gate if RRC work continues. |
### Non-negotiable rules extracted from the contracts
1. **Lean is the source of truth.** Python, Rust, and Verilog are extraction targets only.
1. **Lean is the source of truth.** Python and Verilog are extraction targets only.
2. **Programming choice flow** — before writing new logic, check this decision tree in order:
- Admissibility / routing / alignment / gating decision? → **Lean only.**
- Emitting a top-level receipt or JSON bundle? → **`Semantics.AVMIsa.Emit` only.**
- Classifying rows / computing alignment scores? → **Lean (`Semantics.RRC.*`).**
- Supplying raw input features (equation text, IDs, weak_axes)? → **Python shim OK,** no admissibility logic, regenerable from source.
- Minting/stamping a top-level receipt or JSON bundle? → **Lean stamps; Python formats/stores only.**
- Classifying rows / computing alignment scores? → **Lean (`formal/CoreFormalism/` or a new `formal/*.lean` module).**
- Supplying raw input features (expression text, IDs, weak_axes)? → **Python shim OK,** no admissibility logic, regenerable from source.
- Float arithmetic in a compute path? → **STOP.** Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofRawInt`.
- Advancing promotion status in shim space? → **STOP.** `not_promoted` until a Lean gate passes.
- Pure I/O (read/write JSON, subprocess, format output)? → **Python shim OK.** Receipt output routes through `AVMIsa.Emit`.
3. **No `Float` in compute paths.** `ofFloat` is permitted only at JSON/sensor boundaries and must be immediately bracketed.
- Pure I/O (read/write JSON, subprocess, format output)? → **Python shim OK.** Receipt output is stamped in Lean and stored by Python.
3. **No `Float` in Lean compute paths.** `ofFloat` is permitted only at JSON/sensor boundaries and must be immediately bracketed. `Float` is forbidden in `Core/` entirely.
4. **Post-interaction workflow** (mandatory after any code/receipt/architecture change):
- Update the nearest scoped `AGENTS.md` for every touched subtree.
- Run `lake build Compiler` (and full `lake build` if Lean files touched).
- Run the narrow Lean target first, then full `lake build` if Lean files touched.
- Commit with an explicit file list; **never** `git add .`.
- Run `git status --branch --short --untracked-files=all`.
5. **Do Not Sweep:** never run `git add .`, `git checkout -- .`, or `git clean -fdx`.
6. **Secrets are runtime-only:** use environment variables (`OLLAMA_API_KEY`, `DEEPSEEK_API_KEY`, etc.); never commit literal keys.
7. **Legacy recovery is explicit:** use `RECOVER LEGACY INFORMATION: <path/commit/concept>` only. Current cornfield ref: `backup/distilled-with-vcd-history-2026-05-11`.
7. **Legacy recovery is explicit:** use `RECOVER LEGACY INFORMATION: <path/commit/concept>` only. Cross-repo cornfield ref: `backup/distilled-with-vcd-history-2026-05-11`.
---
@ -157,12 +163,15 @@ Use this when standing up the new project map.
When designing the new project layout, preserve these boundary rules:
- **Lean owns decisions; Python owns I/O.**
- **`Semantics.AVMIsa.Emit` is the sole top-level receipt boundary.**
- **`shared-data/` is ignored by default.** Promote only durable receipts with `git add -f -- <path>`.
- **Research artifacts go outside the git tree** (e.g. `/home/researcher/research/` in the container model).
- **`Core/SilverSightCore.lean` is the root authority and imports nothing.**
- **The `Receipt` is the sole Core/library boundary.** Lean stamps; libraries format/store.
- **`python/` and `qubo/` are I/O and optimization shims only.** No admissibility logic in shim space.
- **Research artifacts go outside the git tree** unless promoted as durable receipts.
- **Every new compression path needs two Lean theorems:** `eigensolid_convergence` and `receipt_invertible`.
- **No library imports another library.** Libraries import `Core/` only.
---
*Generated from active Research Stack agent rules and contracts.*
*Generated from active Research Stack agent rules and contracts, stripped of legacy hacks.*
*Principle: port contracts and rituals, not state.*
*SilverSight master contract: `AGENTS.md`.*

1311
formal/CoreFormalism/FixedPoint.lean Normal file
View file

File diff suppressed because it is too large Load diff

292
formal/CoreFormalism/Q16_16_Spec.lean
View file

@ -1,292 +0,0 @@
/- Q16_16 Canonical Specification
Q16_16 represents fixed-point numbers with 16 integer bits and 16 fractional bits.
Range: [-32768.0, 32767.9999847412109375]
Resolution: 1/65536 ≈ 0.0000152587890625
CANONICAL ROUNDING MODE: round-half-up (banker's rounding)
- Values exactly at half-LSB round to nearest even
- All other values round to nearest
This specification is the single source of truth. All language implementations
(Lean, Python, C) MUST produce identical results for all operations.
FILE: CoreFormalism/Q16_16_Spec.lean
STATUS: canonical specification (source of truth)
STAGE: Stage 1 Foundation
-/
import Mathlib.Data.Int.Basic
import Mathlib.Data.Real.Basic
namespace Q16_16_Canonical
-- ============================================================
-- §1 CONSTANTS AND TYPE
-- ============================================================
/-- Scale factor: 2^16 = 65536. The number of subdivisions per unit. -/
def Q16_SCALE : ℕ := 65536
/-- Maximum representable integer value before scaling. -/
def Q16_MAX_RAW : ℤ := 2147483647 -- INT32_MAX
/-- Minimum representable integer value before scaling. -/
def Q16_MIN_RAW : ℤ := -2147483648 -- INT32_MIN
/-- Q16_16 is represented as a 32-bit signed integer internally,
where the raw value = floor(x * 65536) after canonical rounding. -/
def Q16_16 := { q : ℤ // q ≥ Q16_MIN_RAW ∧ q ≤ Q16_MAX_RAW }
-- ============================================================
-- §2 CONVERSIONS
-- ============================================================
/-- Convert a Float to Q16_16 with canonical round-half-up (banker's rounding).
Algorithm:
scaled = f * 65536.0
If |scaled - round(scaled)| == 0.5:
round to nearest even
Else:
round to nearest integer
This matches Python's round() with no ndigits specified and C's
round() from math.h with the half-way case going to nearest even.
-/
def ofFloat (f : Float) : Q16_16 :=
let scaled := f * (Float.ofNat Q16_SCALE)
let rounded := Float.round scaled
let clipped := max (Float.ofInt Q16_MIN_RAW) (min (Float.ofInt Q16_MAX_RAW) rounded)
⟨Float.toInt clipped, by
-- Proof obligation: result is in valid range
simp [Q16_MIN_RAW, Q16_MAX_RAW]
-- Clip guarantees bounds
have h1 : Float.toInt clipped ≥ -2147483648 := by
have h_clip : clipped ≥ Float.ofInt (-2147483648 : ℤ) := by
apply max_le_iff.mpr
left
apply le_refl
have h2 : Float.toInt (Float.ofInt (-2147483648 : ℤ)) = -2147483648 := by
simp [Float.toInt_ofInt]
have h3 : Float.toInt clipped ≥ Float.toInt (Float.ofInt (-2147483648 : ℤ)) := by
apply Float.toInt_le_toInt
exact h_clip
rw [h2] at h3
exact h3
have h2 : Float.toInt clipped ≤ 2147483647 := by
have h_clip : clipped ≤ Float.ofInt (2147483647 : ℤ) := by
apply min_le_iff.mpr
left
apply le_refl
have h2 : Float.toInt (Float.ofInt (2147483647 : ℤ)) = 2147483647 := by
simp [Float.toInt_ofInt]
have h3 : Float.toInt clipped ≤ Float.toInt (Float.ofInt (2147483647 : ℤ)) := by
apply Float.toInt_le_toInt
exact h_clip
rw [h2] at h3
exact h3
exact ⟨h1, h2⟩⟩
/-- Convert Q16_16 to Float. Exact (no rounding needed). -/
def toFloat (q : Q16_16) : Float :=
Float.ofInt q.val / (Float.ofNat Q16_SCALE)
/-- Convert an Int to Q16_16 (exact, no rounding). -/
def ofInt (i : ℤ) : Q16_16 :=
let scaled := i * (Q16_SCALE : ℤ)
let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW scaled)
⟨clipped, by
simp [Q16_MIN_RAW, Q16_MAX_RAW]
constructor
· exact le_trans (by norm_num) (show -2147483648 ≤ clipped from by
have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; norm_num
exact h)
· have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; norm_num
exact le_trans h (by norm_num)⟩
/-- Convert Q16_16 to Int (truncates fractional part, rounds toward zero). -/
def toInt (q : Q16_16) : ℤ :=
q.val / (Q16_SCALE : ℤ)
-- ============================================================
-- §3 ARITHMETIC OPERATIONS
-- ============================================================
/-- Addition with saturation (clamped to range, no overflow wrap). -/
def add (a b : Q16_16) : Q16_16 :=
let sum := a.val + b.val
let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW sum)
⟨clipped, by
constructor
· have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; rfl
exact h
· have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; rfl
exact h⟩
/-- Subtraction with saturation. -/
def sub (a b : Q16_16) : Q16_16 :=
let diff := a.val - b.val
let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW diff)
⟨clipped, by
constructor
· have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; rfl
exact h
· have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; rfl
exact h⟩
/-- Multiplication: result = (a.val * b.val) / 65536 with canonical rounding.
Uses 64-bit intermediate to prevent overflow, then applies
canonical round-half-up before clamping to 32-bit range.
-/
def mul (a b : Q16_16) : Q16_16 :=
let prod_64 := (a.val : ℤ) * (b.val : ℤ)
-- Divide by scale with rounding: prod_64 / 65536 with half-up
let scaled := prod_64 / (Q16_SCALE : ℤ)
let remainder := prod_64 % (Q16_SCALE : ℤ)
let half_scale := (Q16_SCALE : ℤ) / 2
let rounded :=
if remainder > half_scale then scaled + 1
else if remainder < half_scale then scaled
else if (scaled % 2) = 0 then scaled -- tie: round to even
else scaled + 1
let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW rounded)
⟨clipped, by
constructor
· have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; rfl
exact h
· have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; rfl
exact h⟩
/-- Division: result = (a.val * 65536) / b.val with canonical rounding.
b must be non-zero. Uses 64-bit intermediate precision.
-/
def div (a b : Q16_16) (hb : b.val ≠ 0) : Q16_16 :=
let num_64 := (a.val : ℤ) * (Q16_SCALE : ℤ)
let scaled := num_64 / b.val
let remainder := num_64 % b.val
let half_b := b.val / 2
let rounded :=
if remainder > half_b then scaled + 1
else if remainder < half_b then scaled
else if (scaled % 2) = 0 then scaled -- tie: round to even
else scaled + 1
let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW rounded)
⟨clipped, by
constructor
· have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; rfl
exact h
· have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; rfl
exact h⟩
-- ============================================================
-- §4 COMPARISON OPERATIONS
-- ============================================================
def eq (a b : Q16_16) : Bool := a.val = b.val
def lt (a b : Q16_16) : Bool := a.val < b.val
def le (a b : Q16_16) : Bool := a.val ≤ b.val
-- ============================================================
-- §5 ROUNDTRIP THEOREMS (Core Correctness Properties)
-- ============================================================
/-- The roundtrip error for float→Q16_16→float is bounded by 1/65536.
This is the fundamental correctness property of the encoding. -/
theorem roundtrip_float_error (f : Float) (h_min : f ≥ -32768.0) (h_max : f ≤ 32767.9999847412109375) :
let q := ofFloat f
let f' := toFloat q
(f' - f).abs ≤ 1.0 / (Float.ofNat Q16_SCALE) := by
-- Proof sketch: ofFloat rounds to nearest representable value
-- with error ≤ 0.5 LSB = 0.5/65536. toFloat is exact inverse.
-- Therefore |f' - f| ≤ 1/65536.
simp [ofFloat, toFloat, Q16_SCALE]
-- Detailed proof requires Float.toInt_round properties
sorry -- TODO: complete with Float library lemmas
/-- Integer roundtrip is exact for all integers in the valid range. -/
theorem roundtrip_int_exact (i : ℤ) (h_min : i ≥ -32768) (h_max : i ≤ 32767) :
toInt (ofInt i) = i := by
simp [toInt, ofInt, Q16_SCALE, Q16_MIN_RAW, Q16_MAX_RAW]
-- scaled = i * 65536 is within [-2^31, 2^31-1] for i in [-32768, 32767]
have h_range : -2147483648 ≤ i * 65536 ∧ i * 65536 ≤ 2147483647 := by
constructor
· nlinarith
· nlinarith
-- Clipping is a no-op for in-range values
have h_clip : max (-2147483648) (min 2147483647 (i * 65536)) = i * 65536 := by
rw [min_eq_right h_range.2]
rw [max_eq_left h_range.1]
rw [h_clip]
-- Division reverses the scaling
have h_div : (i * 65536) / 65536 = i := by
field_simp
exact h_div
/-- Zero is represented exactly. -/
theorem zero_exact : ofFloat 0.0 = ⟨0, by norm_num⟩ := by
simp [ofFloat, Q16_SCALE, Q16_MIN_RAW, Q16_MAX_RAW]
sorry -- Requires Float.round_zero lemma
/-- One is represented exactly. -/
theorem one_exact : ofFloat 1.0 = ⟨65536, by norm_num⟩ := by
simp [ofFloat, Q16_SCALE, Q16_MIN_RAW, Q16_MAX_RAW]
sorry -- Requires Float.round and toInt_ofInt lemmas
-- ============================================================
-- §6 SPECIFICATION OF CANONICAL ROUNDING FOR VERIFICATION
-- ============================================================
/-- The canonical rounding function for Q16_16.
This is the mathematical specification of rounding that all
implementations must satisfy.
For a real value x, canonical_round(x) is:
- floor(x * 65536 + 0.5) if fractional part of x*65536 > 0.5
- ceil(x * 65536 - 0.5) if fractional part of x*65536 < 0.5
- nearest even if fractional part of x*65536 == 0.5
-/
def canonical_round (x : ℝ) : ℤ :=
let scaled := x * (Q16_SCALE : ℝ)
let int_part := ⌊scaled⌋
let frac_part := scaled - (int_part : ℝ)
if frac_part > (1 / 2 : ℝ) then int_part + 1
else if frac_part < (1 / 2 : ℝ) then int_part
else if (int_part % 2) = 0 then int_part -- tie: round to even
else int_part + 1
/-- The canonical rounding produces values in the valid Q16_16 range
for inputs in [-32768, 32767.9999847412109375]. -/
theorem canonical_round_in_range (x : ℝ) (h_min : x ≥ -32768) (h_max : x ≤ 32767.9999847412109375) :
let r := canonical_round x
r ≥ Q16_MIN_RAW ∧ r ≤ Q16_MAX_RAW := by
simp [canonical_round, Q16_MIN_RAW, Q16_MAX_RAW, Q16_SCALE]
constructor
· -- Lower bound
have h1 : ⌊x * 65536⌋ ≥ -2147483648 := by
have h2 : x * 65536 ≥ -2147483648 := by nlinarith
have h3 : (⌊x * 65536⌋ : ℝ) ≥ x * 65536 - 1 := by
exact Int.sub_one_lt_floor (x * 65536) |>.le
have h4 : (⌊x * 65536⌋ : ℝ) ≥ -2147483649 := by linarith
have h5 : ⌊x * 65536⌋ ≥ -2147483649 := by exact_mod_cast h4
omega
split_ifs <;> omega
· -- Upper bound
have h1 : ⌊x * 65536⌋ ≤ 2147483647 := by
have h2 : x * 65536 ≤ 2147483647.9999 := by nlinarith
have h3 : (⌊x * 65536⌋ : ℝ) ≤ x * 65536 := by
exact Int.floor_le (x * 65536)
have h4 : (⌊x * 65536⌋ : ℝ) ≤ 2147483647.9999 := by linarith
have h5 : ⌊x * 65536⌋ ≤ 2147483647 := by
by_contra h6
push_neg at h6
have h7 : ⌊x * 65536⌋ ≥ 2147483648 := by omega
have h8 : (⌊x * 65536⌋ : ℝ) ≥ (2147483648 : ℝ) := by exact_mod_cast h7
linarith
exact h5
split_ifs <;> omega
end Q16_16_Canonical

96
lake-manifest.json Normal file
View file

@ -0,0 +1,96 @@
{"version": "1.2.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "e5836dbb05fccdfa24ab3396d46f1f49b1f816ed",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "f3f26cc72646205ca167117487c008ee1dafe816",
"name": "plausible",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/LeanSearchClient",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
"name": "LeanSearchClient",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/import-graph",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "41f407a8e85b0fdc00910633a8f14754139b63f4",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "125807f43a86b5d58892b7ea6972eec0d6c164d2",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"scope": "leanprover",
"rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.32.0-rc1",
"inherited": true,
"configFile": "lakefile.toml"}],
"name": "SilverSight",
"lakeDir": ".lake",
"fixedToolchain": false}

22
lakefile.lean Normal file
View file

@ -0,0 +1,22 @@
import Lake
open Lake DSL
package «SilverSight» where
-- Settings applied to both builds and interactive editing
leanOptions := #[
⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
]
-- Add any additional package configuration options here
@[default_target]
lean_lib «SilverSightCore» where
-- Add any library configuration options here
srcDir := "Core"
roots := #[`SilverSightCore]
lean_lib «SilverSightFormal» where
srcDir := "formal"
roots := #[`CoreFormalism.FixedPoint]
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"

1
lean-toolchain Normal file
View file

@ -0,0 +1 @@
leanprover/lean4:v4.32.0-rc1

2
python/q16_canonical.py
View file

@ -1,6 +1,6 @@
"""Canonical Q16_16 fixed-point arithmetic.
Single source of truth: CoreFormalism/Q16_16_Spec.lean
Single source of truth: CoreFormalism/FixedPoint.lean
All operations MUST produce identical results to the Lean implementation.
Q16_16 represents fixed-point numbers with 16 integer bits and 16 fractional bits.

2
qubo/finsler_metric.py
View file

@ -26,7 +26,7 @@ import numpy as np
# =========================================================================
# Q16_16 Fixed-Point Constants (from CoreFormalism/Q16_16_Spec.lean)
# Q16_16 Fixed-Point Constants (from CoreFormalism/FixedPoint.lean)
# =========================================================================
Q16_SCALE: int = 65536 # 2^16 -- number of subdivisions per unit

2
tests/q16_roundtrip_test.py
View file

@ -413,7 +413,7 @@ def run_test_summary():
print(" STATUS: ALL TESTS PASSED ✓")
print()
print(" Q16_16 rounding is CANONICAL across Python and C.")
print(" Lean specification: CoreFormalism/Q16_16_Spec.lean")
print(" Lean specification: CoreFormalism/FixedPoint.lean")
print(" Python implementation: PythonBridge/q16_canonical.py")
print(" C implementation: CBride/q16_canonical.c")
return 0