composedUnary
plain-language theorem explainer
A rich registry of certified analytic protocols carries a derived unary transformer obtained by composing any two of its registered unary maps. Workers closing the richer countable registry under finite unary composition cite this construction. It is a one-line wrapper: ordinary function composition of the two indexed unary transformers.
Claim. Given a rich registry $R$ (countable families of constant protocols, unary protocol maps, and binary protocol maps) and indices $i,j\in\mathbb{N}$, the composed unary transformer is the map $p\mapsto u_i(u_j(p))$ on protocols, where $u_k$ is the $k$-th registered unary transformer of $R$.
background
A Protocol (Delta-real) is a nested family of rational intervals whose widths shrink at least as $1/(n+1)$; the intended real is the unique point in the intersection. The certified-analytic layer builds countable registries of such protocols so that generated reals cannot smuggle in a continuum of free parameters.
A RichRegistry extends the basic registry by three countable families: constants, unary transformers (maps Protocol → Protocol), and binary transformers. The sibling composeUnary is ordinary function composition $(f\circ g)(p)=f(g(p))$. Generated values are the range of the evaluation map on finite expression trees; upstream countability results record that those trees over countable labels yield a countable value set, which is the fact that blocks continuum smuggling.
proof idea
One-line definitional wrapper. It applies composeUnary to the $i$-th and $j$-th unary transformers stored in the rich registry, yielding the map $p\mapsto R.unary,i,(R.unary,j,p)$. No tactics or lemmas beyond that abbreviation.
why it matters
Sits in the certified-analytic transformer layer whose headline is that adding binary transformers and finite compositions of unary transformers does not re-import the continuum: generated values stay countable and protocol-witnessed, and unary composition is associative. This definition supplies the derived unary map used when building finite composition towers inside RichExpr and when stating closure facts such as rich_transformer_closure and every_value_has_protocol.
In the broader Recognition foundation it keeps the analytic side of the primitive recognition calculus strictly countable, so continuum degrees of freedom cannot enter through transformer algebra before the forcing chain (J-uniqueness, phi, eight-tick, D=3) is applied. No downstream theorems are wired yet in the graph; the declaration is infrastructure for those closure statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.