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/audit-connectors-theorem.md
Brandon Schneider ede983168c feat(lean): complete goldenContractionEnergyDecrease proof + PIST predictions pipeline v2 
- PistSimulation.lean: proven goldenContractionEnergyDecrease (no sorry)
  7 supporting lemmas, h_u'_nonneg + h_pt hypothesis, fold induction
- Connectors.lean: restored zeroIsVoid theorem with Q16_16 proof
- CanonSerialization.lean: removed dead theorem, documented blocker
- FixedPointBridge.lean: eliminated Float from compute paths

PIST predictions pipeline:
- pist_matrix_builder.py: reproducible matrix-only builder (SHA256)
- build_pist_matrices_278.py: generates PIST/Matrices278.lean
- PIST/Classify.lean: classifyProxy/classifyExact stubs (v2 surface)
- PIST/Matrices278.lean: 250-entry matrix HashMap
- build_corpus278.py: reads predictions artifact, uses classify*
- Pipeline contract documented in root AGENTS.md

Cleanup:
- Archived 5 orphan pist_* shims, 5 old route_repair variants
- Quarantined PIST/Repair.lean (no external callers)
- Created 4 opencode agents for remaining TODO items

Build: PistSimulation 3309, Compiler 3313, Full 3571 (0 errors)
2026-05-27 12:40:16 -05:00

1.1 KiB
Raw Blame History

description mode model permission
Audit the temporarily removed theorem in Connectors.lean. Use ONLY when asked to clean up Connectors.lean or evaluate quarantined proofs. subagent anthropic/claude-sonnet-4-6
edit bash read
allow allow allow

Audit Connectors.lean

Context

Semantics/Connectors.lean:94 has:

-- TODO(lean-port): proof required - theorem temporarily removed

A theorem was removed and marked for later restoration. Determine whether it should be restored, replaced, or the comment removed.

What to do

  1. Read Semantics/Connectors.lean around line 90-100.
  2. Read git history to find the removed theorem: 
    git log -p --follow -S "TODO(lean-port): proof required" -- Semantics/Connectors.lean
  3. Determine:
    • Was the theorem part of a larger proof chain that's now broken?
    • Does the theorem have any remaining callers or references?
    • Is the theorem still relevant given the current state of the module?
  4. Either restore the theorem with a complete proof, or add a note that it was evaluated and the TODO is stale, then remove the TODO.
  5. Run lake build Compiler to verify.