Registry
plain-language theorem explainer
A countable registry packages certified analytic ingredients as two maps: naturals to constant Delta-real protocols, and naturals to unary protocol transformers. Binary analytic work stays with the native additive structure already proved on Delta-reals. Anyone citing transcendental protocol closure or countable analytic content uses this carrier. Pure structure definition: no proof obligations.
Claim. A registry is a pair of maps $(c,u)$ with $c:\mathbb{N}\to\mathrm{Protocol}$ sending each index to a constant Delta-real protocol, and $u:\mathbb{N}\to\mathrm{Protocol}\to\mathrm{Protocol}$ sending each index to a unary transformer of protocols. Further binary analytic operations may be encoded as unary transforms on paired protocols; native addition and negation remain those of Delta-reals.
background
A Delta-real protocol 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 common to all intervals. That structure (from the Delta-real module) is the only analytic carrier used here: evaluation never returns an uncountable graph.
The local setting is certified analytic protocols inside the primitive recognition calculus. Finite expression trees (rationals, registered constants, negation, addition, subtraction) are the native objects. The registry supplies the countable menu of constants and unary transformers those trees may mention; binary protocol operations stay with the additive structure already available on protocols.
Upstream path-space constants and gravity-gap snippets appear only as dependency noise for this declaration. The mathematically load-bearing prior is the protocol structure itself and its proved additive operations.
proof idea
No proof. This is a structure declaration with two fields: a constant family indexed by naturals, and a unary transformer family indexed by naturals. Field types are plain function types into and on protocols. Downstream definitions pattern-match on expression constructors and read these fields; nothing is discharged here.
why it matters
This is the carrier for the module's main claim: transcendental protocol closure. That theorem states that any countably indexed registry of certified analytic constants and transformers generates only countably many real values, each witnessed by a Delta-real protocol, with rational literals and native add/neg behaving as expected under the value display. The continuum is not the carrier of analytic content; a certified countable protocol registry is.
Direct consumers include expression evaluation (which returns a protocol), the real-valued display of that evaluation, the set of generated values, the witness that every generated value has a protocol, and the additive/negation identities under value. Without this structure there is no place to hang a countable menu of certified ingredients, and the countability-plus-witness package cannot be stated.
In the Recognition foundation layer this keeps analytic content on countable, certifiable objects rather than on bare reals, aligning with the broader insistence that recognition data be protocol-shaped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.