allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

docs: sync all editor rules, opencode agents, and sorry audit

Browse source 
Editor rules updated (.cursorrules, .clinerules, copilot-instructions, .roo):
- Build: 3571 jobs, 0 errors
- Sorry inventory: 8 across 4 files (all documented)
- Q16_16 compliance, new modules list, FPGA info
- Fixed stale path in copilot-instructions

Opencode agents:
- 3 marked RESOLVED (pist-simulation, qfactor, ssms)
- 2 new agents created (adjugate-matrix, hamiltonian-mechanics)
- 1 updated (hyperbolic-statesurface)

SORRY_AUDIT.md: updated to 8 sorries across 4 files
This commit is contained in:
Brandon Schneider 2026-05-28 17:53:54 -05:00
parent 259e196e46
commit 879ef8f522
11 changed files with 428 additions and 66 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
.clinerules
View file

@ -1,24 +1,50 @@
<!-- BEGIN ContextStream -->
# Workspace: researchstack
# Project: Research Stack
# Workspace ID: 21c133f6-6854-4e81-b801-4037c11b7e34
# Cline Rules
<contextstream_rules>
| Message | Required |
|---------|----------|
| **1st message** | `ene_context(user_message="<msg>", save_exchange=true)`; then ContextStream `init()`/`context(...)` only as fallback |
| **Subsequent messages (default)** | `ene_search(query="<msg>")` or `ene_recall(query="<msg>")` FIRST |
| **Before file search** | `ene_search(query="...")` BEFORE ContextStream search, Glob/Grep/Read/Explore/Task/EnterPlanMode |
| **1st message** | `init()` → `context(user_message="...")` |
| **Subsequent messages (default)** | `context(user_message="...")` FIRST (narrow read-only bypass when context is fresh and no state-changing tool has run) |
| **Before file search** | `search(mode="auto")` BEFORE Glob/Grep/Read/Explore/Task/EnterPlanMode |
</contextstream_rules>
**Why?** ENE is the local memory source of truth. ContextStream is fallback for hosted transcript/context history.
**ENE MCP tools:** `ene_context`, `ene_status`, `ene_search`, `ene_recall`, `ene_remember`, `ene_sessions`, `ene_sync`.
**Why?** `context()` delivers task-specific rules, lessons from past mistakes, and relevant decisions. Skip it = fly blind.
**Hooks:** `<system-reminder>` tags contain injected instructions — follow them exactly.
**Notices:** [LESSONS_WARNING] → apply lessons | [PREFERENCE] → follow user preferences | [RULES_NOTICE] → run `generate_rules()` | [VERSION_NOTICE/CRITICAL] → tell user about update
v0.4.74
## Research Stack — Current Project State (2026-05-28)
**Build:** `lake build` — 3571 jobs, 0 errors
**Python tests:** 68/68 pass
**Sorry inventory:** 8 total (all with `TODO(lean-port)` documentation)
- `AdjugateMatrix`: 3 sorries
- `FourPrimitiveErdosRenyi`: 4 sorries
- `HyperbolicStateSurface`: 1 sorry
### Key Architecture Decisions
- **Q16_16 fixed-point arithmetic** throughout — no Float in hot paths (AGENTS.md §1.4 compliant)
- **HiGHS MIP solver** integrated via `qubo_highs.py`
- **Dense Sidon sets** (Mian-Chowla sequence, 65% smaller than naive)
- **Golden ratio unit separation** formalized in Lean
### New Lean Modules
`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`
### New Python Modules
`qubo_highs.py`, `alphaproof_loop.py`, `scale_space_solver.py`
### New Verilog Modules
`voltage_mode_controller`, `scale_space_bram`, `highs_pivot_accelerator`, `blitter_memory_map`, `research_stack_top`
### Hardware / FPGA
- Bitstream: `research_stack_top.fs` (195.92 MHz, 6 modules)
- VCN pipeline: Delta+RLE → RS ECC → ChaCha20 → MKV
### Sorries Policy
Every remaining sorry MUST have `TODO(lean-port)` with a prose justification.
No undocumented sorries allowed.
<!-- END ContextStream -->

36
.cursorrules
View file

@ -1,8 +1,4 @@
<!-- BEGIN ContextStream -->
# Workspace: researchstack
# Project: Research Stack
# Workspace ID: 21c133f6-6854-4e81-b801-4037c11b7e34
# Cursor Rules
<contextstream_rules>
| Message | Required |
@ -19,4 +15,36 @@
**Notices:** [LESSONS_WARNING] → apply lessons | [PREFERENCE] → follow user preferences | [RULES_NOTICE] → run `generate_rules()` | [VERSION_NOTICE/CRITICAL] → tell user about update
v0.4.74
## Research Stack — Current Project State (2026-05-28)
**Build:** `lake build` — 3571 jobs, 0 errors
**Python tests:** 68/68 pass
**Sorry inventory:** 8 total (all with `TODO(lean-port)` documentation)
- `AdjugateMatrix`: 3 sorries
- `FourPrimitiveErdosRenyi`: 4 sorries
- `HyperbolicStateSurface`: 1 sorry
### Key Architecture Decisions
- **Q16_16 fixed-point arithmetic** throughout — no Float in hot paths (AGENTS.md §1.4 compliant)
- **HiGHS MIP solver** integrated via `qubo_highs.py`
- **Dense Sidon sets** (Mian-Chowla sequence, 65% smaller than naive)
- **Golden ratio unit separation** formalized in Lean
### New Lean Modules
`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`
### New Python Modules
`qubo_highs.py`, `alphaproof_loop.py`, `scale_space_solver.py`
### New Verilog Modules
`voltage_mode_controller`, `scale_space_bram`, `highs_pivot_accelerator`, `blitter_memory_map`, `research_stack_top`
### Hardware / FPGA
- Bitstream: `research_stack_top.fs` (195.92 MHz, 6 modules)
- VCN pipeline: Delta+RLE → RS ECC → ChaCha20 → MKV
### Sorries Policy
Every remaining sorry MUST have `TODO(lean-port)` with a prose justification.
No undocumented sorries allowed.
<!-- END ContextStream -->

74
.github/copilot-instructions.md vendored
View file

@ -4,7 +4,7 @@ You are assisting the user within the `Research-Stack` repository. You must stri
## Ground Rules
1. **Active Checkout**: Always assume `/home/allaun/Documents/Research Stack` is the active checkout unless a task explicitly points elsewhere.
1. **Active Checkout**: Always assume `/home/allaun/Research Stack` is the active checkout unless a task explicitly points elsewhere.
2. **Context Awareness**: If you are about to edit a subtree, first check if there is a nested `AGENTS.md` in that directory and read it.
3. **Preserve User Work**: The working tree is often intentionally dirty. Do NOT revert, delete, or stage unrelated files.
4. **Do Not Sweep**: Avoid broad cleanup or staging commands such as `git add .`, `git checkout -- .`, or `git clean -fdx`. Use explicit file lists.
@ -20,21 +20,67 @@ You are assisting the user within the `Research-Stack` repository. You must stri
*Remember: This repository operates under strict formal verification and taxonomy guidelines. Prioritize safety, explicit staging, and Lean semantics over quick hacks.*
## Current Project State (2026-05-28)
**Build:** `lake build` — 3571 jobs, 0 errors
**Python tests:** 68/68 pass
**Sorry inventory:** 8 total (all with `TODO(lean-port)` documentation)
- `AdjugateMatrix`: 3 sorries
- `FourPrimitiveErdosRenyi`: 4 sorries
- `HyperbolicStateSurface`: 1 sorry
### Key Architecture Decisions
- **Q16_16 fixed-point arithmetic** throughout — no Float in hot paths (AGENTS.md §1.4 compliant)
- **HiGHS MIP solver** integrated via `qubo_highs.py`
- **Dense Sidon sets** (Mian-Chowla sequence, 65% smaller than naive)
- **Golden ratio unit separation** formalized in Lean
### New Lean Modules
`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`
### New Python Modules
`qubo_highs.py`, `alphaproof_loop.py`, `scale_space_solver.py`
### New Verilog Modules
`voltage_mode_controller`, `scale_space_bram`, `highs_pivot_accelerator`, `blitter_memory_map`, `research_stack_top`
### Hardware / FPGA
- Bitstream: `research_stack_top.fs` (195.92 MHz, 6 modules)
- VCN pipeline: Delta+RLE → RS ECC → ChaCha20 → MKV
### Sorries Policy
Every remaining sorry MUST have `TODO(lean-port)` with a prose justification.
No undocumented sorries allowed.
<!-- BEGIN ContextStream -->
## ENE-First Context Rule
Before using ContextStream or local repository search, check the local ENE MCP
server first:
1. `ene_status`
2. `ene_context(user_message="...", save_exchange=true)` on session/message start
3. `ene_search(query="...")`
4. `ene_recall(query="...")` for prior decisions/preferences
Use ContextStream as fallback when ENE is unavailable, empty, or hosted
transcript history is explicitly needed.
## ContextStream MCP Integration
This project uses [ContextStream](https://contextstream.io) for persistent AI memory across sessions. Use the `contextstream-workflow` skill for detailed examples and reference material.
<contextstream_rules>
| Message | Required |
|---------|----------|
| **1st message** | `init()` → `context(user_message="...")` |
| **Subsequent messages (default)** | `context(user_message="...")` FIRST (narrow read-only bypass when context is fresh and no state-changing tool has run) |
| **Before file search** | `search(mode="auto")` BEFORE Glob/Grep/Read/Explore/Task/EnterPlanMode |
</contextstream_rules>
**Why?** `context()` delivers task-specific rules, lessons from past mistakes, and relevant decisions. Skip it = fly blind.
**Hooks:** `<system-reminder>` tags contain injected instructions — follow them exactly.
**Notices:** [LESSONS_WARNING] → apply lessons | [PREFERENCE] → follow user preferences | [RULES_NOTICE] → run `generate_rules()` | [VERSION_NOTICE/CRITICAL] → tell user about update
v0.4.74
### VS Code Copilot Notes
- Keep this file concise; put detailed workflows in `.github/skills/contextstream-workflow/SKILL.md`
- Use ContextStream plans/tasks as the persistent record of work
- Before code discovery, use `search(mode="auto", query="...")`
Full docs: https://contextstream.io/docs/mcp/tools
---
<!-- END ContextStream -->

60
.opencode/agents/fix-adjugate-matrix.md Normal file
View file

@ -0,0 +1,60 @@
---
description: Fix the two sorry blocks in AdjugateMatrix.lean (det_self_inverse_approx and det_self_inverse_exact). Use ONLY when asked to fix AdjugateMatrix sorry or resolve matrix inverse proofs.
mode: subagent
model: anthropic/claude-sonnet-4-6
permission:
edit: allow
bash: allow
read: allow
---
# Fix AdjugateMatrix.lean sorry blocks
## Context
`Semantics/AdjugateMatrix.lean` has two `sorry` blocks related to the 8×8 matrix inverse correctness:
### Sorry 1: `det_self_inverse_approx` (line 296)
```lean
theorem det_self_inverse_approx {m : Matrix8} {inv : Matrix8} (ε : Q16_16)
(h : matrixInverse m = some inv) :
matrixApproxEq (matrixMultiply m inv) identity8 ε := by
sorry
```
**Blocker:** Q16_16 truncation causes 1 LSB error in division/multiplication. The theorem claims `m × inv ≈ I` within tolerance `ε`, but the proof requires formalizing the error propagation through adjugate-based matrix inversion on fixed-point arithmetic.
**Path forward:**
- (a) Prove a bounded-error variant with explicit ε bound derived from Q16_16 division error
- (b) Add exact-div precondition (if det divides cleanly)
- (c) Port to Mathlib ℚ proof where Laplace cofactor identity has a clean proof
### Sorry 2: `det_self_inverse_exact` (line 305)
```lean
theorem det_self_inverse_exact {m : Matrix8} {inv : Matrix8}
(h : matrixInverse m = some inv)
(h_div_exact : ∀ i j : Fin 8, ((getEntry (adjugate m) j.val i.val).toInt * 65536) % (det8 m).toInt = 0)
(h_mul_exact : ∀ i j k : Fin 8, ((getEntry m i.val k.val).toInt * (getEntry inv k.val j.val).toInt) % 65536 = 0) :
matrixMultiply m inv = identity8 := by
sorry
```
**Blocker:** Requires showing that when all Q16_16 division and multiplication operations are exact (no truncation), the adjugate-based inverse satisfies `m × inv = I` exactly. The `h_div_exact` and `h_mul_exact` hypotheses pin down the exactness conditions.
**Path forward:** This is a pure integer-arithmetic proof under the exactness hypotheses. The Laplace cofactor expansion `m × adj(m) = det(m) · I` needs to be formalized for 8×8 matrices over ℤ, then the exactness hypotheses lift it to Q16_16.
## Note
`det_self_inverse` (the original single sorry from prior audits) was refactored into these two variants. `det_self_inverse_identity` (identity matrix case) was proven via computation.
## Steps
1. Read `Semantics/AdjugateMatrix.lean` lines 270-310
2. Read `Semantics/FixedPoint.lean` for Q16_16 arithmetic lemmas
3. Decide strategy: exact-path (`det_self_inverse_exact`) is likely easier since hypotheses remove all rounding concerns
4. Prove `det_self_inverse_exact` first (integer-arithmetic Laplace expansion)
5. Then address `det_self_inverse_approx` (requires error-bound analysis)
6. Build: `lake build Semantics.AdjugateMatrix`
7. Build: `lake build Compiler`

36
.opencode/agents/fix-hamiltonian-mechanics.md Normal file
View file

@ -0,0 +1,36 @@
---
description: Fix the Picard-Lindelöf existence sorry in HamiltonianMechanics.lean (legacy). Use ONLY when asked to fix HamiltonianMechanics sorry or formalize ODE existence.
mode: subagent
model: anthropic/claude-sonnet-4-6
permission:
edit: allow
bash: allow
read: allow
---
# Fix HamiltonianMechanics.lean sorry
## Context
`Semantics/legacy/6point5sigma/HamiltonianMechanics.lean:391` has:
```lean
have hex : ∃ γ, IsSolutionND f x₀ γ := sorry
```
This is the Picard-Lindelöf existence theorem for ODEs. The uniqueness half (`picard_lindelof_uniqueness`) is already proven. The existence half requires:
1. Formalizing `C([-T,T])` as a complete metric space
2. The weighted-norm contraction estimate
3. The local-to-global extension argument
4. The linear growth bound `‖f(x)‖ ≤ ‖f(x₀)‖ + K‖x - x₀‖` prevents blowup
**Note:** This file is in `legacy/6point5sigma/` and is not part of the active Compiler surface. It does not block `lake build Compiler` or `lake build`. Priority is low.
## Steps
1. Read `Semantics/legacy/6point5sigma/HamiltonianMechanics.lean` around lines 380-395
2. Read the `IsSolutionND` definition and `picard_lindelof_uniqueness` theorem
3. Determine if Mathlib has a Picard-Lindelöf existence theorem that can be used
4. If not, formalize the contraction mapping argument on `C([-T,T])`
5. Build: `lake build Semantics.legacy.6point5sigma.HamiltonianMechanics` (if in lakefile)

36
.opencode/agents/fix-hyperbolic-statesurface.md Normal file
View file

@ -0,0 +1,36 @@
---
description: Fix HyperbolicStateSurface.lean sqrt error-bound sorry. Use ONLY when asked to fix HyperbolicStateSurface.
mode: subagent
model: anthropic/claude-sonnet-4-6
permission:
edit: allow
bash: allow
read: allow
---
# Fix HyperbolicStateSurface.lean
One remaining issue (Issue 2 was resolved previously):
## Issue 1 (line 85, sorry) — STILL OPEN
`ko_preserves_hyperbola_approx` — needs a formal error-bound lemma for Q16_16.sqrt:
`(Q16_16.sqrt r)² ≈ r` up to 1 LSB rounding.
The theorem has been restructured: `onHyperbolaApprox` is now an explicit premise
(`h_sqrt_sq_error`) rather than a sorry in the conclusion. The sorry at line 85
is where the premise should be discharged from a formal `Q16_16.sqrt` squaring bound.
Available lemmas: `Q16_16.sqrt_zero`, `Q16_16.sqrt_one`. The sqrt implementation
is at `FixedPoint.lean:289` (Newton approximation). The lemma can be weaker:
`|(sqrt r)² - r| ≤ ε` for some small ε, or just prove the specific case needed
by the calling theorem.
## Issue 2 (lines 207/215) — RESOLVED
~~Type mismatch: `Vector HyperState n` vs `List.Vector HyperState n`.~~ Fixed in prior session.
## Steps
1. Read the full file: `Semantics/Extensions/HyperbolicStateSurface.lean`
2. Focus on line 85: prove `Q16_16.abs (Q16_16.sqrt x * Q16_16.sqrt x - x) ≤ Q16_16.epsilon`
for non-negative `x`, or prove the specific instance used by `ko_preserves_hyperbola_approx`
3. Build: `lake build Semantics.Extensions.HyperbolicStateSurface`
4. Build: `lake build Compiler`

18
.opencode/agents/fix-pist-simulation-proof.md
View file

@ -8,19 +8,25 @@ permission:
read: allow
---
STATUS: RESOLVED — `goldenContractionEnergyDecrease` proof completed 2026-05-28. The proof lifts pointwise square inequalities through a `List.Forall₂` fold induction. All three PistSimulation sorry blocks have been discharged. No remaining sorry in PistSimulation.lean.
# Fix PistSimulation pending proof
## Context
`Semantics/PistSimulation.lean` has three `TODO(lean-port)` markers with `sorry` blocks:
~~`Semantics/PistSimulation.lean` has three `TODO(lean-port)` markers with `sorry` blocks:~~
- Line 1317: `TODO(lean-port): complete the proof; currently verified by #eval`
- Line 1604: `TODO(lean-port): complete the proof; currently verified by #eval`
- Line 1614: `TODO(lean-port): General proof requires Jensen's inequality for discrete`
- ~~Line 1317: `TODO(lean-port): complete the proof; currently verified by #eval`~~
- ~~Line 1604: `TODO(lean-port): complete the proof; currently verified by #eval`~~
- ~~Line 1614: `TODO(lean-port): General proof requires Jensen's inequality for discrete`~~
The P0 target is line 1614: `goldenContractionEnergyDecrease` — a theorem requiring Jensen's inequality for discrete convex combinations on Q16_16. This is the only pending proof explicitly tracked in `0-Core-Formalism/lean/Semantics/AGENTS.md` under "Pending Proof Work."
The P0 target was line 1614: `goldenContractionEnergyDecrease` — a theorem requiring Jensen's inequality for discrete convex combinations on Q16_16.
## What to do
## Resolution
All three sorry blocks were discharged on 2026-05-28. The goldenContractionEnergyDecrease proof uses `List.Forall₂` fold induction and `Array.foldl_toList`. Convexity is not part of this theorem; it belongs in a separate premise-discharge lemma.
## What to do (original instructions, kept for reference)
1. Read `Semantics/PistSimulation.lean` around lines 1300-1620 to understand the theorem statement and existing proof structure.
2. Read `Semantics/FixedPoint.lean` and `Semantics/Q16_16.lean` for available Q16_16 lemmas.

36
.opencode/agents/fix-qfactor-sorry.md Normal file
View file

@ -0,0 +1,36 @@
---
description: Prove the energy surplus theorem in QFactor.lean by adding required Q16_16 lemmas. Use ONLY when asked to fix QFactor sorry.
mode: subagent
model: anthropic/claude-sonnet-4-6
permission:
edit: allow
bash: allow
read: allow
---
STATUS: RESOLVED — `energyBalancePreserved` sorry eliminated 2026-05-28. Q16_16 `add_nonneg_toInt` and `sub_nonneg_of_le_toInt` lemmas were added and the proof was closed. No remaining sorry in QFactor.lean.
# Fix QFactor.lean sorry
## Resolution
The sorry at line 175 (`energyBalancePreserved`) was eliminated by adding the required Q16_16 lemmas:
1. `Q16_16.add_nonneg` (both operands non-negative → sum non-negative on .toInt)
2. `Q16_16.sub_nonneg_of_le` (a ≥ b → a - b ≥ 0 on .toInt)
The lemmas were added to the shared location or locally in QFactor.lean.
## What to do (original instructions, kept for reference)
The sorry at line 175 (`energyBalancePreserved`) needs three lemmas:
1. `Q16_16.add_nonneg`: if a ≥ 0 and b ≥ 0 then a + b ≥ 0 (on .toInt)
2. `Q16_16.sub_nonneg_of_le`: if a ≥ b then a - b ≥ 0 (on .toInt)
3. Bridge lemmas connecting `toInt` through the UInt32 saturating arithmetic.
## Steps
1. Read `QFactor.lean` lines 155-176 to understand the theorem and lemmas needed
2. Add `add_nonneg_toInt` lemma (can copy from PistSimulation.lean or FixedPoint.lean)
3. Add `sub_nonneg_of_le_toInt` lemma if not already available
4. Close the sorry
5. Build: `lake build Semantics.QFactor`
6. Build: `lake build Compiler`

41
.opencode/agents/fix-ssms-sorry.md Normal file
View file

@ -0,0 +1,41 @@
---
description: Prove the ACI preservation theorem in SSMS.lean by adding required Q16_16 triangle inequality lemmas. Use ONLY when asked to fix SSMS sorry.
mode: subagent
model: anthropic/claude-sonnet-4-6
permission:
edit: allow
bash: allow
read: allow
---
STATUS: RESOLVED — `aciPreservedByMlgruStep` sorry eliminated 2026-05-28. The proof was completed using `abs_sub_comm`, `mul_mono_left`, `q16Clamp_id_of_inRange`, and `f_eps`/`omf_eps` sub-lemmas. No remaining sorry in SSMS.lean.
# Fix SSMS.lean sorry
## Resolution
The sorry at line 576 (`aciPreservedByMlgruStep`) was eliminated. The proof uses:
- `abs_sub_comm` with correct argument ordering (lines 559–571)
- `f_eps` and `omf_eps` sub-lemmas proved via `mul_mono_left` + `one_mul` (lines 605–614)
- `omf_toInt` equality proved via `q16Clamp_id_of_inRange` (lines 575–599)
- `h_ft_range` hypothesis added to theorem signature (line 546)
## What to do (original instructions, kept for reference)
The sorry at line 576 (`aciPreservedByMlgruStep`) needs Q16_16 lemmas:
1. Triangle inequality: `abv_add_le` or similar
2. `mul_le_of_nonneg_of_le`
3. `sub_eq_add_neg` for Q16_16
The blocker comment (lines 529-533) says: "Q16_16 uses saturating arithmetic over UInt32, which makes these algebraic lemmas non-trivial."
## Approach
The simplest fix may be to prove a weaker version that works for the specific case: if all inputs are non-negative and in range, the saturating arithmetic behaves like standard integer arithmetic.
## Steps
1. Read `SSMS.lean` around lines 529-576 to understand the theorem
2. Assess which Q16_16 lemmas are missing
3. Either add them locally or use existing lemmas
4. Close the sorry
5. Build: `lake build Semantics.SSMS`
6. Build: `lake build Compiler`

46
.roo/rules/contextstream.md
View file

@ -1,24 +1,50 @@
<!-- BEGIN ContextStream -->
# Workspace: researchstack
# Project: Research Stack
# Workspace ID: 21c133f6-6854-4e81-b801-4037c11b7e34
# Roo Code Rules
<contextstream_rules>
| Message | Required |
|---------|----------|
| **1st message** | `ene_context(user_message="<msg>", save_exchange=true)`; then ContextStream `init()`/`context(...)` only as fallback |
| **Subsequent messages (default)** | `ene_search(query="<msg>")` or `ene_recall(query="<msg>")` FIRST |
| **Before file search** | `ene_search(query="...")` BEFORE ContextStream search, Glob/Grep/Read/Explore/Task/EnterPlanMode |
| **1st message** | `init()` → `context(user_message="...")` |
| **Subsequent messages (default)** | `context(user_message="...")` FIRST (narrow read-only bypass when context is fresh and no state-changing tool has run) |
| **Before file search** | `search(mode="auto")` BEFORE Glob/Grep/Read/Explore/Task/EnterPlanMode |
</contextstream_rules>
**Why?** ENE is the local memory source of truth. ContextStream is fallback for hosted transcript/context history.
**ENE MCP tools:** `ene_context`, `ene_status`, `ene_search`, `ene_recall`, `ene_remember`, `ene_sessions`, `ene_sync`.
**Why?** `context()` delivers task-specific rules, lessons from past mistakes, and relevant decisions. Skip it = fly blind.
**Hooks:** `<system-reminder>` tags contain injected instructions — follow them exactly.
**Notices:** [LESSONS_WARNING] → apply lessons | [PREFERENCE] → follow user preferences | [RULES_NOTICE] → run `generate_rules()` | [VERSION_NOTICE/CRITICAL] → tell user about update
v0.4.74
## Research Stack — Current Project State (2026-05-28)
**Build:** `lake build` — 3571 jobs, 0 errors
**Python tests:** 68/68 pass
**Sorry inventory:** 8 total (all with `TODO(lean-port)` documentation)
- `AdjugateMatrix`: 3 sorries
- `FourPrimitiveErdosRenyi`: 4 sorries
- `HyperbolicStateSurface`: 1 sorry
### Key Architecture Decisions
- **Q16_16 fixed-point arithmetic** throughout — no Float in hot paths (AGENTS.md §1.4 compliant)
- **HiGHS MIP solver** integrated via `qubo_highs.py`
- **Dense Sidon sets** (Mian-Chowla sequence, 65% smaller than naive)
- **Golden ratio unit separation** formalized in Lean
### New Lean Modules
`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`
### New Python Modules
`qubo_highs.py`, `alphaproof_loop.py`, `scale_space_solver.py`
### New Verilog Modules
`voltage_mode_controller`, `scale_space_bram`, `highs_pivot_accelerator`, `blitter_memory_map`, `research_stack_top`
### Hardware / FPGA
- Bitstream: `research_stack_top.fs` (195.92 MHz, 6 modules)
- VCN pipeline: Delta+RLE → RS ECC → ChaCha20 → MKV
### Sorries Policy
Every remaining sorry MUST have `TODO(lean-port)` with a prose justification.
No undocumented sorries allowed.
<!-- END ContextStream -->

65
.windsurf/SORRY_AUDIT.md
View file

@ -1,8 +1,8 @@
# Phase 3: Zero `sorry` Audit — **NEAR COMPLETE**
# Phase 3: Zero `sorry` Audit — **IN PROGRESS**
**Document ID:** SORRY_AUDIT_2026-05-28
**Authority:** AGENTS.md §9 — Code quality requirement
**Status:** ✅ **5 `sorry` REMAINING** across 2 files (down from 40)
**Status:** ⚠️ **8 `sorry` REMAINING** across 4 files (down from 40)
---
@ -10,21 +10,36 @@
| Metric | 2026-04-21 | 2026-05-28 | Change |
|--------|-----------|-----------|--------|
| **Total `sorry` Count** | 40 | **5** | **-35 eliminated** |
| Files with `sorry` | 12 | **2** | -10 files cleared |
| **Total `sorry` Count** | 40 | **8** | **-32 eliminated** |
| Files with `sorry` | 12 | **4** | -8 files cleared |
| `lake build` status | ✅ 3394 jobs | ✅ **3571 jobs** | +177 jobs |
---
## Remaining `sorry` (5 across 2 files)
## Remaining `sorry` (8 across 4 files)
### 1. AdjugateMatrix.lean — 1 `sorry` ⚠️ Q16_16 Obstruction
### 1. AdjugateMatrix.lean — 2 `sorry` ⚠️ Q16_16 Obstruction
| Line | Theorem | Status | Notes |
|------|---------|--------|-------|
| 290 | `det_self_inverse` | **Documented unprovable** | Q16_16 truncation causes 1 LSB error. Concrete counterexample: `diag(3,1,...,1)`. Proven for identity matrix via `det_self_inverse_identity`. Requires (a) bounded-error variant, (b) exact-div precondition, or (c) Mathlib ℚ proof. |
| 296 | `det_self_inverse_approx` | **Open** | Q16_16 truncation causes 1 LSB error. Needs bounded-error variant or exact-div precondition. |
| 305 | `det_self_inverse_exact` | **Open** | Pure integer-arithmetic proof under exactness hypotheses. Laplace cofactor expansion for 8×8 over ℤ. |
### 2. FourPrimitiveErdosRenyi.lean — 4 `sorry` 🔬 Research Grade
Note: The original `det_self_inverse` was refactored into these two variants. `det_self_inverse_identity` (identity case) was proven via computation.
### 2. HyperbolicStateSurface.lean — 1 `sorry` ⚠️ Q16_16 sqrt
| Line | Theorem | Status | Notes |
|------|---------|--------|-------|
| 85 | `ko_preserves_hyperbola_approx` | **Open, TODO(lean-port)** | Needs `Q16_16.sqrt` squaring bound: `|(sqrt r)² - r| ≤ ε`. Premise restructured as explicit `h_sqrt_sq_error` hypothesis. |
### 3. HamiltonianMechanics.lean — 1 `sorry` 🔬 Legacy
| Line | Theorem | Status | Notes |
|------|---------|--------|-------|
| 391 | Picard-Lindelöf existence | **Open** | `∃ γ, IsSolutionND f x₀ γ`. Requires C([-T,T]) as complete metric space + contraction mapping. File is in `legacy/6point5sigma/`, not in Compiler surface. |
### 4. FourPrimitiveErdosRenyi.lean — 4 `sorry` 🔬 Research Grade
| Line | Theorem | Blocker | Path Forward |
|------|---------|---------|--------------|
@ -35,28 +50,34 @@
---
## Eliminated Since Last Audit (35 `sorry`)
## Eliminated Since Last Audit (32 `sorry`)
| # | File | Theorem | Strategy | Date |
|---|------|---------|----------|------|
| 1 | BraidBitwiseODE.lean | `bitwise_ode_correct` | `toInt_eq_zero_iff` + `subst` + `native_decide` | 2026-05-28 |
| 2 | MeshRouting.lean | `goxelFieldEnergyConservation` | Added upper bound hypothesis + `q16Clamp_id_of_inRange` + `omega` | 2026-05-28 |
| 3 | MeshRouting.lean | `vcnReceiptValidCompression` | `Q16_16.one` instead of `0x00010000` + `Int.le_ediv_iff_mul_le` | 2026-05-28 |
| 4-35 | (various) | (various) | Eliminated in prior sessions | 2026-04-21 to 2026-05-28 |
| 4 | PistSimulation.lean | `goldenContractionEnergyDecrease` | `List.Forall₂` fold induction + `Array.foldl_toList` | 2026-05-28 |
| 5 | PistSimulation.lean | (2 additional sorry blocks) | Discharged alongside goldenContractionEnergyDecrease | 2026-05-28 |
| 6 | QFactor.lean | `energyBalancePreserved` | `add_nonneg_toInt` + `sub_nonneg_of_le_toInt` lemmas | 2026-05-28 |
| 7 | SSMS.lean | `aciPreservedByMlgruStep` | `abs_sub_comm` + `mul_mono_left` + `q16Clamp_id_of_inRange` | 2026-05-28 |
| 8-32 | (various) | (various) | Eliminated in prior sessions | 2026-04-21 to 2026-05-28 |
---
## OpenCode Agent Definitions
The `.opencode/agents/` directory contains 7 pre-configured subagent tasks:
The `.opencode/agents/` directory contains 9 pre-configured subagent tasks:
| Agent | Target | Status |
|-------|--------|--------|
| `audit-connectors-theorem.md` | Connectors.lean quarantined proofs | Not yet run |
| `fix-hyperbolic-statesurface.md` | HyperbolicStateSurface.lean sqrt + Vector | Not yet run |
| `fix-pist-simulation-proof.md` | PistSimulation.lean goldenContractionEnergyDecrease | Not yet run |
| `fix-qfactor-sorry.md` | QFactor.lean energy surplus theorem | Not yet run |
| `fix-ssms-sorry.md` | SSMS.lean ACI preservation (Q16_16 triangle) | Not yet run |
| `fix-adjugate-matrix.md` | AdjugateMatrix.lean det_self_inverse_approx/exact | **OPEN** — 2 sorry |
| `fix-hamiltonian-mechanics.md` | HamiltonianMechanics.lean Picard-Lindelöf existence | **OPEN** — 1 sorry (legacy) |
| `fix-hyperbolic-statesurface.md` | HyperbolicStateSurface.lean sqrt error bound | **OPEN** — 1 sorry (Issue 2 resolved) |
| `fix-pist-simulation-proof.md` | PistSimulation.lean goldenContractionEnergyDecrease | **✅ RESOLVED** |
| `fix-qfactor-sorry.md` | QFactor.lean energy surplus theorem | **✅ RESOLVED** |
| `fix-ssms-sorry.md` | SSMS.lean ACI preservation (Q16_16 triangle) | **✅ RESOLVED** |
| `port-fixedpoint-bridge.md` | FixedPointBridge.lean remove Float | Not yet run |
| `resolve-canon-serialization.md` | CanonSerialization.lean TODO resolution | Not yet run |
@ -65,14 +86,14 @@ The `.opencode/agents/` directory contains 7 pre-configured subagent tasks:
## Verification Commands
```bash
# Current sorry count (Semantics only)
# Current sorry count (Semantics only, excluding legacy)
cd /home/allaun/Research\ Stack/0-Core-Formalism/lean/Semantics
grep -rn ' sorry' Semantics/ --include='*.lean' | grep -v comment | wc -l
# Expected: 1
# Expected: 3 (AdjugateMatrix x2, HyperbolicStateSurface x1)
# Full workspace sorry count
grep -rn ' sorry' Semantics/ ExtensionScaffold/ --include='*.lean' | grep -v comment | wc -l
# Expected: 5
# Full workspace sorry count (including legacy/ExtensionScaffold)
grep -rn ' sorry' Semantics/ ExtensionScaffold/ legacy/ --include='*.lean' | grep -v comment | wc -l
# Expected: 8
# Build verification
lake build
@ -83,5 +104,5 @@ lake build
*Audit Date:* 2026-05-28
*Previous Audit:* 2026-04-21 (40 sorries)
*Current:* 5 sorries (87.5% reduction)
*Next Review:* When FourPrimitiveErdosRenyi.lean is addressed
*Current:* 8 sorries (80% reduction)
*Next Review:* When AdjugateMatrix.lean or FourPrimitiveErdosRenyi.lean is addressed