eval
plain-language theorem explainer
Recursive evaluation sends a finite expression over a rich certified-analytic registry to a nested-interval protocol. Anyone building countable closures of analytic transformers cites it as the denotation map. The body is structural recursion on the expression constructors, dispatching to ofRat, registry lookups, and the protocol algebra (neg, add, sub, unary, binary).
Claim. Given a rich registry $R$ (countable constants and unary/binary protocol transformers) and a finite expression $e$ built from rationals, registry constants, negation, addition, subtraction, and indexed unary/binary transformers, $\mathrm{eval}(R,e)$ is the protocol obtained by interpreting each constructor via the corresponding protocol operation or registry entry.
background
In the primitive recognition calculus, a Protocol is a nested sequence of rational intervals with a width bound: a certified real presented by constructive approximations. DeltaReal supplies the base algebra: constant protocols at rationals (ofRat), and closed operations neg, add, sub that act intervalwise while preserving nesting and width control.
A RichRegistry packages a countable family of constant protocols together with countable families of unary and binary maps on protocols. RichExpr is the free finite syntax over that signature: rational leaves, constant indices, unary/binary applications, and the ring operations. The local module builds certified analytic transformers by evaluating such syntax into protocols rather than bare reals, so every value carries an explicit approximation certificate.
Upstream, PathSpace and IntegersFromLogic appear only as name collisions on const/neg in the dependency graph; the live semantics here are the DeltaReal protocol constructors and the registry fields.
proof idea
Definition by structural recursion on RichExpr. Rational leaves map to Protocol.ofRat. Constant indices look up R.const. Negation, addition, and subtraction recurse and apply Protocol.neg, Protocol.add, Protocol.sub. Unary and binary nodes recurse on subexpressions then apply R.unary k or R.binary k. No separate lemmas: the recursion equation is the definition.
why it matters
This is the denotation map for the richer certified-analytic language used in Foundation.PrimitiveRecognitionCalculus. Sibling results (value, values, every_value_has_protocol, rich_transformer_closure) rest on it: once expressions evaluate to protocols, one can prove the image is countable, closed under the registry transformers, and every value carries a protocol certificate.
In the Recognition stack, certified analytic transformers support constructive real analysis underneath J-cost geometry and the forcing chain, without floating classical choice into approximation data. The definition itself is pure scaffolding for those closure theorems rather than a physics landmark (T5–T8, RCL, phi), but it is the bridge from finite syntax to nested-interval reals those later arguments need.
No downstream edges are recorded yet; the immediate consumers are the in-module value and closure lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.