every_value_has_protocol
plain-language theorem explainer
Every real generated by a rich certified-analytic registry is the display value of some Delta-real protocol. Closure theorems for binary and unary transformers cite this witness fact. The proof unpacks range membership and evaluates the witnessing finite expression.
Claim. Let $R$ be a rich registry (countable constants plus unary and binary protocol transformers). If $x \in \mathbb{R}$ lies in the set of values generated by evaluating finite expressions over $R$, then there exists a protocol $p$ with display value equal to $x$.
background
A rich registry packages three countable families: constant protocols, unary protocol transformers, and binary protocol transformers. Finite expressions over that registry evaluate to protocols; the associated real is the protocol's display value. The set of generated values is the range of that evaluation map.
Protocols are the Delta-real carriers of certified analytic content. The parallel fact for the thinner registry (constants and unary transformers only) already states that every registry value has a protocol witness by construction. The present statement is the same witness property after binary transformers and richer expression trees are admitted.
Local setting is the certified analytic transformer layer of Primitive Recognition Calculus: keep generated reals countable and protocol-witnessed so the continuum is not smuggled in as analytic content.
proof idea
Membership $x \in \mathrm{values}, R$ means $x$ is the evaluation of some finite rich expression $e$. Unpack that existential, take the protocol obtained by evaluating $e$ in $R$, and observe that its display value is definitionally $x$. Same shape as the thinner-registry witness theorem.
why it matters
Supplies the protocol-witness conjunct in rich transformer closure and in the certified analytic transformer headline. Those parents assert that adding binary transformers and finite unary compositions still yields only countably many display values, each protocol-witnessed, with associative unary composition. Downstream transcendental protocol closure on the thinner registry uses the same pattern: the continuum is not the carrier of analytic content; a certified countable protocol registry is. This lemma is the rich-registry half of that discipline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.