composeUnary
plain-language theorem explainer
Ordinary left-to-right composition of two unary maps on measurement protocols: send p to f(g(p)). Anyone building finite transformer pipelines on Delta-real protocols cites this. The body is pure function composition, so associativity is definitional.
Claim. If $f$ and $g$ are unary transformers of protocols (maps $\mathrm{Protocol}\to\mathrm{Protocol}$), their composition is the unary transformer $(f\circ g)(p)=f(g(p))$.
background
In this module, a Protocol is a Delta-real: a nested family of rational intervals whose widths shrink at least as $1/(n+1)$, so a unique real is the common intersection. Unary transformers are maps Protocol → Protocol used to build certified analytic operations without smuggling in an uncountable continuum of bare reals.
The sibling registry machinery (RichRegistry, RichExpr) tracks which unary and binary transformers are admitted. Composition is the basic way to form longer unary pipelines from registered pieces. A parallel Protocol structure in RS-native measurement records extraction metadata; here the operative object is the Delta-real protocol from the foundation layer.
proof idea
Definitional one-liner: the value is the ordinary function composite fun p => f (g p). No lemmas are invoked; equality of composites is later discharged by rfl in the associativity theorem.
why it matters
This is the primitive used by composedUnary, which builds a derived unary transformer from any two registered unaries on a RichRegistry. Associativity composeUnary_assoc is immediate from the definition and is the third conjunct of certified_transformer_headline: finite compositions of unary transformers (plus binary ones) keep generated values countable and protocol-witnessed, so the analytic layer does not re-import the continuum. That headline is the local closure claim for certified transformers in the Primitive Recognition Calculus foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.