[jasisz]

Four corner-cases tests, all outcome: either. This replaces #319: nested-redex-aux is unchanged from there, and vanishing-occurrence is now a corner case. My comment there was wrong: it is not a duplicate of positivity-whnf but its counterpart. There the vanishing occurrence sits under an arrow inside the field and the official kernel rejects; here it is at the head of the field, where whnf removes it, and the official kernel accepts.

• nested-redex-aux: two nested occurrences that differ only by a beta-redex give the official kernel two auxiliary types. sokonanoda rejects, by design (Valid nested inductive rejected when two nested occurrences differ only by a redex intgrah/sokonanoda#12).
• vanishing-occurrence: the type being declared occurs only inside a redex at the head of a field. In Add corner-cases/nested-redex-aux and other/vanishing-occurrence #319's CI, kefir, kefir-wasm and metalean-fast rejected it (metalean-fast reports a positivity failure), and eink0rn because the export says isRec = true while it derives false: the official kernel computes isRec without reducing, but checks positivity after reducing. The other 27 checkers accepted.
• imax-nested-absorption: imax u v = imax (imax u v) v and imax u v = imax v (imax u v) hold for every assignment, but the official kernel's normalization does not establish them. Locally the nanoda family, con-leche, con-ron, sokonanoda and nano-lean accept; official, lean4lean, Pestka, tenet and kefir reject. Unlike imax-right-successor, no right operand is a successor.
• large-elim-maybe-prop: a large recursor for MaybePropBox.{u} (α : Sort u) : Sort u | mk : α → MaybePropBox α, used by get. The official kernel only gives this type a recursor into Prop; the export uses the kernel's recursor for level u + 1, rewritten to u. It is sound because the field is a proof whenever the type is a proposition, the same argument as in proj-maybe-prop. con-leche and con-ron accept it; their rule is blockLargeElimAllowed in ConLeche/Kernel/Inductives/BlockRec.lean; everything else I ran rejects (nanoda master and nanoclo panic).

The .lean files compile with the arena toolchain (4.34.1); the .ndjson is a Lean 4.35.0 export of the u + 1 version with the recursor's level edited by hand.