classify_display
plain-language theorem explainer
The display row of the objecthood registry: the protocol-to-real value map is surjective onto ℝ, and observational equality of protocols is exactly equality of those real values. Cite it when treating ℝ as the forgetful display of the ℝδ protocol interface. Proof is a direct projection of the two relevant conjuncts from the forgetful-display theorem on Δ-real protocols.
Claim. The value map from $\Delta$-real protocols to $\mathbb{R}$ is surjective, and for any two protocols $x,y$, observational equality $x \simeq_{\mathrm{obs}} y$ holds if and only if $x.v = y.v$ in $\mathbb{R}$. Thus $\mathbb{R}$ is the forgetful display of the $\mathbb{R}_\delta$ protocol interface.
background
In the Primitive Recognition Calculus, objecthood is stratified by how a carrier sits relative to cost, comparison, and display. The ObjecthoodRegistry module records each stratum (forced rationals, forced scale, display, completion, convention, quotient, observable, permitted) as a named classification theorem feeding a periodic table of object kinds.
A $\Delta$-real protocol is a structured interface whose evaluation yields a real; Protocol.value is the forgetful map sending a protocol to that real. Observational equality (ObsEq) is the protocol-level indistinguishability relation, coarser a priori than literal identity of protocols.
The upstream package is DeltaReal.Protocol.display_real_forgetful, which packages surjectivity of value, faithfulness of observational equality against value equality, and related forgetful properties. Adjacent modules (GenerableReal, ValidComparison, CompletionConservativity) supply the surrounding calculus of what can be generated, compared, and completed without smuggling continuum structure into cost-closed carriers.
proof idea
One-line wrapper. Destructure DeltaReal.Protocol.display_real_forgetful to obtain the four-component package; keep the surjectivity witness and the faithfulness biconditional (ObsEq ↔ equal value); discard the two unused conjuncts; reassemble as the required pair.
why it matters
This is the registry entry that pins the status of ordinary real numbers inside Recognition Science: ℝ is not a free-floating continuum axiom at the recognition layer, but the forgetful display of the ℝδ protocol interface, with value surjective and observationally faithful. It sits among the sibling classifiers (classify_forced_rationals, classify_forced_scale, classify_completion, classify_convention, classify_quotient, classify_observable, classify_permitted) that together build objecthood_periodic_table.
The neighboring completion classifier stresses the complementary point: completeness (LUB) is an independent axiom, not forced by any countable cost-closed carrier. Display is therefore the thin real readout; continuum strength is deferred to completion. No downstream consumers are wired yet in the graph, so the immediate role is taxonomic: fixing what "display" means before later PRC or forcing-chain arguments quote the registry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.