NumberSystem
plain-language theorem explainer
The inductive definition enumerates the five canonical number systems as the standard tiers for successive algebraic closure. Recognition Science researchers cite it when fixing configDim D = 5 or verifying the finite cardinality of the number-system space. The declaration is a direct inductive enumeration that derives decidable equality, representation, equality, and finite-type instances with no further proof obligations.
Claim. The number systems form an inductive type whose five constructors are the natural numbers, the integers, the rational numbers, the real numbers, and the complex numbers, deriving decidable equality, representation, boolean equality, and finite-type structure.
background
The module introduces elementary regular number systems as the five canonical tiers that realize configDim D = 5. Each tier adds one algebraic closure step, yielding the sequence naturals, integers, rationals, reals, complexes. The upstream inductive definition in NumberSystemsFromRS supplies a parallel enumeration of the same five systems, differing only in constructor naming.
proof idea
The declaration is an inductive definition that introduces five constructors and immediately derives the instances DecidableEq, Repr, BEq, and Fintype. No tactic steps or lemmas are applied; the deriving clause discharges all obligations.
why it matters
This definition supplies the type whose cardinality is asserted to be five by the downstream NumberSystemCert structure and the numberSystem_count theorem. It anchors the five-system configuration inside the Recognition framework and is referenced by the parallel certification in NumberSystemsFromRS, which adds the positivity condition on the rational tier. The construction directly supports the configDim D = 5 convention stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.