numberSystemCount
plain-language theorem explainer
Recognition Science enumerates exactly five number systems tied to successive recognition depths from discrete counts through complex amplitudes. A mathematician tracing how the J-cost domain on positive rationals forces the configuration dimension would cite this cardinality. The proof is a one-line decision procedure that applies the derived Fintype instance of the inductive enumeration.
Claim. The set consisting of the natural numbers, the integers, the rational numbers, the real numbers, and the complex numbers has cardinality five: $|$natural numbers, integers, rationals, reals, complexes$|=5$.
background
The module defines an inductive type with five constructors: natural for discrete recognition counts, integer for signed differences, rational for ratios where the J-cost function is defined, real for continuous recognition fields, and complex for amplitude-phase pairs. The J-cost function, drawn from upstream cost definitions in MultiplicativeRecognizerL4 and ObserverForcing, maps positive ratios to non-negative reals and is restricted to the rational positive domain. The module states that these five systems realize configDim D = 5.
proof idea
The proof is a term-mode one-liner that invokes the decide tactic. It relies on the Fintype instance automatically derived from the inductive definition together with its DecidableEq and BEq instances.
why it matters
This theorem supplies the five_systems field of the NumberSystemCert record in the same module. It directly realizes the module claim that five systems arise from recognition depths and supports the placement of the J-cost function on the rational positive subset. The result sits inside the chain that derives physical constants from the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.