K_gate_tolerance
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute the value of K.
- Does not incorporate systematic biases.
- Does not treat correlated errors between channels.
- Does not apply outside the RSUnits structure.
formal statement (Lean)
81noncomputable def K_gate_tolerance (U : RSUnits) (σ_tau σ_ell : ℝ) : ℝ :=
proof body
Definition body.
82 -- Combined uncertainty for K from τ_rec and λ_kin measurements
83 -- σ_K = K_gate_ratio · √((σ_τ/τ)² + (σ_ℓ/ℓ)²) (error propagation)
84 let rel_tau := σ_tau / (tau_rec_display U)
85 let rel_ell := σ_ell / (lambda_kin_display U)
86 K_gate_ratio * Real.sqrt (rel_tau^2 + rel_ell^2)
87
88/-- K-gate passes if measured values agree within tolerance -/