numberSystemCert
plain-language theorem explainer
This definition supplies a NumberSystemCert instance by populating the five_systems field with the result of numberSystem_count. It certifies the existence of precisely five regular number systems corresponding to the successive algebraic closures from naturals to complexes. Researchers formalizing the Recognition Science number hierarchy reference it as the elementary certificate. The implementation is a direct record construction delegating to a decided theorem.
Claim. Let NumberSystemCert be the structure asserting that the finite cardinality of the type of regular number systems equals 5. This definition supplies an instance of that structure by setting the cardinality field to the value of the count theorem.
background
The module defines five canonical number system tiers as the successive algebraic closures: natural numbers, integers, rationals, reals, and complex numbers. Each tier adds one closure step, producing a total of five systems that are treated as standard and structurally well-known. The local setting states that the Lean formalization carries zero sorries and zero axioms.
proof idea
This is a one-line definition that constructs the NumberSystemCert record by setting its five_systems field to the theorem numberSystem_count.
why it matters
This definition supplies the base certificate used by the corresponding numberSystemCert in NumberSystemsFromRS, which extends the structure with an additional rational positivity field. It fills the structural requirement for the five number systems in the Recognition Science framework, aligning with the five-dimensional configDim stated in the module. No open questions are directly touched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.