K_gate_bridge
plain-language theorem explainer
The two K-route observables agree under bridge evaluation for every RS unit choice: both return the same dimensionless constant K. Certified-surface and band-invariance checks cite this as the bridge-level K-gate identity. The proof is a one-line simplification unfolding bridge evaluation and the two constant observables.
Claim. For every choice of RS units $U$, bridge evaluation of the $K_A$ observable equals bridge evaluation of the $K_B$ observable. Both sides equal the fixed dimensionless constant $K$.
background
The Verification Bridge Core module supplies the minimal bridge-invariance layer for the certified surface (RS spec and band invariance). It defines unit-rescaling with fixed $c$, an Observable type (a real-valued map on RS units together with a dimensionless/anchor-invariance witness), bridge evaluation, and the canonical K-gate pair.
Bridge evaluation is the composite $A\circ Q$: on an observable $O$ and units $U$ it is simply $O.f(U)$, and is invariant under anchor rescaling by construction. The two route displays $K_A$ and $K_B$ are both defined as the constant observable with value $\mathrm{Constants}.K$ and a trivial dimensionless proof.
The local claim is therefore pure agreement of those two constant displays once they are read through the bridge, not a derivation of $K$ itself.
proof idea
Term-mode tactic proof. Introduce an arbitrary units parameter $U$, then simp with the definitions of bridge evaluation and of the two K observables. Each side reduces to $\mathrm{Constants}.K$, so the equality is reflexive. No external lemmas are required beyond those definitional unfolds.
why it matters
This is the bridge-level K-gate identity listed in the module charter: the two route displays agree identically as observables. It closes the certified-surface package that also carries units rescaling, observables, bridge evaluation, and anchor invariance, while deliberately staying outside the larger rendering and manifest scaffolds so the import closure stays small.
In the Recognition framework the K-gate is the check that alternate display routes of the same dimensionless constant coincide after bridge evaluation. Downstream certified-surface consumers can treat the two routes as interchangeable without reopening unit or anchor choices. No further parent theorems are recorded in the graph yet; the result stands as a leaf identity inside the minimal verification core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.