valid_comparison_doctrine
plain-language theorem explainer
A display-level comparison of native objects is legitimate exactly when the native observable protocol already equates them, and this criterion is preserved under bridge composition. Anyone building multi-layer display stacks (Hilbert displays, real forgetful maps, analytic protocols) cites this as the stability law for legitimate equality tests. The proof is a one-line pair of the native-iff lemma and the composition lemma.
Claim. For bridges $B_1:N\to D$ and $B_2:D\to E$ into a common observable type $O$, a pair $x,y\in N$ is a valid comparison under $B_1$ if and only if $B_1$'s native observations agree, and it is a valid comparison under the composite bridge if and only if $B_2$'s native observations of the $B_1$-displays agree.
background
In the Primitive Recognition Calculus, a Bridge packages a native carrier $N$, a display carrier $D$, and an observable type $O$, together with maps display, observeNative, and observeDisplay obeying the commuting law: observing the display recovers the native protocol. Validity of a comparison is then defined purely on the display side: two native points form a valid comparison when their displayed observations coincide.
Because the commuting law identifies display observation with native observation, validity is expected to collapse to native equality. Bridges also compose: if $B_1$ goes $N\to D$ and $B_2$ goes $D\to E$, the composite display is $B_2\circ B_1$ with native observation $B_2.\mathrm{observeNative}\circ B_1.\mathrm{display}$. The doctrine packages both the native collapse and its stability under that composition.
Upstream siblings supply the two halves: the native-iff characterization of valid comparison, and the corresponding statement after composition. Related display machinery (finite Hilbert displays of $F_{RS}$ amplitudes, dimension constants $D=3$) sits in neighboring foundation modules but is not required for the abstract bridge algebra here.
proof idea
Term-mode pairing of two prior lemmas. The first conjunct is exactly validComparison_iff_native applied to $B_1$: commuting rewrites display observation to native observation, so valid comparison is native equality. The second conjunct is validComparison_compose on $B_1,B_2$: after composition, valid comparison expands to equality of $B_2$'s native observations on the $B_1$-displays. No further case analysis or induction.
why it matters
This is the doctrine-level packaging of legitimate comparison in the Primitive Recognition Calculus. Downstream, strongClosureCertificate in DeltaNativeStrongClosure assembles the closed Delta-native theorem surface and needs a stable notion of which display equalities count as native facts; the doctrine supplies that stability under stacked bridges (real forgetful maps, generable carriers, certified analytic protocols).
In framework terms it is bookkeeping rather than a forcing step: it does not force $\varphi$, the eight-tick octave, or $D=3$. It does guarantee that once a native protocol is fixed, every legitimate display comparison (Hilbert vector display, real embedding, etc.) is just a rephrasing of native equality and remains so after further display layers. That keeps multi-layer certificates from inventing spurious distinctions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.