value_rat
plain-language theorem explainer
Rational literals in a rich certified-analytic expression tree display as their ordinary real embeddings. Anyone proving algebraic closure or simp-normalizing rich registry values cites this. The proof is a one-line simp wrapper through value, eval, and the Delta-real rational protocol.
Claim. For any rich registry $R$ (countable constants plus unary and binary protocol transformers) and any rational $q\in\mathbb{Q}$, the real display value of the rational-literal expression built from $q$ equals the canonical embedding $q\in\mathbb{R}$.
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). The base certified-analytic layer already has a registry of constants and transformers, with expressions that include rational literals, addition, and negation.
This module lifts that layer to a richer registry: countable families of constant protocols, unary protocol transformers, and binary protocol transformers, together with finite expression trees over them. The display map value is evaluation of the expression to a protocol, then extraction of that protocol's real.
Upstream, the plain-registry lemma already records that rational literals evaluate to their rational values via Protocol.value_ofRat. The rich-registry statement is the same identity on the enlarged expression type.
proof idea
One-line simp wrapper. Unfold the rich value (eval then protocol value), unfold eval on the rational-literal constructor, and apply Protocol.value_ofRat, which identifies the rational protocol's real with the canonical embedding of $q$. No case analysis or induction is required.
why it matters
Feeds the third conjunct of rich_transformer_closure: rich certified-analytic closure still generates only countably many display values, each protocol-witnessed, and preserves rational literals, addition, and negation under the value map. The same identity appears in the plain-registry transcendental_protocol_closure, whose doc-comment states the framework point: the continuum is not the carrier of analytic content; a certified countable protocol registry is.
In the Recognition foundation this keeps the phi-ladder constants, J-cost special values, and other RS-native rationals honest under display when expressions are built with unary and binary transformers. It is bookkeeping, not a forcing step, but without it the rich closure theorem cannot assert that rationals survive the richer syntax unchanged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.