display_exceeds_generation
plain-language theorem explainer
For any countable constant family κ, some real is the value of a Delta-real protocol yet lies outside the generable field of κ. Anyone tracking the ontology/display split in Primitive Recognition Calculus cites this Phase 2 headline. The proof is a two-line term: pick a non-member from properness of the generable field, then invoke surjectivity of protocol value.
Claim. For every sequence $\kappa:\mathbb{N}\to\mathbb{R}$ of named constants, there exists $r\in\mathbb{R}$ such that $r$ is the value of some Delta-real protocol (nested rational intervals with width $\le 1/(n+1)$) and $r$ does not belong to the generable field of $\kappa$.
background
A Delta-real protocol is a nested family of rational intervals whose widths shrink at least as $1/(n+1)$. Its value is the unique real in every interval (equivalently the supremum of the lower endpoints). Upstream, value is surjective onto $\mathbb{R}$: every classical real is the forgetful display of some protocol.
The generable field of a constant family $\kappa$ is the smallest field of reals closed under the field operations and containing the rationals together with the named constants $\kappa(n)$. It is countable, hence a proper subset of $\mathbb{R}$ (the sibling properness result). The local setting is Primitive Recognition Calculus: analysis may display the full continuum, while the operational ontology is only what finite generation from $\kappa$ can build.
proof idea
Term-mode, two steps. First apply the properness of the generable field: it is not equal to $\mathbb{R}$, so by the set-theoretic characterization of non-universality there is some $r\notin\mathrm{genField},\kappa$. Second, surjectivity of protocol value supplies a protocol whose value is exactly that $r$. Package the pair. No further algebra; the gap is pure cardinality plus the Phase 1 surjectivity headline.
why it matters
Phase 2 headline of the Primitive Recognition Calculus foundation: display exceeds generation. The protocol value map lands on the full continuum, while the ontology is the countable generable field; the gap is exactly the reals that exist only as display, never as finite generation. The doc-comment states the intent directly: this is the guard against smuggling uncountable ontology in through the analysis interface.
No downstream consumers are wired yet in the graph. The result sits beside the operational-carrier lemma (generable field closed under field ops, contains rationals and named constants) and completes the Phase 1/Phase 2 pair: classical $\mathbb{R}$ is forgetful display of Delta-reals, yet generation never exhausts that display. In the broader Recognition forcing chain this keeps the analytic interface honest relative to countable constructive content, without touching T5–T8 or the mass ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.