NumberSystemCert
The structure NumberSystemCert packages the assertion that an inductive enumeration of elementary number systems contains exactly five members. Algebraists or formalists working on successive algebraic closures from naturals to complexes would cite the structure when fixing the count of canonical tiers. It is realized as a single-field structure whose content is supplied by a cardinality computation on the inductive type.
claimLet $N$ be the inductive type whose constructors are the naturals, integers, rationals, reals and complexes. A NumberSystemCert is the structure whose sole field asserts that the Fintype cardinality of $N$ equals 5.
background
The module defines five canonical number system tiers obtained by successive algebraic closure: naturals, integers, rationals, reals and complexes. The sibling inductive NumberSystem enumerates these five cases and derives Fintype, DecidableEq and Repr so that cardinality is immediately computable. Parallel inductive definitions appear in NumberSystemsFromRS together with an extended certificate structure that adds a positivity condition on the rationals.
proof idea
The declaration is a bare structure definition containing one field of type Fintype.card NumberSystem = 5. No lemmas or tactics are invoked inside the structure itself; the field value is supplied at each construction site by a separate cardinality lemma such as numberSystem_count.
why it matters in Recognition Science
The structure supplies the common interface used by the numberSystemCert definitions in both the elementary and RS-derived modules. These instances anchor the algebraic backbone that later constructions rely upon when introducing J-cost and the phi-ladder. It records the standard five-tier count that the Recognition framework treats as the starting point for rational-based calculations.
scope and limits
- Does not assert that these five systems exhaust all possible number systems.
- Does not encode ordering, positivity or closure properties beyond cardinality.
- Does not reference the Recognition Composition Law or any forcing-chain step.
Lean usage
def cert : NumberSystemCert where five_systems := numberSystem_countformal statement (Lean)
28structure NumberSystemCert where
29 five_systems : Fintype.card NumberSystem = 5
30