NumberSystemCert
plain-language theorem explainer
The certification structure for regular number systems records that the inductive enumeration of those systems has cardinality exactly five. Workers on algebraic closure steps in the Recognition framework cite it to fix the dimension of the number-system space at five. The declaration is a bare structure with a single field and no further content.
Claim. Let $N$ be the set whose elements are the naturals, integers, rationals, reals and complexes. The certification structure for regular number systems is the record whose single field asserts that the cardinality of $N$ equals 5.
background
The module introduces five canonical number-system tiers that realize configDim $D=5$: naturals, integers, rationals, reals and complexes. Each tier is obtained from the previous one by a single canonical algebraic-closure step. The local setting is therefore the elementary enumeration of these tiers, treated as standard and structurally well-known with zero axioms or sorries.
proof idea
The declaration is a structure definition whose body consists solely of the cardinality field. Instantiation occurs in the sibling definition numberSystemCert by direct assignment of the count value.
why it matters
The structure supplies the cardinality certificate that is consumed by the two numberSystemCert definitions, one in each module. It thereby anchors the five-tier enumeration used throughout the Recognition Science treatment of number systems and their relation to configDim. No open question is closed by this declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.