probability_display_valid_iff
plain-language theorem explainer
For finite distinction events on a uniform space of size N+1, two events are validly comparable under the probability display bridge exactly when their counting probabilities agree. Cite this when grounding discrete-probability comparisons inside the valid-comparison doctrine. The proof is a one-line application of the native-equality characterization of valid comparisons.
Claim. For every natural number $N$ and events $E,F$ on the finite space $\mathrm{Fin}(N+1)$, the probability-display bridge yields a valid comparison of $E$ and $F$ if and only if their uniform probabilities agree: $\mathrm{prob}(E)=\mathrm{prob}(F)$, where $\mathrm{prob}$ is the rational counting ratio $|E|/(N+1)$.
background
In the Primitive Recognition Calculus, a finite distinction event on a nonempty space of cardinality $N+1$ is a predicate on $\mathrm{Fin}(N+1)$. Its uniform probability is the rational counting ratio of satisfying points over $N+1$.
A bridge packages a native type, a display type, and an observation map. A comparison of two native objects is valid precisely when the observations of their displays agree (both sides must come through the same bridge). The probability display bridge is the concrete instance that sends events to displayed probability values.
Upstream, the general native-equality lemma for valid comparisons states that, along any bridge whose observation recovers a native equality predicate, valid comparison is equivalent to that native equality. Here the native equality is equality of counting probabilities.
proof idea
One-line term proof: apply the general native-equality characterization of valid comparisons to the probability display bridge at the two events. That lemma reduces a valid comparison along a bridge to equality of the native observables; for this bridge the native observable is the uniform counting probability.
why it matters
Feeds the valid-comparison examples headline, which packages concrete bridges for real display, finite probability display, and finite Hilbert display as the doctrine's working examples. That headline records the three equivalences side by side; this theorem is the probability conjunct.
It places discrete probability inside the same comparison discipline used for real and Hilbert displays: two finite events are legitimately compared exactly when their counting measures agree. No open scaffolding remains; the claim is fully proved and sits at the foundation layer of the recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.