IR072-74 are accepted in empty context by ordinary HA and independent Lean; every dependency is authenticated, definitions expanded, full quantified endpoint retained. Only then replace planning pages with canonical exact/defined proof explorers and seek Alpha promotion/deployment.
Method: structural-check. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.