compose
plain-language theorem explainer
Composition of recognition bridges: given a native-to-display bridge and a display-to-further-display bridge that both commute with the same observable protocol, their composite is again a valid bridge from native objects to the outer display. Anyone chaining comparison layers (cost morphisms, ledger neutrality, phi-forcing additivity) cites this. The construction is definitional: map composition plus a one-line transport of the outer commuting law.
Claim. Let $B_1$ be a bridge from native type $N$ to display $D$ with observables in $O$, and $B_2$ a bridge from $D$ to a further display $E$ with the same $O$. Define the composite bridge $B_2\circ B_1:N\to E$ by display map $d_2\circ d_1$, native observation $o^{\mathrm{nat}}_2\circ d_1$, and display observation $o^{\mathrm{disp}}_2$. Then for every native $n$, $o^{\mathrm{disp}}_2(d_2(d_1(n)))=o^{\mathrm{nat}}_2(d_1(n))$, so the composite satisfies the bridge commuting law.
background
A bridge packages three maps and a commuting square: a display map $N\to D$, a native observation $N\to O$, a display observation $D\to O$, and the law that observing the display of a native object recovers the native observation. The module treats valid comparisons as those that arise through a common bridge so that displayed observations agree.
Composition is the natural way to stack comparison layers: first render the native object into an intermediate display, then re-display that intermediate object. The outer bridge's native observation is applied to the intermediate display values, not to the original native type, which is why the composite native observation is $o^{\mathrm{nat}}_2\circ d_1$.
Upstream, the same Bridge structure is the local carrier; related display maps elsewhere (Hilbert amplitude display, lattice edge sets, forced $D=3$) are separate consumers of the comparison doctrine, not inputs to this definition.
proof idea
Definitional construction, not a deep proof. The composite display is ordinary function composition $B_2.\mathrm{display}\circ B_1.\mathrm{display}$. Native observation of the composite is $B_2.\mathrm{observeNative}\circ B_1.\mathrm{display}$; display observation is simply $B_2.\mathrm{observeDisplay}$.
The commuting field is discharged by a one-line tactic: for each native $n$, apply $B_2$'s commuting law at the intermediate point $B_1.\mathrm{display},n$. No extra lemmas are required beyond the structure fields of the two input bridges.
why it matters
Bridge composition is the plumbing that lets Recognition Science stack native, intermediate, and outer displays while preserving observable agreement. Downstream it is used heavily: cost-algebra morphisms, circle-winding singular simplices and path-backtrack boundaries, ledger neutral-state interfaces, the derived cost from a comparison operator, and the additive regime of $J$ for independent events all thread through composed bridges.
In the forcing picture this supports the comparison doctrine behind the Recognition Composition Law and the derived $J$-cost (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), without itself forcing $\varphi$, the eight-tick octave, or $D=3$. It is infrastructure: once bridges compose, multi-layer validity lemmas (e.g. validity of the composite comparison) can be stated once and reused across foundation and algebra modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.