RSObject
plain-language theorem explainer
A finite typed catalog of every mathematical object the Recognition program has constructed so far, from the finite-distinction carrier through Hilbert and manifold displays. Anyone citing the objecthood periodic table or commitment audits depends on this enumeration. It is a plain inductive definition: each constructor names one object class, with no proof obligations.
Claim. An inductive type whose constructors name the objects built by the program: the finite-distinction carrier $\mathbb{Q}_\delta$; the protocol real display $\mathbb{R}_\delta$; the classical complete field $\mathbb{R}$; the cost-scale unit $\lambda$; the physical gauge quotient; admissible observable families; the finite-generation carrier; the single coherence-forced exponent; continuum, point, space, set, equality regime, infinity mode, and function transport; finite probability and amplitude; valid comparison and conservative completion; complex scalars; finite and completed Hilbert displays; manifold and measure displays; and physical observable display objects.
background
The ObjecthoodRegistry module records what the Primitive Recognition Calculus has actually constructed, and under what epistemic commitment each construction sits. Objects are not treated as a flat ontology: each is tagged later by a commitment kind (forced, display, completion, convention, quotient, observable, permitted).
Upstream material supplies the concrete carriers being named. Cost and scale infrastructure (J-cost of recognition events, multiplicative recognizer cost, rung coarsening cost, and the $\phi^k$ scale) sit behind calibration and coherence. Certified analytic protocols expose a real-valued display map from registry expressions. Delta-real, generable-real, quotient-selection, prime-axis coherence, probability, amplitude, valid-comparison, and completion-conservativity modules each contribute one of the constructors listed here.
Local setting: this inductive is the raw catalog. The companion map commitmentOf assigns each constructor a commitment tag; audit theorems then prove the assignment matches the intended periodic table.
proof idea
No proof. The declaration is an inductive type with twenty-six nullary constructors and derived DecidableEq and Repr instances. Each constructor is a named token for one object class already built elsewhere in the foundation stack; classification and audits live in sibling definitions and theorems.
why it matters
This catalog is the carrier of the Phase 8 headline result: the periodic table of objecthood. Downstream, commitmentOf assigns each constructor a commitment kind; objecthood_periodic_table proves the core assignment (forced rationals and coherence scale, display of protocol reals, completion to classical $\mathbb{R}$, convention for the cost unit, quotient for the physical gauge). background_object_audit extends the same discipline to continuum, point, space, set, equality, infinity, function, probability, amplitude, valid comparison, and conservative completion, so background objects cannot enter untyped. display_object_extension closes the table for complex numbers, finite and infinite Hilbert spaces, manifolds, measures, and physics display objects.
In framework terms this is bookkeeping for the forcing chain's constructive residue: T5–T8 force $J$, $\phi$, the eight-tick octave, and $D=3$, but every intermediate carrier still needs an explicit objecthood tag. The inductive makes that tag space finite and decidable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.