NumberSystem
Recognition Science defines five number systems inductively as natural, integer, rational, real, and complex, each representing a successive recognition depth from discrete counts through signed differences, ratios, continuous fields, to amplitude-phase pairs. Researchers deriving number systems from the J-cost function and configDim D equals 5 would cite this when establishing the complete set of systems. The definition is a direct inductive enumeration deriving decidable equality, representation, boolean equality, and finite type instances.
claimThe number systems are formalized by the inductive type with five constructors: natural (discrete recognition counts), integer (signed recognition differences), rational (rational recognition ratios), real (continuous recognition field), and complex (recognition amplitude and phase).
background
In Recognition Science, the module on number systems identifies the five canonical systems ℕ, ℤ, ℚ, ℝ, ℂ with configDim D = 5. Each corresponds to a recognition depth: natural numbers capture discrete recognition counts, integers capture signed recognition differences, rationals capture rational recognition ratios where the J-cost function applies, reals capture continuous recognition fields, and complexes capture recognition as amplitude times phase. The J-cost function is defined on positive reals, a subset of the reals.
proof idea
The declaration is a direct inductive definition enumerating the five constructors and automatically deriving the instances for DecidableEq, Repr, BEq, and Fintype. No additional proof steps or lemmas are applied.
why it matters in Recognition Science
This definition supplies the enumeration of the five number systems required for configDim D = 5. It is referenced by the NumberSystemCert structure, which requires Fintype.card of the number systems to equal 5, and by the theorem numberSystemCount, which establishes this equality by decision. The definition supports the framework's identification of number systems with recognition depths and the domain of the J-cost function on positive rationals, closing the enumeration in the mathematics module.
scope and limits
- Does not define any operations or algebraic structure on the number systems.
- Does not prove the cardinality or certification properties.
- Does not embed the recognition depth interpretations into the type.
- Does not reference the J-cost function or upstream forcing chain.
formal statement (Lean)
24inductive NumberSystem where
25 | natural | integer | rational | real | complex
26 deriving DecidableEq, Repr, BEq, Fintype
27