display_object_extension
plain-language theorem explainer
Six extended RS objects receive fixed commitment labels: complex numbers, finite Hilbert spaces, and manifold displays are displays; infinite Hilbert spaces and measures are completions; physics display objects are observables. Anyone citing the objecthood periodic table or the Delta-native strong-closure certificate needs this row. The proof is pure reflexivity against the commitment assignment.
Claim. Under the objecthood classification map, complex numbers, finite Hilbert spaces, and manifold displays are assigned the display commitment; infinite Hilbert spaces and measure displays are assigned the completion commitment; and physics display objects are assigned the observable commitment.
background
The ObjecthoodRegistry module maintains a periodic table of mathematical objects the Recognition program has built. Each object is an RSObject constructor; each is tagged by a Commitment saying how it enters the theory. The seven commitments are: forced (uniquely determined by the law), permitted (admissible free choice), quotient (identification under equivalence), completion (closure adding limit points, an independent axiom), display (a rendering or instrument, not a native ingredient), observable (defined by what can be measured), and convention (a gauge or labeling choice).
The map commitmentOf is the classification assignment itself. Earlier rows already place finite-distinction rationals as forced, protocol reals as display, classical reals as completion, the calibration unit as convention, and the physical quotient as quotient. This theorem extends that table to the analytic and geometric display layer: complex numbers, Hilbert spaces, manifolds, measures, and physics display objects.
Upstream, the Hilbert display completion supplies the concrete rendering of finite RS amplitudes as finite Hilbert vectors, which motivates tagging finite Hilbert structure as display rather than as a native carrier.
proof idea
Term-mode proof consisting of a six-fold pair of rfl. Each conjunct is definitional equality against the corresponding clause of commitmentOf, so no lemmas are invoked. The theorem simply reifies the table rows as a single named conjunction.
why it matters
Closes the objecthood-table extension requested by the completion plan (doc-comment). Downstream, strongClosureCertificate in DeltaNativeStrongClosure assembles the closed Delta-native theorem surface and consumes this classification so that display and completion objects sit in the right commitment slots when the certificate is built.
In framework terms this is bookkeeping, not a forcing step: it does not touch T5–T8, the RCL, or the mass ladder. It records that complex structure, finite Hilbert geometry, and manifold charts are instruments (displays), that infinite-dimensional Hilbert space and measures require genuine completion axioms, and that physics display objects are typed as observables. That separation keeps native RS carriers (finite-distinction, forced scale) cleanly apart from analytic scaffolding used only for comparison with standard physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.