display_real_forgetful
plain-language theorem explainer
Classical reals arise as the forgetful value of Delta-real protocols: nested rational intervals of width at most 1/(n+1). The value map is surjective onto ℝ, fixes the rational embedding, equates observational equality with equal values, and is a ring homomorphism for add, neg, and sub. Foundation workers cite this as the Phase 1 headline that ℝ is recovered, not primitive. The proof is a six-lemma term pack.
Claim. Let a Delta-real protocol be a nested family of rational intervals with width at most $1/(n+1)$ at precision $n$, and let $\mathrm{value}$ send each protocol to its unique real. Then $\mathrm{value}$ is surjective onto $\mathbb{R}$; the constant rational protocol at $q$ has value $q$; two protocols are observationally equal (intervals overlap at every precision) if and only if their values coincide; and $\mathrm{value}$ intertwines protocol addition, negation, and subtraction with the corresponding operations on $\mathbb{R}$.
background
A Delta-real protocol is a nested sequence of rational intervals whose widths shrink at least as fast as $1/(n+1)$. The intended quantity is the unique real common to all intervals. Observational equality means the intervals of two protocols overlap at every precision level; it is the native equality before any real display is chosen.
The module recovers classical analysis from these refinement protocols rather than taking a completed continuum as primitive. The value map is the forgetful display that reads off the unique real. Upstream lemmas already establish surjectivity of value, the rational embedding identity, the equivalence of observational equality with equal values, and the three ring-homomorphism identities for add, neg, and sub on protocols.
Related certified-analytic layers reuse the same value display: native addition, negation, and subtraction on expression registries remain addition, negation, and subtraction after evaluation, by reducing to the protocol-level identities packed here.
proof idea
Pure term-mode packaging. The proof is the six-tuple of already-proved component lemmas: surjectivity of value, the ofRat value identity, the observational-equality iff value-equality theorem, and the three homomorphism facts for protocol add, neg, and sub. No new calculation; the conjunction is assembled by angle-bracket introduction of those six names.
why it matters
Phase 1 headline of the primitive recognition calculus: ℝ is not a completed primitive object but the forgetful value display of refinement protocols. Nothing in analysis needs more than rational data to any requested precision.
Downstream, strongClosureCertificate installs this statement as the deltaReal entry of the closed Delta-native theorem surface. classify_display projects out the surjectivity-plus-faithfulness half to register the display class in the objecthood registry: the protocol-real value map is surjective onto ℝ and faithful, so ℝ is the forgetful display of the ℝδ protocol interface.
In the broader Recognition stack this sits under Foundation, before mass ladders and forcing T0–T8. It licenses treating classical real arithmetic as a derived display while keeping the native carrier countable and protocol-based.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.