kGateWitness
plain-language theorem explainer
The K-gate witness is the proposition that, for every admissible RS unit system, the recognition-time display over τ₀ and the kinematic-length display over ℓ₀ both equal the same K-gate ratio. Anyone wiring the universal dimensionless pack or the inevitability scaffold cites it as the strong-CP / K-gate slot. It is a pure Prop definition; discharge is deferred to the companion units theorem.
Claim. For every RS unit system $U=(\tau_0,\ell_0,c)$ with $\tau_0\neq 0$ and $\ell_0\neq 0$, $$\frac{\tau_{\mathrm{rec}}^{\mathrm{disp}}(U)}{\tau_0}=K_{\mathrm{gate}}\quad\text{and}\quad\frac{\lambda_{\mathrm{kin}}^{\mathrm{disp}}(U)}{\ell_0}=K_{\mathrm{gate}}.$$
background
RecogSpec packages the dimensionless claims that a Recognition Science bridge must meet. The K-gate is the statement that two canonical display observables, one on the time axis and one on the length axis, collapse to one and the same dimensionless ratio once they are normalized by the fundamental tick $\tau_0$ and voxel length $\ell_0$.
RS units are the minimal structure $(\tau_0,\ell_0,c)$ with the structural law $c\cdot\tau_0=\ell_0$. The recognition-time display and kinematic-length display are the two observables whose ratios to $\tau_0$ and $\ell_0$ are compared against the fixed constant $K_{\mathrm{gate}}$. Non-vanishing of $\tau_0$ and $\ell_0$ is required so the normalizations are defined.
Upstream, $\tau_0$ is the fundamental tick and $\ell_0$ the fundamental length (voxel); in derived SI form one has relations such as $\tau_0^2=\hbar G/(\pi c^5)$. This witness does not re-derive those identities; it only names the agreement of the two normalized displays.
proof idea
Definition only: the body is the universal quantification over RS units of the conjunction of the two normalized equalities, guarded by $\tau_0\neq 0$ and $\ell_0\neq 0$. No tactics run here. The companion one-line theorem kGate_from_units discharges the proposition by applying the units-level identity K_gate_eqK for each admissible $U$.
why it matters
This proposition is the strong-CP / K-gate slot inside the explicit universal dimensionless pack: UD_explicit sets strongCP0 to exactly this witness. The inevitability scaffold then closes the dimensionless half of the story by invoking kGate_from_units, which proves the witness from RS unit identities (comment in that proof: strongCP0 = kGateWitness).
It also feeds the honest-closure certificate and the explicit dimless pack construction, so any audit of "are the two K-gate channels the same number?" routes through this Prop. In framework terms it is a consistency gate on the display layer, not a mass or coupling derivation: it locks time-side and length-side K-displays before dimensionless inevitability is asserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.