NumberSystemCert
plain-language theorem explainer
The structure bundles a cardinality assertion on the enumerated number systems with a positivity fact on the rationals. Researchers formalizing Recognition Science number systems cite it to confirm the count matches the five recognition depths. The declaration is a bare structure definition with no lemmas or computational reduction.
Claim. A record type whose fields assert that the enumerated collection of number systems has cardinality five and that the unit element satisfies $1>0$ in the rationals.
background
The module identifies five canonical number systems with recognition depths: natural numbers for discrete counts, integers for signed differences, rationals for ratios where the J-cost function is defined, reals for continuous fields, and complexes for amplitude-phase pairs. The NumberSystem inductive type enumerates these five cases and derives Fintype so that its cardinality is computable. This rests on the upstream inductive definition of NumberSystem in ElementaryRegularNumberSystems, which likewise lists naturals, integers, rationals, reals, and complexes.
proof idea
The declaration is a structure definition that directly introduces two fields; no lemmas are invoked and no tactics are applied.
why it matters
The structure is instantiated by the numberSystemCert definitions in both the present module and ElementaryRegularNumberSystems. It supplies the concrete certificate required to link the five systems to configDim D = 5 and to locate the domain of the J-cost function on positive reals, thereby supporting the Recognition Science claim that the number systems arise at successive recognition depths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.