kGate_from_units
plain-language theorem explainer
For any RS unit system with nonzero fundamental tick and length, both display-route ratios equal the canonical K-gate ratio. Dimensionless inevitability and the honest-closure certificate cite this as the strong-CP / K-gate witness. The proof is a one-line handoff to the core RSUnits K-gate equality.
Claim. For every RS unit system $U$ with $\tau_0(U)\neq 0$ and $\ell_0(U)\neq 0$, both route ratios equal the canonical K-gate ratio: $\tau_{\mathrm{rec}}^{\mathrm{display}}(U)/\tau_0(U)=K_{\mathrm{gate}}$ and $\lambda_{\mathrm{kin}}^{\mathrm{display}}(U)/\ell_0(U)=K_{\mathrm{gate}}$.
background
RecogSpec packages the Recognition Science specification as a bundle of witnesses (bands, anchors, gates) that dimensionless claims must discharge. The K-gate is the statement that the two independent display routes, one temporal and one spatial, collapse to a single dimensionless ratio once units are fixed.
RS units are the minimal triple $(\tau_0,\ell_0,c)$ with the structural relation $c\cdot\tau_0=\ell_0$. The fundamental tick is the RS-native time quantum ($\tau_0=1$ in native gauge); the voxel is the matching length quantum. Display quantities $\tau_{\mathrm{rec}}^{\mathrm{display}}$ and $\lambda_{\mathrm{kin}}^{\mathrm{display}}$ are the reconstructed period and kinematic length expressed in those units.
Upstream, K_gate_eqK already proves the two ratios separately: each equals $K_{\mathrm{gate}}$ under the nonzero hypotheses on $\tau_0$ and $\ell_0$. The present declaration simply packages that conjunction as the named witness expected by the RecogSpec interface.
proof idea
Term-mode one-line wrapper. Introduce the unit system $U$ and the two nonzero hypotheses, then apply the upstream theorem that both display ratios equal the canonical K-gate ratio. No extra algebra: the witness is definitionally that conjunction.
why it matters
Inside the inevitability scaffold, the dimensionless package is a four-way conjunction; one conjunct is exactly this K-gate witness (commented there as the strong-CP / K-gate slot). Discharging it here lets inevitability_dimless_holds close without a local proof.
The same witness is consumed by the honest-closure certificate, which records what the stack has actually proved under $\varphi$-closed observables. In the broader forcing chain the K-gate is the units-level consistency check that temporal and spatial displays agree once $c$, $\tau_0$, and $\ell_0$ are tied together, complementary to the eight-tick octave and the $D=3$ spatial forcing rather than a substitute for them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.