composeUnary_assoc
plain-language theorem explainer
Unary protocol transformers compose associatively: (f∘g)∘h equals f∘(g∘h) as maps Protocol → Protocol. Anyone citing the certified analytic transformer headline needs this algebraic fact. The proof is definitional equality via rfl on the pointwise composition.
Claim. For any maps $f,g,h$ from protocols to protocols, the unary composition satisfies $(f \circ g) \circ h = f \circ (g \circ h)$, where unary composition is the pointwise map $p \mapsto f(g(p))$.
background
In the Primitive Recognition Calculus, a Protocol is a Delta-real: a nested family of rational intervals whose widths shrink as $1/(n+1)$, so the intended real is the unique point in the intersection. Unary transformers are maps Protocol → Protocol used to build richer analytic expressions without leaving the certified, countable setting.
The local module defines composeUnary as ordinary function composition: $(f \circ g)(p) = f(g(p))$. Rich registries close under binary operations and under finite compositions of such unary maps; the goal is to keep every generated real protocol-witnessed and the value set countable.
Associativity is the standard monoid law for endofunction composition. It is recorded here so the certified transformer headline can quote it as a named lemma rather than an inline rfl.
proof idea
One-line definitional proof. After unfolding composeUnary on both sides, both expressions are the function $p \mapsto f(g(h(p)))$, so rfl closes the goal. No lemmas are applied.
why it matters
Feeds directly into certified_transformer_headline, which asserts three facts for any rich registry: the generated value set is countable, every value has a Protocol witness, and unary transformer composition is associative. The headline's doc-comment states the scientific claim: adding binary transformers and finite unary compositions does not re-import the continuum.
In the Recognition foundation this is bookkeeping, not a forcing-chain step (T0–T8). It keeps the analytic transformer layer algebraically clean so later mass-ladder and measurement-protocol work can compose certified maps without continuum leakage. No open scaffold is involved; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.