eval
plain-language theorem explainer
Recursive evaluation turns a finite expression tree over a countable analytic registry into a single Delta-real protocol. Anyone building certified real values from rationals, registered constants, and unary transformers cites this map. The definition is structural recursion on the expression constructors, wiring each node to the matching Protocol operation.
Claim. Given a countable registry $R$ of certified analytic protocol ingredients, evaluation is the unique map $\mathrm{eval}_R$ sending each finite expression $e$ to a Delta-real protocol by: rationals to $\mathrm{ofRat}$, registered constants to $R$'s $k$th constant protocol, negation/addition/subtraction to the corresponding Delta-real protocol operations, and unary nodes to $R$'s $k$th unary transformer applied to the recursively evaluated subexpression.
background
In the Primitive Recognition Calculus, real quantities are not bare reals but Delta-real protocols: certified analytic presentations that stay countable. A Registry packages a countable family of constant protocols and unary protocol transformers. Binary structure is deliberately limited to the additive operations already available on Delta-reals; further analytic binary maps can be encoded as unary transforms on paired protocols.
Expr is the free finite expression language over that registry: rational leaves, constant indices, negation, addition, subtraction, and unary applications. The design goal, stated on Expr, is that the expression tree is the native object and evaluation returns a protocol, never an uncountable graph.
Upstream, Protocol operations such as ofRat, neg, add, and sub live in DeltaReal; the registry supplies the analytic constants and unaries. The sibling value is simply display of the evaluated protocol as a real.
proof idea
Definition by structural recursion on Expr, not a theorem. Each constructor maps to the matching Protocol constructor or registry field: rat to Protocol.ofRat, const k to R.const k, neg/add/sub to Protocol.neg/add/sub on the recursive images, and unary k a to R.unary k applied to eval R a. No lemmas are invoked; well-foundedness is the inductive structure of Expr.
why it matters
This is the bridge from finite certified-analytic syntax to Delta-real protocols. Downstream, value is evaluation followed by display as a real, and the values set, countability, and every_value_has_protocol results sit on top of that pipeline. The module's transcendental_protocol_closure and related lemmas need a uniform evaluator so that closed-form analytic expressions remain inside the countable protocol universe rather than escaping into arbitrary reals.
In the Recognition foundation stack this keeps mass-ladder constants, J-cost special values, and other analytic ingredients presentable as finite certificates. It does not itself force phi or the T0-T8 chain; it is infrastructure so those forced quantities can be named and manipulated as protocols.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.