Mathematics Elementary Regular Number Systems

The five canonical tiers

The elementary regular number systems are the five canonical tiers of number: the naturals ℕ, the integers ℤ, the rationals ℚ, the reals ℝ, and the complexes ℂ. Each tier adds exactly one algebraic closure step. Starting from counting, the integers add subtraction, the rationals add division, the reals add limits of convergent sequences, and the complexes add roots of polynomials. This ladder is standard mathematics, taught in every curriculum, and it is the classical surface on which the framework's structural claim rests.

The ladder has a known history. The naturals appear in Euclid's arithmetic; negative numbers were systematized in Indian mathematics by the 7th century; rationals as ratios go back to Greek geometry; the reals were made rigorous by Dedekind and Cantor in the 19th century; and the complexes, long treated as convenient fictions, gained full acceptance after Gauss and Hamilton.

In Recognition Science, the framework models these five tiers as a single finite classification. Its machine-checked library of formal theorems defines a type with exactly five members, one for each tier, and proves that the count is five. The proof is a direct computation: the library checks the finite list and confirms there are no other canonical tiers. The certificate structure packages that count as a reusable fact. This is a definitional choice, not a derived necessity; the framework chooses to recognize these five as the elementary regular systems.

The consequence is a clean boundary: the ladder stops at the complexes. There is no sixth canonical tier in this classification, because each step beyond would require a new kind of closure, not another instance of the same pattern. The framework's contribution is to make the classical five-tier ladder explicit as a finite, machine-checked object, and to anchor further structural work on that exact count.

inductive NumberSystem where
  | naturals
  | integers
  | rationals
  | reals
  | complexes
  deriving DecidableEq, Repr, BEq, Fintype

inductive NumberSystem where
  | naturals
  | integers
  | rationals
  | reals
  | complexes
  deriving DecidableEq, Repr, BEq, Fintype

theorem numberSystem_count : Fintype.card NumberSystem = 5 := by decide

structure NumberSystemCert where
  five_systems : Fintype.card NumberSystem = 5

What this page does not claim

The five-tier ladder is a derived necessity, not a definitional choice. The framework proves any algebraic property of the number systems beyond the finite count. The classification includes quaternions or any higher-dimensional system.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/ElementaryRegularNumberSystems.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: