For every dispatched lemma freeze exact hypotheses, binder order, arities and expanded HA AST hash. Proposed IRD names acquire reviewed existing/new definition identities only after hygienic expansion-equivalence tests. Reject circular definitions and a definition containing its desired theorem.
Method: structural-check. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.
Planned prerequisites and notation
- No new campaign prerequisites; exact existing-premise audit still required.