realDisplayBridge
plain-language theorem explainer
A concrete bridge that treats a Delta-real protocol as equal to its completed real value under valid comparison. Anyone checking when two constructive reals may be compared cites this instance. The fields are pure identity: native and display observations are both the protocol value, and the square commutes by reflexivity.
Claim. The real-display bridge is the valid-comparison bridge from Delta-real protocols to $\mathbb{R}$ whose display map sends each protocol to its denoted real value, whose native observation is that same value, and whose display observation is the identity on $\mathbb{R}$, so the observation square commutes.
background
A Delta-real protocol is a nested family of rational intervals whose width at precision $n$ is at most $1/(n+1)$. The intended quantity is the unique real common to every interval; that real is recovered as the supremum of the lower endpoints (equivalently, the unique point in the intersection).
Valid comparison is the doctrine that two native objects may be compared only after both are displayed into a common observational type, with native and display observations required to commute. A bridge packages the display map and the two observation maps together with that commuting square.
This module supplies concrete bridges for the main display targets used in the primitive recognition calculus: completed reals, finite counting probabilities, and finite Hilbert norms. The real case is the simplest: the display is already the completed value.
proof idea
Definitional construction of a bridge record. Display and native observation are both set to the Delta-real value map; display observation is the identity on $\mathbb{R}$. The commuting proof is a one-line reflexivity after introducing the protocol argument: both paths evaluate to the same real.
why it matters
Feeds the sibling theorem that two protocols are validly comparable under this bridge if and only if their real values coincide, and appears in the module headline that the doctrine has concrete bridges for real, finite-probability, and finite-Hilbert display. That headline is the existence certificate for the comparison layer of the primitive recognition calculus: without an explicit real bridge, equality of completed values would sit outside the valid-comparison interface. The construction is pure scaffolding for later analytic and mass-ladder work that needs to compare constructive reals without smuggling classical equality past the observation square.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.