Also, Two things to document before moving on - 8 blocks, not 11. D-057 said eleven sign conditions; the Lean proof has an 8-block ψ-table plus the IIMaj bound handled separately. That's presumably the B̃₄ restructuring I flagged last time — but the archive should say so explicitly. One design note: "Lean proof diverges from D-057: 11 conditions → 8-block table + separate IIMaj″ bound; reason: B̃₄ non-concavity." Thirty minutes now, or a confused referee/future-you later. - The E-029 upgrade deserves a line in the paper. "Grid-measured 0.189 → analytically proved ≤ 1.316" is precisely the measured-to-traced conversion story the whole project is about. It belongs in the formalization appendix as a worked example.