A complete finite-witness characterization of ordinary generation #
The public entry points are
GenLimit.FiniteWitness.ordinary_iff_finiteWitnesses,
GenLimit.FiniteWitness.full_characterization, and
GenLimit.FiniteWitness.universal_normalization.
All ordinary-generation definitions come from the upstream generic Core API.