Expr
plain-language theorem explainer
Finite expression trees over a certified analytic registry: rationals, indexed constants, negation, addition, subtraction, and unary transformers. The tree is the native carrier of analytic content; evaluation yields a Delta-real protocol rather than an uncountable continuum object. Downstream closure theorems cite this type as the countable syntax of all generated values. The declaration is a pure inductive definition with derived equality, printing, and countability.
Claim. An inductive type of finite certified-analytic expressions with constructors: embed a rational $q\in\mathbb{Q}$; reference the $k$-th registry constant; negate an expression; add or subtract two expressions; apply the $n$-th unary transformer to an expression. The type carries decidable equality, a printable representation, and a countability instance.
background
In the Primitive Recognition Calculus, real numbers that appear in analytic arguments are not taken as bare continuum points. They are witnessed by Delta-real protocols: nested rational interval approximations with certified nesting and shrinking. A Registry packages a countable family of such certified constants together with countable unary protocol transformers.
The present inductive type is the free syntax of finite combinations of those ingredients. Rational leaves inject $\mathbb{Q}$ directly; constant leaves point into the registry by natural index; unary nodes apply a registry transformer by index; binary nodes close under addition and subtraction (with negation as a unary special case). Evaluation (defined next in the module) interprets each tree as a Protocol, never as an uncountable graph.
Upstream, Protocol.neg and interval negation supply the semantic operations that the syntax will mirror. The design keeps analytic content countable at the syntactic level before any value display to $\mathbb{R}$.
proof idea
No proof body: this is an inductive datatype declaration. The six constructors generate the free algebra of finite expression trees. Lean derives DecidableEq, Repr, and Countable automatically from the finitary constructors over countable parameter types ($\mathbb{Q}$ and $\mathbb{N}$). Semantic meaning is supplied later by the recursive evaluator eval on a Registry.
why it matters
This type is the syntactic backbone of certified analytic protocols. The evaluator eval and the real display value are defined by recursion on it; the lemmas value_add, value_neg, and value_sub show that the syntax operations commute with ordinary real arithmetic after display.
The headline consumer is transcendental_protocol_closure: any countably indexed registry generates only countably many real values, each witnessed by a Delta-real protocol. The continuum is therefore not the carrier of analytic content; a certified countable protocol registry is. Downstream, strongClosureCertificate and the FormalSystem packaging reuse the same expression language.
In Recognition Science terms, this keeps the analytic layer aligned with the countable, constructive spine of the forcing chain rather than smuggling uncountable choice into constant definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.