RichRegistry
plain-language theorem explainer
A rich registry packages three countable families of certified analytic data: constant protocols, unary protocol transformers, and binary protocol transformers. Downstream closure and headline theorems cite it as the ambient generator of finite rich expressions. It is a pure structure definition with no proof obligation.
Claim. A rich registry is a triple of maps $C:\mathbb{N}\to\mathrm{Protocol}$, $U:\mathbb{N}\to(\mathrm{Protocol}\to\mathrm{Protocol})$, and $B:\mathbb{N}\to(\mathrm{Protocol}\to\mathrm{Protocol}\to\mathrm{Protocol})$, i.e. a countable supply of constant delta-reals together with countable families of unary and binary protocol transformers.
background
In the Primitive Recognition Calculus, a Protocol (delta-real) is a nested family of rational intervals whose width at precision $n$ is at most $1/(n+1)$; the intended real is the unique point in the intersection. Certified analytic work builds reals only through such protocols, so that every displayed value carries an explicit constructive witness.
This module extends the plain certified-analytic language by allowing not only rational constants and field operations, but also a countable menu of registered constant protocols and of unary/binary transformers on protocols. The registry is the ambient data for finite expression trees (RichExpr) and their evaluation to protocols.
Upstream, Protocol supplies the carrier type; the registry itself does not choose particular transformers, only the shape of a countable catalogue from which expressions may draw.
proof idea
No proof: this is a structure declaration with three fields. Inhabitants are assembled by supplying the three maps; later lemmas quantify over an arbitrary RichRegistry and evaluate finite expressions against it.
why it matters
The registry is the parameter for the whole certified-transformer stack. Evaluation (eval/value), the protocol-witness lemma, and rich_transformer_closure all take a rich registry and show that generated display values stay countable and protocol-witnessed, with the expected rational/add/neg laws. The headline theorem packages that closure with associativity of unary composition: adding binary transformers and finite unary compositions does not re-import the continuum.
In Recognition Science terms this is foundation hygiene for the analytic layer sitting under mass ladders and constants: constructive real content must remain countable and witnessed, even after enriching the transformer language. The structure is the interface those closure results quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.