real_display_valid_iff
plain-language theorem explainer
Two Delta-real protocols compare as equal under the real display bridge exactly when they denote the same real. Anyone auditing that RS real displays preserve native equality cites this. The proof is a one-line application of the general native-bridge comparison criterion.
Claim. For Delta-real protocols $x$ and $y$, the real-display bridge yields agreeing observations if and only if the denoted reals satisfy $x = y$ as values (equivalently, $\mathrm{value}(x) = \mathrm{value}(y)$).
background
A Delta-real protocol is a nested sequence of rational intervals whose widths shrink at least as fast as $1/(n+1)$. Its denoted real is the unique point in every interval, realized as the supremum of the lower endpoints.
In the Primitive Recognition Calculus, native objects are shown to an observer only through a bridge: display maps the native type to a display type, and observeDisplay reads an observation. A comparison of two natives is valid when the two displayed observations agree.
The real display bridge is the concrete bridge that sends a Delta-real protocol to its real value as the observation. The general lemma validComparison_iff_native states that, for bridges whose observation is exactly the native value map, valid comparison is equivalent to equality of those native values.
proof idea
One-line term proof: instantiate the general native-bridge criterion on the real display bridge and the two protocols. That lemma already equates valid comparison with equality of the bridge's native values; for this bridge those values are exactly DeltaReal.value.
why it matters
This is the real-display half of the valid-comparison examples package. The parent headline theorem conjoins three concrete bridges (real, finite probability, finite Hilbert) and records that each reduces valid comparison to native equality of the corresponding observables.
In the foundation layer this pins down what "same real" means operationally: two protocols are observationally indistinguishable under real display precisely when they name the same real. That is the minimal soundness check before later layers treat displayed reals as interchangeable in forcing-chain and measurement arguments. It does not itself invoke T5--T8 or the RCL; it only certifies the display layer those later steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.