validComparison_compose
plain-language theorem explainer
Composition of display bridges preserves legitimacy of comparisons: x and y are validly compared through B₁ then B₂ exactly when the second bridge's native observations of the two displayed values agree. Cited by anyone packaging the valid-comparison doctrine. Proof is a one-line application of the native-observation characterization to the composed bridge.
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 display $E$ with the same $O$. For $x,y\in N$, the comparison of $x$ and $y$ through the composed bridge is valid if and only if $B_2$'s native observation of $B_1(\mathrm{display}\,x)$ equals $B_2$'s native observation of $B_1(\mathrm{display}\,y)$.
background
A bridge from native objects $N$ to a display carrier $D$ with observables in $O$ packages three maps: a display map $N\to D$, a native observation protocol $N\to O$, and a display observation $D\to O$, together with the commuting law that observing the display recovers the native protocol. A display comparison of two native objects is declared valid when the two displayed values yield equal observations under that bridge.
Composition of bridges chains the display maps and reuses the second bridge's native observation on the intermediate display, so the composite still satisfies the commuting law. The sibling characterization states that validity through a single bridge is equivalent to equality of native observations; the present result lifts that equivalence to a composite bridge.
The module sits in the Primitive Recognition Calculus layer of the Foundation stack: it isolates when a comparison performed in a display carrier is legitimate relative to the native observable protocol, independent of any particular physical model.
proof idea
One-line term wrapper. Instantiate the native-observation characterization of valid comparison at the composed bridge: validity of the composite comparison is definitionally the same as equality of the composite's native observations, which unpack to $B_2$'s native observation of $B_1$'s displays of $x$ and $y$. No extra algebraic work.
why it matters
This is the composition half of the valid-comparison doctrine. The parent theorem packages two biconditionals: (i) validity through a single bridge equals native-observation equality, and (ii) validity through a composite equals native equality after the first display. The doctrine's doc-comment states the point directly: legitimacy of a display comparison "descends to equality of the native observable protocol, and this legitimacy is stable under composition of display bridges."
In the Recognition framework, displays (Hilbert completions, Clifford presentations, lattice carriers) are interchangeable only when comparisons they induce remain faithful to the native protocol. Stability under bridge composition is what lets one stack display layers without inventing new comparison criteria. It is pure Foundation bookkeeping rather than a T0–T8 forcing step, but it underwrites any later claim that two displayed amplitudes, masses, or edge counts may be compared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.