Vol2 Beilinson Rectification

Vol II Beilinson Rectification

Run the full local rectification loop on the live surface.

Inputs

• exact target file or theorem if given
• otherwise the smallest live surface implied by the user prompt

Mandatory loop

1. Start with a short progress update naming the target and first verification step.
2. Register a nontrivial task in update_plan.
3. Read before editing:
   • target file
   • local context
   • active \input graph from main.tex
   • current dirty diff
   • relevant compute/tests or build logs
4. Run three hostile passes:
   • RED: logic, hypotheses, signs, formulas, scope
   • BLUE: consistency, labels, status tags, duplicate formulations, build/test collisions
   • GREEN: missing definitions, dangling references, structural gaps, statements that should be weakened or split