K_B_obs
plain-language theorem explainer
Defines the B-route K-gate display as the constant observable whose value is the dimensionless bridge ratio $K=\varphi^{1/2}$ on every unit system. Anyone checking bridge-level K-gate equality cites it. Dimensionlessness is immediate reflexivity under anchor rescaling.
Claim. The B-route K-gate observable is the map sending every RS unit system to the constant $K=\varphi^{1/2}$, and this map is dimensionless (invariant under units rescaling with fixed $c$).
background
The Verification Bridge Core module supplies the minimal certified-surface infrastructure: units rescaling with fixed $c$, dimensionless observables, bridge evaluation, and the canonical K-gate pair. An Observable is a real-valued display $f$ on RS unit systems together with a proof that $f$ is dimensionless (unchanged under anchor rescaling).
Upstream, the constant $K$ is defined non-circularly as $K=\varphi^{1/2}$, the dimensionless bridge ratio. The companion A-route observable is the sibling constant display; both feed the bridge-level identity that the two routes agree under evaluation.
proof idea
Definitional construction, not a tactic proof. The display field is the constant function returning Constants.K. Dimensionlessness is discharged by rfl: after any units rescaling the constant is unchanged, so the two evaluations are definitionally equal.
why it matters
Supplies one half of the bridge-level K-gate. Downstream, K_gate_bridge states that bridge evaluation of the A-route and B-route observables agree identically on every unit system, proved by simplifying both constant displays. That equality is the certified-surface form of the K-gate used by RS band-invariance checks. In the broader framework $K=\varphi^{1/2}$ is the dimensionless bridge ratio tying the golden-ratio ladder to observable displays; this def packages that constant as a proper dimensionless observable so the gate can be stated without smuggling larger verification scaffolds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.