rich_transformer_closure
plain-language theorem explainer
For any rich certified-analytic registry (constants plus unary and binary protocol transformers), the generated real display values remain countable, each is witnessed by a protocol, and the native rational, add, neg, and sub constructors evaluate exactly as ordinary arithmetic. Analysts building countable certified bases for Recognition calculus cite this packaging lemma. The proof is a six-component term that assembles the already-proved countability, witness, and homomorphism facts.
Claim. Let $R$ be a rich registry (countable constants together with countable families of unary and binary protocol transformers). Write $V(R)$ for the set of real display values of finite expressions over $R$. Then $V(R)$ is countable; every $x\in V(R)$ is the display value of some protocol; rational literals evaluate as $(q:\mathbb{R})$; and evaluation intertwines addition, negation, and subtraction with the corresponding operations on $\mathbb{R}$.
background
The module develops certified analytic transformers for the Primitive Recognition Calculus: protocols that carry both a formal expression tree and a real display value, so that algebraic identities can be checked on the nose. A plain Registry already supplies countable constants and unary transformers. A RichRegistry adds a countable family of binary transformers as well, so expressions may combine two subexpressions under a registered binary map.
RichExpr is the free inductive syntax over that registry: rational literals, constant indices, unary and binary applications, and the native arithmetic constructors neg, add, sub. Evaluation sends each expression to a protocol, then to its real display value. The set of all such display values is the object whose countability and arithmetic closure are packaged here.
Upstream, the plain-registry lemmas already prove that every generated value has a protocol witness, that rationals evaluate correctly, and that native add/neg/sub are homomorphisms for the value map. The Recognition Composition Law (CostAxioms.Composition) sits in the broader foundation as the multiplicative d'Alembert constraint that forces the J-cost, but is not invoked inside this packaging step.
proof idea
Pure term-mode packaging. The goal is a six-fold conjunction. The proof supplies the six already-established components as a single anonymous constructor:
values_countable Rfor countability of the rich value set,every_value_has_protocol Rfor the protocol witness,value_rat Rfor rational literals,value_add R,value_neg R,value_sub Rfor the three arithmetic homomorphisms.
No new induction or simplification is performed; the rich-registry analogues of the plain-registry lemmas are simply collected into one statement.
why it matters
Recognition Science needs a countable, protocol-witnessed analytic basis so that continuum-looking constructions (J-cost identities, ladder evaluations, certified constants) remain finitary and machine-checkable. Extending the plain registry by binary transformers is the natural next step for composition of analytic maps; this theorem records that the extension does not break countability, witnessability, or arithmetic soundness.
It sits at the end of the RichExpr section as the closure certificate for the richer syntax. Downstream use is not yet wired in this module (used_by is empty), but any later development that treats rich expressions as a certified analytic language will cite this single conjunction rather than six separate lemmas. In the forcing chain it supports the analytic side of the foundation (T5 J-uniqueness and the Recognition Composition Law) by guaranteeing that the display values one manipulates stay inside a countable, protocol-backed set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.