probabilityDisplayBridge
plain-language theorem explainer
Packages uniform counting probability on Fin(N+1) as a valid-comparison bridge from native finite events to the rationals. Cited by anyone proving that two finite events are validly comparable exactly when their counting probabilities agree. The structure fills display and native observation with the counting ratio, display observation with identity, and commutation by reflexivity.
Claim. For each $N \in \mathbb{N}$, there is a valid-comparison bridge from finite distinction events on $\mathrm{Fin}(N+1)$ into $\mathbb{Q}$, whose display map sends an event $E$ to the rational counting probability $|E|/(N+1)$. Native observation equals that same map; display observation is the identity on $\mathbb{Q}$.
background
In the primitive recognition calculus, a finite distinction event on a nonempty finite space is a predicate on $\mathrm{Fin}(N+1)$. Its uniform probability is the rational counting ratio $\mathrm{prob}(E) = |E|/(N+1)$.
A valid-comparison bridge is the structure that packages a display map from a native type into a display type, together with native and display observation maps into a common codomain, subject to a commutation identity: observing the display equals observing the native object. The module supplies concrete bridges so the abstract valid-comparison doctrine has working examples.
Upstream, the probability layer already defines the event type and the counting map; the identity map on the display codomain is the trivial observation on rationals.
proof idea
Structure-instance definition, not a multi-step proof. Display and native observation are both set to the counting probability map. Display observation is the identity on $\mathbb{Q}$. The commutation field is discharged by introducing an arbitrary event and closing with reflexivity, since both composite paths are definitionally the same map.
why it matters
Gives the finite-probability leg of the valid-comparison examples. Downstream, the iff theorem states that two events are a valid comparison under this bridge exactly when their counting probabilities agree, by reducing to the general native-observation criterion. The module headline then conjoins this with the real-display and Hilbert-display bridges, recording that the doctrine has concrete bridges for real display, finite probability display, and finite Hilbert display. In the Recognition setting this is the elementary probabilistic witness that equal displayed costs (here, equal counting ratios) are the only legitimate comparisons of finite distinction events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.