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
Research-Stack/.opencode/agents/fix-pist-simulation-proof.md
Brandon Schneider dac28c1b52 docs: sync all editor rules, opencode agents, and sorry audit 
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
2026-05-28 17:53:54 -05:00

2.3 KiB
Raw Blame History

description mode model permission
Complete the goldenContractionEnergyDecrease proof in PistSimulation.lean. Use ONLY when asked to fix PistSimulation pending proofs or resolve TODO(lean-port) markers in Semantics/PistSimulation.lean. subagent anthropic/claude-sonnet-4-6
edit bash read
allow allow 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:

  • 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 was line 1614: goldenContractionEnergyDecrease — a theorem requiring Jensen's inequality for discrete convex combinations on Q16_16.

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.
  3. Attempt to complete the proof using Jensen's inequality for discrete convex combinations.
  4. If a full proof is not possible, add a detailed blocker comment explaining what lemmas are missing.
  5. Run lake build Semantics.PistSimulation to verify no build breaks.
  6. Run lake build Compiler to verify the narrow surface.

Constraints

  • Do NOT delete or comment-out the theorem — either fix the proof or leave the sorry + TODO(lean-port) intact.
  • Do NOT import Float (ofFloat) — use Q16_16.ofNat/Q16_16.ofRatio/Q16_16.ofInt.
  • If the proof requires Jensen's inequality, look for or create a convexOn lemma on Q16_16 before using generic mathlib versions.