every_value_has_protocol
plain-language theorem explainer
Every real generated by a certified analytic registry is witnessed by an explicit Delta-real protocol. Citation target for transcendental protocol closure and the countability-of-analytic-content argument. Proof is a one-line range unpacking: membership means some finite expression evaluates to that real, and evaluation itself is the protocol.
Claim. For every countable certified analytic registry $R$ and every real $x$ belonging to the set of values generated by $R$, there exists a Delta-real protocol $p$ such that the displayed value of $p$ equals $x$.
background
A registry packages a countable family of constant protocols and unary protocol transformers. Finite expression trees over those labels are the native objects; evaluation returns a protocol, never an uncountable graph. The displayed real attached to an expression is the protocol's value field, and the set of registry values is the range of that display map.
Protocols come from the Delta-real layer: certified analytic carriers whose display values are ordinary reals. The module's point is that analytic content lives on countable protocol registries, not on the continuum as a carrier. The companion countability lemma records that finite trees over countable labels yield only countably many values; the present result supplies the matching protocol witness for each such value.
proof idea
Membership $x \in \mathrm{values}(R)$ means $x$ is in the range of the display map, so there is a finite expression $e$ with $\mathrm{value}(R,e)=x$. Unpack that existential, take the protocol $\mathrm{eval}(R,e)$, and the defining equation of display gives $p.\mathrm{value}=x$. Pure construction; no analytic estimates.
why it matters
This is the witness half of transcendental protocol closure: that theorem packages countability of registry values together with a protocol for every value, plus the rational and additive display laws. The same pattern is reused for rich registries (binary transformers and unary composition) in rich transformer closure and the certified transformer headline, which state that adding those operations still keeps generated values countable and protocol-witnessed.
In the Recognition foundation this blocks continuum smuggling: analytic constants and transformers may be registered, but every displayed real remains a certified protocol object. That is the local carrier discipline behind later forcing and ladder constructions; the continuum is not treated as a free source of analytic content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.