IsValidComparison
plain-language theorem explainer
A comparison of two native objects through a display bridge is valid exactly when the two displayed values yield the same observation. Anyone working with native-to-display bridges in the primitive recognition calculus cites this predicate. It is a one-line definition: equality of the two observe-display compositions.
Claim. Fix a bridge $B$ from native type $N$ to display type $D$ with observables in $O$, with maps $\mathrm{display}:N\to D$ and $\mathrm{observe}_{\mathrm{display}}:D\to O$. For $x,y\in N$, the comparison is valid when $\mathrm{observe}_{\mathrm{display}}(\mathrm{display}(x))=\mathrm{observe}_{\mathrm{display}}(\mathrm{display}(y))$.
background
The ambient module fixes the language of display bridges for the primitive recognition calculus. A bridge from native objects $N$ to a display carrier $D$ with observables in $O$ is a triple of maps: display $N\to D$, observe-native $N\to O$, and observe-display $D\to O$, together with a commuting law: observing the display of any native equals the native observable protocol.
Comparisons in physics are often performed on a display (Hilbert vectors, probabilities, reals) rather than on the native recognition objects. Validity asks whether that display-level equality is legitimate: both sides must come from natives through the same bridge, and the displayed observations must agree. Because the bridge commutes, this is equivalent to equality of the native observables (proved downstream).
Related constants such as spatial dimension $D=3$ (T8/T9) appear elsewhere in the foundation stack; this definition itself is pure type-level comparison infrastructure and does not fix $D$.
proof idea
Definition, not a theorem. The predicate is the propositional equality of the two composite maps $n\mapsto \mathrm{observe}_{\mathrm{display}}(\mathrm{display}(n))$ evaluated at the two natives. No tactics or lemmas are applied; unfolding is the entire content.
why it matters
This predicate is the atomic legitimacy check for display-side comparisons in Recognition Science. Downstream, validComparison_iff_native rewrites it to native-observable equality via the bridge commuting law, and valid_comparison_doctrine packages that equivalence with stability under bridge composition: a display comparison is legitimate exactly when it descends to the native protocol, and composition of bridges preserves the criterion.
Concrete carriers use it directly. The finite Hilbert display headline states that finite Hilbert space is a display of native $F_{RS}[i]$ amplitudes preserving Born weights, squared norm, and normalization, with norm comparison valid through the bridge. Example lemmas specialize the predicate to Hilbert-norm, probability, and real displays (Born-weight sums, event probabilities, etc.). Without a shared validity notion, those display theorems would not connect back to native recognition objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.