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: update SORRY_AUDIT — 40→5 sorries (87.5% reduction)

Browse source
This commit is contained in:
Brandon Schneider 2026-05-28 17:25:46 -05:00
parent cf35583d17
commit a89b475f6b
1 changed files with 87 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

87
.windsurf/SORRY_AUDIT.md Normal file
View file

@ -0,0 +1,87 @@
# Phase 3: Zero `sorry` Audit — **NEAR COMPLETE**
**Document ID:** SORRY_AUDIT_2026-05-28
**Authority:** AGENTS.md §9 — Code quality requirement
**Status:** ✅ **5 `sorry` REMAINING** across 2 files (down from 40)
---
## Executive Summary
| Metric | 2026-04-21 | 2026-05-28 | Change |
|--------|-----------|-----------|--------|
| **Total `sorry` Count** | 40 | **5** | **-35 eliminated** |
| Files with `sorry` | 12 | **2** | -10 files cleared |
| `lake build` status | ✅ 3394 jobs | ✅ **3571 jobs** | +177 jobs |
---
## Remaining `sorry` (5 across 2 files)
### 1. AdjugateMatrix.lean — 1 `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. |
### 2. FourPrimitiveErdosRenyi.lean — 4 `sorry` 🔬 Research Grade
| Line | Theorem | Blocker | Path Forward |
|------|---------|---------|--------------|
| 123 | (unknown) | Needs reading | Investigate |
| 132 | (unknown) | Needs reading | Investigate |
| 141 | (unknown) | Needs reading | Investigate |
| 149 | (unknown) | Needs reading | Investigate |
---
## Eliminated Since Last Audit (35 `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 |
---
## OpenCode Agent Definitions
The `.opencode/agents/` directory contains 7 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 |
| `port-fixedpoint-bridge.md` | FixedPointBridge.lean remove Float | Not yet run |
| `resolve-canon-serialization.md` | CanonSerialization.lean TODO resolution | Not yet run |
---
## Verification Commands
```bash
# Current sorry count (Semantics only)
cd /home/allaun/Research\ Stack/0-Core-Formalism/lean/Semantics
grep -rn ' sorry' Semantics/ --include='*.lean' | grep -v comment | wc -l
# Expected: 1
# Full workspace sorry count
grep -rn ' sorry' Semantics/ ExtensionScaffold/ --include='*.lean' | grep -v comment | wc -l
# Expected: 5
# Build verification
lake build
# Expected: exit code 0, 3571 jobs
```
---
*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