BridgeEval
plain-language theorem explainer
Bridge evaluation applies a dimensionless observable to a choice of RS units (anchors), returning a real display value. It is the certified-surface map A∘Q: evaluate under anchors, with invariance built into the Observable structure. Anyone proving band invariance or K-gate equality cites it. The body is a one-line projection onto the observable's evaluation map.
Claim. Given a dimensionless observable $O$ (a map $f$ from RS units to $\mathbb{R}$ that is invariant under anchor rescaling with fixed $c$) and a choice of RS units $U$, the bridge evaluation is $O(U) := f(U) \in \mathbb{R}$.
background
The Verification Bridge Core module supplies the minimal certified-surface infrastructure for RS band invariance: anchor rescaling at fixed $c$, dimensionless observables, and bridge-level K-gate equality. It deliberately stays small so the certified import-closure does not pull in larger rendering scaffolds.
An Observable here is a dimensionless display: a function $f : \mathrm{RSUnits} \to \mathbb{R}$ together with a proof that $f$ is unchanged under units rescaling that keeps $c$ fixed. RS units package the elementary tick $\tau_0$, length $\ell_0$, and speed $c$ with the relation $c,\tau_0 = \ell_0$. Bridge evaluation is the act of feeding those anchors into $f$.
Upstream, RS-native units fix the gauge $\tau_0 = 1$ tick, $\ell_0 = 1$ voxel, $c = 1$. The present definition is the evaluation half of the bridge; invariance is not proved here but is carried by the dimensionless witness on the observable.
proof idea
Definition, not a proof. The body is the one-line application $O.f,U$: project the observable structure to its evaluation map and apply it to the given RS units. The @[simp] attribute makes this reduce automatically in downstream simp-driven equalities (for example the K-gate bridge).
why it matters
This is the evaluation primitive for the certified bridge surface. Downstream, anchor-invariance states that if two unit packages are related by rescaling at fixed $c$, then bridge evaluation of any observable agrees on both; the proof is exactly the dimensionless witness applied to that rescaling. The K-gate bridge theorem then shows the two canonical route displays $K_A$ and $K_B$ agree under bridge evaluation for every choice of units, by simp unfolding this definition.
In the Recognition framework this is the A∘Q layer that turns abstract dimensionless displays into concrete reals under anchors, without smuggling larger verification machinery. It does not itself force constants or dimensions (T5–T8); it only standardizes how certified observables are read once units are chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.