mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-30 18:56:16 +00:00
dac28c1b52
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
60 lines
2.8 KiB
Markdown
60 lines
2.8 KiB
Markdown
---
|
||
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`
|