RichExpr
plain-language theorem explainer
Finite expression trees over a richer certified-analytic registry: rationals, named constants, negation, addition, subtraction, and indexed unary/binary transformers. Downstream evaluation maps each tree to a protocol and a real display value. Anyone proving countable closure of certified transformers cites this datatype. It is a pure inductive definition with derived decidable equality, representation, and countability.
Claim. A finite expression over a rich certified-analytic registry is a term built from rational literals, named constants indexed by $\mathbb{N}$, unary negation, binary addition and subtraction, and registry-indexed unary and binary transformers applied to subexpressions. The type of such expressions is countable and has decidable equality.
background
In the Primitive Recognition Calculus, real numbers that appear as display values are not free continuum objects. They are witnessed by protocols: nested rational interval approximations with a well-defined real value. Certified analytic transformers are maps on protocols that stay inside this witnessed fragment.
The richer registry packages named constant protocols together with families of unary and binary protocol transformers. Finite expressions over that registry are the syntactic objects one can build before evaluating. Constructors cover rationals, constant indices, ring operations (neg, add, sub), and applications of registry transformers by natural-number index.
Upstream protocol negation and interval negation supply the semantic meaning of the syntactic neg constructor once evaluation is defined. The module goal is to show that enriching the expression language still yields only countably many protocol-witnessed reals.
proof idea
No proof body: this is an inductive datatype declaration. The constructors are the grammar of finite rich expressions. Lean derives DecidableEq, Repr, and Countable automatically from the finitary constructors over countable parameter types ($\mathbb{Q}$ and $\mathbb{N}$). Semantic content appears only later, when eval interprets each constructor into protocol operations and registry lookups.
why it matters
This datatype is the carrier for the rich certified-analytic closure theorems. Evaluation (eval/value) interprets expressions as protocols and reals; lemmas such as value_add and value_neg show the interpretation respects arithmetic. The closure theorem rich_transformer_closure then proves the generated value set is countable, every value has a protocol witness, and arithmetic constructors evaluate as expected. The headline theorem packages countability, protocol witnessing, and associativity of unary transformer composition: adding binary transformers and finite unary compositions does not re-import the continuum. In Recognition Science terms, this keeps analytic structure inside a countable, certificate-backed fragment rather than smuggling classical continuum choice into the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.