K_gate_tolerance
plain-language theorem explainer
K_gate_tolerance supplies the tolerance band for checking consistency between clock-derived and length-derived values of the dimensionless bridge ratio K. Experimental checks of measurement agreement in RS units reference this definition when applying the K-gate test. The body is a direct algebraic term that scales the root-sum-square of two relative uncertainties by the fixed K_gate_ratio constant.
Claim. The tolerance band equals $K_{gate ratio} sqrt( (sigma_tau / tau_rec_display(U))^2 + (sigma_ell / lambda_kin_display(U))^2 )$, where $K_{gate ratio} = pi / (4 ln phi)$, $tau_rec_display(U) = (2 pi tau_0) / (8 ln phi)$, $lambda_kin_display(U) = (2 pi ell_0) / (8 ln phi)$, and $U$ is an RSUnits structure containing the base scales $tau_0$, $ell_0$ and speed $c$.
background
The module supplies display equalities that convert base RS units into clock and length scales for the dimensionless bridge ratio K. RSUnits is the structure holding tau0, ell0 and c subject to the relation c * tau0 = ell0. tau_rec_display and lambda_kin_display each rescale the respective base by the common factor 2 pi / (8 ln phi). K_gate_ratio is the auxiliary constant pi / (4 ln phi). K itself is defined non-circularly as phi to the power 1/2. These pieces together allow error propagation without reference to the underlying forcing steps.
proof idea
The definition is a single term-mode expression. It forms the relative uncertainties rel_tau := sigma_tau / tau_rec_display U and rel_ell := sigma_ell / lambda_kin_display U, takes the square root of their sum of squares, and multiplies the result by K_gate_ratio. The computation invokes only the definitions of K_gate_ratio, tau_rec_display and lambda_kin_display together with the field projections of RSUnits; no additional lemmas are required.
why it matters
validateKGate consumes this tolerance to assert that the absolute difference between the tau-derived and lambda-derived values of K lies inside the band. The definition therefore closes the consistency check for the bridge ratio K = sqrt(phi) inside the constants layer. It supports the numerical calibration that follows the J-uniqueness step and the self-similar fixed point phi in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.