Lean Kernel Arena / extra-rec

Proof of False from an extra recursor that no inductive declaration could produce.

The export contains False exactly as the prelude has it — an empty Prop-valued inductive with no constructors — together with its ordinary False.rec. Smuggled into the same inductive group is a second recursor, named rogue, whose type is False itself and which has no motives, no minor premises and no rules. The theorem inconsistent : False is then simply rogue.

A checker must derive the recursors of an inductive group from the inductive declaration and reject any exported recursor that is not one of them; here that fails on the name (rogue is not False.rec) as well as on the type. A checker that instead registers exported recursors as given ends up with an inhabitant of the genuine empty type.

This is a different gap from nat-rec-rules, which perturbs the rules of a legitimate recursor: here an entire recursor constant is fabricated, so validating only the rules of the recursors one expects does not catch it.