Commitment
plain-language theorem explainer
Seven mutually exclusive commitment kinds tag how a mathematical object enters Recognition Science: forced by law, permitted free choice, quotient identification, independent completion axiom, instrument display, measurement-defined observable, or gauge convention. Downstream objecthood audits and the periodic table of RS objects cite this taxonomy. The declaration is a plain inductive enumeration with decidable equality.
Claim. There is a finite type of commitment kinds with seven constructors: uniquely forced by the law; an admissible free choice; identification under an equivalence; closure by adding limit points as an independent axiom; a rendering or instrument (not a native ingredient); defined by what can be measured; and a gauge or labeling choice. Equality of kinds is decidable.
background
The Primitive Recognition Calculus builds objects from distinctions, traces, and admissible comparisons rather than taking classical continuum machinery as primitive. Once many constructions exist (delta-rationals, protocol reals, classical completions, Hilbert displays, physical quotients), the program needs a typed answer to how each object was licensed into the theory.
Commitment is that license taxonomy. Forced means the law leaves no freedom (as with cost projectors fixed by projector axioms, or uniquely determined scales). Permitted marks an admissible free choice. Quotient records identification under an equivalence (object-level division and gauge quotients). Completion is an independent closure axiom adding limit points. Display is a rendering or instrument map (finite Hilbert display of amplitudes), not a native ingredient. Observable is fixed by measurability. Convention is a pure gauge or unit labeling choice.
The module packages these tags so background notions (continuum, point, space, set, probability, amplitude) cannot enter untyped.
proof idea
No proof body: this is an inductive definition. Seven nullary constructors name the commitment kinds, with derived DecidableEq and Repr. Downstream code pattern-matches on the constructors (as in the classification assignment from RS objects to commitment kinds) rather than proving properties of the enum itself.
why it matters
This enum is the spine of the objecthood registry. The classification map sends each catalogued RS object to one commitment; the Phase 8 headline theorem then asserts the periodic table: distinction-forced rationals and coherence scale, display for the protocol real value map, completion for classical reals, convention for the cost unit, quotient for the physical gauge quotient, and so on.
Parent results include the background-object audit (continuum as completion, point and space as display, set as permitted, equality regime as quotient) and the display-object extension (complex numbers and finite Hilbert space as display, infinite Hilbert space and measures as completion). A parallel strength-audit structure in the Strength module reuses the same discipline of typed tags on claims.
In framework terms this keeps forcing-chain content (unique J-cost, phi, eight-tick structure) cleanly separated from gauge choices, instrument layers, and independent analytic closures, so later physics claims can cite exactly which commitment underwrites each background object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.