NumberSystem
plain-language theorem explainer
The inductive enumeration of five number systems tied to distinct recognition depths in Recognition Science. Researchers working on the mapping from recognition processes to number systems would cite it to ground the claim that exactly five systems match configDim D = 5. The declaration is introduced directly as an inductive type with five constructors plus standard derivations for equality and finiteness.
Claim. Let $NS$ be the inductive type whose five constructors correspond one-to-one to the natural numbers, integers, rationals, reals, and complex numbers.
background
The module states that the five canonical number systems equal configDim D = 5, with each system assigned a recognition depth: discrete counts for naturals, signed differences for integers, rational ratios (where the J-cost function is defined) for rationals, continuous fields for reals, and amplitude-phase pairs for complexes. The J-cost function itself is restricted to positive reals. This definition sits in the same module as the downstream cardinality statements and mirrors an earlier inductive enumeration of the same five systems in the ElementaryRegularNumberSystems module.
proof idea
The declaration is the inductive definition itself, listing the five constructors and attaching the deriving clauses for decidable equality, representation, boolean equality, and finiteness. No lemmas or tactics are invoked.
why it matters
It supplies the type on which the downstream NumberSystemCert structures and numberSystemCount theorems rest, both of which conclude that the cardinality equals 5. The definition therefore anchors the Recognition Science claim that number systems arise as recognition depths at configDim D = 5, with the rational case singled out as the domain of the J-cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.