valid_comparison_examples_headline
plain-language theorem explainer
Three concrete display bridges (real protocols, finite events, finite amplitudes) make valid comparison equivalent to equality of the displayed scalar: protocol value, event probability, or total Born weight. Anyone citing the Delta-native comparison doctrine uses this as the worked example pack. The proof is a three-way product of the sibling iff lemmas.
Claim. For real protocols $x,y$, valid comparison under the real display bridge holds iff $x$ and $y$ have the same real value. For finite events $E,F$ on $\mathrm{Fin}(N+1)$, valid comparison under the probability display bridge holds iff $\mathrm{prob}(E)=\mathrm{prob}(F)$. For finite amplitudes $\psi,\varphi$, valid comparison under the Hilbert-norm bridge holds iff $\sum_i |\psi_i|^2 = \sum_i |\varphi_i|^2$.
background
Primitive Recognition Calculus treats comparison as a typed bridge from abstract carriers to displayed scalars, not bare equality of raw objects. A valid comparison is the relation induced by such a bridge: two objects compare when their displays agree.
Three sibling bridges are packaged here. The real display bridge sends a DeltaReal protocol to its evaluated real value. The probability display bridge sends a finite distinction event on $\mathrm{Fin}(N+1)$ to its probability mass. The Hilbert-norm bridge sends a finite complex amplitude to the sum of Born weights $\sum_i (\psi_i)^2$ over the finite index set.
The module collects worked examples showing that, for these bridges, the abstract valid-comparison predicate collapses exactly to equality of those displayed scalars. Upstream, Born weight is the squared component of a finite amplitude; probability is the measure of a finite event; protocol value is evaluation-then-display as a real.
proof idea
One-line term proof: the conjunction of the three sibling characterizations real_display_valid_iff, probability_display_valid_iff, and hilbert_display_valid_iff. No extra algebra; the headline is pure packaging of those iff lemmas into a single triple claim.
why it matters
This is the concrete example surface for the valid-comparison doctrine: real, probability, and Hilbert displays all reduce comparison to scalar equality. Downstream it feeds strongClosureCertificate in Delta-native strong closure, which assembles the closed theorem surface (real forgetful display, generable carriers, certified analytic protocols and transformers). In the Recognition stack it shows that the comparison layer is not vacuous: the three standard finite displays used in the calculus already satisfy the valid-comparison interface. It does not itself force J-uniqueness or the T0–T8 chain; it certifies the comparison examples those layers rely on when they talk about displayed equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.