K_A_obs
plain-language theorem explainer
Defines the route-A K-gate display as the constant dimensionless bridge ratio K = φ^{1/2}, packaged as an Observable. Anyone checking bridge-level K-gate equality cites this as one of the two canonical displays. The body is a structure literal: constant function plus a trivial dimensionless proof by rfl.
Claim. The route-A K-gate observable is the map sending every unit anchor to the constant $K = \varphi^{1/2}$, together with the certificate that this display is dimensionless (invariant under anchor rescaling with fixed $c$).
background
BridgeCore is the minimal certified-surface layer for RS band invariance. It packages unit-anchor rescaling (UnitsRescaled, fixed $c$), dimensionless displays (Observable), bridge evaluation, and the canonical K-gate pair.
An Observable is a real-valued function of RS unit anchors together with a proof that the value is dimensionless: under any allowed rescaling of anchors it is unchanged. Bridge evaluation then reads the display at a chosen anchor; invariance is built in.
The constant $K$ used here is the dimensionless bridge ratio from Constants, defined non-circularly as $K = \varphi^{1/2}$. It is the shared numerical content of the two route displays compared by the K-gate.
proof idea
Definitional structure literal, not a theorem proof. The display function ignores the unit argument and returns Constants.K. Dimensionlessness is discharged by intro on any two anchors and a rescaling hypothesis, then rfl, since a constant function is automatically invariant.
why it matters
Feeds K_gate_bridge, which states that the two route displays agree identically as observables: for every anchor $U$, bridge evaluation of route A equals bridge evaluation of route B. That equality is the bridge-level K-gate on the certified surface.
In the RS framework, $K = \varphi^{1/2}$ is the dimensionless bridge ratio tying the golden-ratio fixed point (forcing chain T6) into verification infrastructure. Packaging it as a route-A observable keeps the certified import-closure small and free of the larger rendering scaffolds, while still exposing the K-gate identity used by band-invariance checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.