NumberSystemCert
plain-language theorem explainer
NumberSystemCert packages the assertion that the inductive enumeration NumberSystem contains exactly five tiers. Algebraic number theorists or Recognition Science researchers tracking configDim would cite this structure to confirm the five-step ladder from naturals through complexes. The declaration is a bare structure definition whose single field records the Fintype cardinality.
Claim. The structure $NumberSystemCert$ consists of the field $five_systems : |NumberSystem| = 5$, where $NumberSystem$ is the inductive type whose constructors are the naturals, integers, rationals, reals, and complexes.
background
The module ElementaryRegularNumberSystems defines the inductive type NumberSystem with five constructors: naturals, integers, rationals, reals, complexes. Module documentation states these are the five canonical tiers, each adding one algebraic closure step, and equates the count to configDim D = 5. The upstream inductive NumberSystem in NumberSystemsFromRS supplies an identical five-case enumeration.
proof idea
This is a structure definition. It introduces NumberSystemCert with the single field five_systems that requires Fintype.card NumberSystem = 5. No lemmas or tactics are invoked; the declaration is self-contained.
why it matters
The structure supplies the certificate type instantiated by the downstream definitions numberSystemCert in both this module and NumberSystemsFromRS. It anchors the Recognition Science five-tier count that aligns with configDim = 5. The parallel structure in NumberSystemsFromRS augments the same field with a rational positivity condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.