commitmentOf
plain-language theorem explainer
Assigns every catalogued Recognition Science object a commitment kind: forced, permitted, quotient, completion, display, observable, or convention. This is the lookup table behind the objecthood periodic table and the background/display audits. The body is an exhaustive case split on the object constructors; no proof obligations.
Claim. Define a map $C$ from the Recognition Science object catalogue to the seven commitment kinds $\{\mathrm{forced},\,\mathrm{permitted},\,\mathrm{quotient},\,\mathrm{completion},\,\mathrm{display},\,\mathrm{observable},\,\mathrm{convention}\}$. Finite-distinction rationals, the coherence scale, and finite probability are forced; protocol reals, points, spaces, complexes, finite Hilbert space, and manifolds are displays; classical reals, continuum, infinity, infinite Hilbert space, measures, and conservative completion are completions; the cost unit is convention; physical gauge identification and equality are quotients; generable carriers, sets, and finite amplitudes are permitted; observable families, function transport, valid comparison, and physics display objects are observables.
background
The module builds an objecthood registry for Primitive Recognition Calculus: every mathematical ingredient the program uses must carry an explicit production tag, so nothing enters as untyped background.
A commitment is one of seven ways an object can arise. Forced means uniquely determined by the law (no free choice). Permitted is an admissible free choice. Quotient is identification under equivalence. Completion adds limit points by an independent closure axiom. Display is a rendering or instrument, not a native ingredient. Observable is defined by what can be measured. Convention is a gauge or labeling choice.
An RS-object is a constructor in the catalogue of built objects: finite-distinction rationals $\mathbb{Q}_\delta$, protocol reals as a value display onto $\mathbb{R}$, classical order-complete reals, the cost-scale unit $\lambda$, the physical gauge quotient, admissible observable families, finite-generation carriers, the coherence-forced prime scale, continuum/completion interfaces, and later background and display extensions (point, space, set, equality, infinity, probability, amplitude, Hilbert spaces, manifolds, measures).
proof idea
Pure definition by exhaustive pattern match. Each constructor of the object inductive is mapped to one constructor of the commitment inductive. There is no tactic proof, no lemma application, and no computational content beyond the case table itself. Downstream theorems simply evaluate this map on named constructors and conjoin the equalities.
why it matters
This map is the periodic table of objecthood itself (Phase 8 headline). The parent theorem objecthood_periodic_table packages the core assignments: distinction-forced rationals and coherence scale, display for the protocol real value map, completion for classical $\mathbb{R}$, convention for the cost unit, quotient and observable for the gauge identification and its probes, permitted for the generable inventory. Objecthood is not flat: each object is produced by a typed commitment kind.
Two audits depend on the same table. The background-object audit tags continuum, point, space, set, equality, infinity, function, probability, amplitude, valid comparison, and conservative completion so background structure cannot enter untyped. The display-object extension tags complexes, finite and infinite Hilbert spaces, manifolds, measures, and physics display objects, closing the completion-plan extension. In the broader RS forcing chain this is bookkeeping rather than a T0–T8 step, but it makes the ontology of carriers, displays, and completions machine-checkable before physics constants or the mass ladder are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.