paper: state the divergence direction as a theorem, and decide on mechanization

[lex00]

Part of #5.

What

Promote the divergence direction from #17 into a stated theorem with an argued proof, and decide whether to mechanize.

The recommendation is not to mechanize

The Onward! Papers call accepts "compelling arguments, exploratory implementations, and substantial examples" as validation. A conformance suite that two independent implementations pass, plus a differential corpus proving byte-identical output across both evaluation paths, clears that bar without a proof assistant.

Mechanize only to make the claim airtight rather than accepted. If it happens, it belongs in spec/mechanization/ with its own CI job, not wired into the default test run.

What the theorem has to survive

The two exceptions from #17. A theorem stated as clean and then caveated twice reads worse than a theorem stated with its exceptions in it. Put them in the statement.

Done when

The claim is numbered, its proof obligation is discharged by argument plus the suite, and the mechanization decision is recorded either way.

[lex00]

Per #31: the theorem to state is about identity across the fold/run boundary — that a shared entity is one object regardless of which side each referrer took — not about the fallback existing or agreeing. The fallback and same-function agreement are precedented (CTFE); the identity property is not. See spec/prior-art.md, "What survives, precisely", item 4.

[lex00]

Landed: paper/theorem.md. Theorem 1, one instance per entity, case split on g ∈ T(B) from J3 with the three assumptions named (F-Memo, F-Count, one module instance per file on the run path). Theorem 2, the permitted direction, with F-Exc-Lazy and F-Exc-Registry inside the statement, and the corollary that every other divergence costs coverage and never correctness. Mechanisation declined, reason recorded. Zero gated prose findings.