feat: certify the nested inductive elimination instead of trusting it

This PR moves the elimination of nested inductive declarations out of the kernel. The kernel no longer rewrites a checked mutual model back into the nested presentation; it asks Lean for a certificate and declares the result over it, requiring every type, constructor and recursor to be realised by a definition in the environment the model was checked in, and every computation rule to hold there.

`Lean.Meta.NestedGen` builds that certificate: the model, the four bridge components relating each auxiliary copy to the type it stands for, the constructors and recursors presented as definitions over the model, and a proof of every rule the kernel states. The proofs are ordinary terms, so checking them is ordinary type checking and adds nothing to the trusted code base. The kernel states the rules itself rather than accepting them along with their proofs, so what gets proved is what is about to be believed.

Whether a declaration has a nested occurrence is now decided by the code that would unfold it, so one definition of what counts as an occurrence serves both. There is no way to turn the certificate off: the recursors the kernel declares come from it.

This subsumes the recent hardening of the old path. #14577 and #14621 type checked what the elimination dropped and re-checked what it restored; here nothing is dropped or restored, the model is checked in full, and the restored declarations have to be realised over it. #14616 reserved the `_nested` prefix because the auxiliary types lived in a kernel environment; they now live in a scratch environment that is discarded, so naming one is refused by ordinary type checking and its test is rewritten to say so.

Co-Authored-By: Claude <noreply@anthropic.com>