the specification is plain language first, Lean names in the realization table only, with a table of canonical legitimacy cases (R3)

Maintainer ruling, landed by the phase-2 round: every definition in one or two plain sentences before its mathematics; Lean names confined to the final table; eight canonical legitimacy cases from the classification rows. The spec is SPEC.md version 2 in the round directory; the phase-1 spec stays as history.