K_gate_check
plain-language theorem explainer
The K-gate consistency check defines a predicate that holds when the dimensionless ratios formed from a measured time interval and a measured length agree within a supplied tolerance using the RS units structure. Researchers validating unit conversions between empirical data and native RS scales would reference this predicate. The definition computes the two ratios directly from the measured inputs divided by the unit components and tests their absolute difference.
Claim. Let $t_m, l_m$ be measured time and length, let $U$ be an RS units structure with components $t_0^U$ and $l_0^U$, and let $e$ be a tolerance. The predicate holds precisely when $|t_m / t_0^U - l_m / l_0^U| < e$.
background
RSUnits is the minimal structure carrying the fundamental time unit $t_0$, length unit $l_0$, and speed $c$ obeying the relation $c t_0 = l_0$. The module centers on the dimensionless bridge ratio K together with display equalities that map measured quantities onto these native units. Upstream, $t_0$ is introduced as the tick duration and $l_0$ as the voxel size, with derivations expressing them in terms of Planck-scale constants.
proof idea
The definition is a direct construction: it forms the first ratio as the measured time divided by the time component of U, the second ratio as the measured length divided by the length component of U, and asserts that the absolute difference of these two ratios is strictly smaller than the tolerance argument.
why it matters
This predicate supplies the consistency gate for the K ratio inside the constants module and thereby supports verification of display speeds and unit-invariance statements. It links empirical measurements to the RS-native units obtained from the forcing chain (T5 J-uniqueness through T8 D=3). No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.