validComparison_iff_native
plain-language theorem explainer
A comparison of two native objects through a display bridge is valid exactly when their native observables agree. Anyone working with display carriers (Hilbert, probability, real protocols) cites this to reduce display equality to the native observation protocol. The proof is a two-line unfold-and-rewrite using the bridge commuting law on each argument.
Claim. Let $B$ be a bridge from native type $N$ to display type $D$ with observable type $O$, and let $x,y\in N$. Then the display comparison of $x$ and $y$ is valid if and only if $B$'s native observation of $x$ equals $B$'s native observation of $y$.
background
In the primitive recognition calculus, a bridge packages three maps: a display map $N\to D$, a native observation $N\to O$, and a display observation $D\to O$, together with a commuting law that forces observation after display to equal native observation. Validity of a comparison is defined purely on the display side: the two displayed values must yield the same observation under the display observer.
The module isolates when such a display-side equality is legitimate rather than an artifact of the carrier. The commuting square is the only structural hypothesis; no metric, topology, or measure is assumed on $N$, $D$, or $O$.
Downstream examples instantiate the same bridge pattern for real protocols, finite probability events, and finite Hilbert displays of $F_{RS}[i]$ amplitudes, so the native/display distinction is shared infrastructure rather than ad hoc per carrier.
proof idea
Unfold the definition of valid comparison to the equality of display observations of the two displayed natives. Rewrite each side by the bridge commuting law applied at $x$ and at $y$. Both sides become native observations, and the biconditional is immediate. No external lemmas are required beyond the structure fields.
why it matters
This is the atomic legitimacy criterion for display comparisons in the recognition calculus. It feeds the composition theorem (validity under stacked bridges) and the doctrine theorem, which packages single-bridge and composite legitimacy as one statement. Concrete carriers cite it directly: real-display, probability-display, and Hilbert-norm bridges all reduce their valid-comparison predicates to native equality of values, probabilities, or Born-weight sums.
The finite Hilbert display headline uses the same bridge discipline to assert that norm comparison is valid through the native/display/observable path while preserving Born weights and normalization. In framework terms this keeps display mathematics (Hilbert space, probability) as faithful readouts of native recognition data rather than independent ontologies, consistent with the foundation layer that forces $D=3$ and the eight-tick structure elsewhere in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.