value_rat
plain-language theorem explainer
Rational literals in a certified analytic expression tree display as their ordinary real embeddings. Anyone proving registry closure, simplification, or arithmetic-preservation lemmas cites this. The proof is a one-line simp that unfolds evaluation and the rational protocol constructor.
Claim. For any countable certified-analytic registry $R$ and any rational $q\in\mathbb{Q}$, the real display value of the expression tree consisting of the rational literal $q$ equals the canonical embedding of $q$ into $\mathbb{R}$.
background
A Delta-real protocol is a nested family of rational intervals whose widths shrink at least as $1/(n+1)$. Its real value is the supremum of the lower endpoints (equivalently, the unique real in every interval). Rational constants are injected via a dedicated constructor that builds such a protocol whose value is exactly the embedded rational.
A registry packages a countable family of constant protocols and unary protocol transformers. Finite expression trees over a registry are the native objects: evaluation returns a protocol, never an uncountable graph. The value map is evaluation followed by that real display.
This lemma sits in the certified-analytic protocols layer, which keeps all analytic content countable and protocol-witnessed before any continuum carrier is introduced.
proof idea
One-line simp proof. Unfold the registry value map (evaluation then protocol display), the expression evaluator on the rational-literal constructor, and the Delta-real fact that the rational protocol's display equals the embedded rational. No case analysis or induction.
why it matters
Feeds the third conjunct of transcendental protocol closure: any countably indexed registry of certified analytic constants and transformers generates only countably many reals, each protocol-witnessed, with rationals, addition, and negation preserved under display. The same identity is restated for rich registries and appears in rich transformer closure.
In the Recognition foundation this keeps the continuum out of the carrier of analytic content: certified countable protocol registries, not bare reals, hold the analytic data. The lemma is the base case that arithmetic and transcendental generators stay honest on $\mathbb{Q}$ before counting arguments and protocol witnesses close the set of values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.