Lean Kernel Arena / eink0rn

eink0rn — a Lean 4 kernel in Haskell, written clean-room, that normalises the surface language away before checking anything.

• One inductive type, one recursor. Nested inductives are compiled to mutual blocks and every mutual block is then flattened to a single indexed family, so the core never sees a nested occurrence or a mutual one.
• Recursors are derived, not believed. The eliminator and its iota rules are rebuilt from the inductive specification and the exported ones must match, so no export can smuggle in an unwarranted large elimination or an extra reduction rule.
• Clean room. No Lean kernel source of any kind was read — not lean4, not lean4lean, not trepplein, not nanoda. The references were Carneiro's The Type Theory of Lean, the NDJSON format specification, and this arena's verdicts.

The type theory it does implement is written down normatively in SPEC.md, and every place it knowingly departs from official Lean is argued in §12 — including the one --enforce-mutual-univ turns off below, so that the language scored here is the language every other checker is scored on. Nothing is declined; the largest export peaks around eight gigabytes.