numberSystem_count
plain-language theorem explainer
The declaration establishes that the finite type NumberSystem, consisting of the five canonical algebraic number systems, has exactly five elements. Researchers working on algebraic structures in Recognition Science would reference this count when establishing the dimension of the number system hierarchy. The proof proceeds via a single decide tactic that exhausts the finite enumeration derived from the inductive constructors.
Claim. $ | { ℕ, ℤ, ℚ, ℝ, ℂ } | = 5 $
background
The module introduces NumberSystem as an inductive type whose five constructors are naturals, integers, rationals, reals and complexes; each constructor corresponds to one successive algebraic closure step and the type derives Fintype, Repr and DecidableEq. The local setting fixes configDim D = 5 for this hierarchy of regular number systems. The upstream inductive definition supplies the enumeration, while a parallel inductive appears in NumberSystemsFromRS.
proof idea
One-line wrapper that applies the decide tactic to the Fintype.card expression; the tactic succeeds immediately because the inductive type carries a derived Fintype instance with exactly five elements.
why it matters
The result supplies the five_systems field of numberSystemCert, anchoring the five-tier count inside the module. It directly implements the module's statement that five canonical tiers realize configDim D = 5 and feeds the structural count used by downstream certificates in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.