validateKGate
plain-language theorem explainer
validateKGate defines the proposition that the tau-derived and lambda-derived estimates of the dimensionless bridge ratio K agree within the propagated measurement tolerance. Researchers auditing consistency between the two routes to K would cite this predicate when testing display equalities. It is realized as a direct definition that binds the tolerance from K_gate_tolerance and checks the absolute difference of the two K values.
Claim. For a measurement record $m$ containing measured recurrence time, kinetic length, units pack $U$, and uncertainties $σ_τ, σ_λ$, the predicate holds when $|K_τ - K_λ| < ε$, where $ε$ is the tolerance $K_{gate} √{(σ_τ/τ_{disp})^2 + (σ_λ/λ_{disp})^2}$ obtained by error propagation on the display quantities.
background
The module treats the dimensionless bridge ratio K together with display equalities that convert between recurrence time and kinetic length. K itself is the constant $φ^{1/2}$ taken from the upstream Constants.K definition. KGateMeasurement is the structure that packages a measured τ_rec, measured λ_kin, the RSUnits pack, and the two sigma uncertainties for the validation test. K_gate_tolerance implements the combined relative-error band using the display functions tau_rec_display and lambda_kin_display.
proof idea
One-line definition that first evaluates K_gate_tolerance on the measurement's units and sigma fields, then asserts that the absolute difference between the tau-route and lambda-route K values lies strictly inside that band.
why it matters
The predicate is the positive statement whose negation appears in the downstream falsifier_K_gate_mismatch. It supplies the concrete consistency check required by the K-gate validation layer inside the constants module, confirming that the two independent routes to K = φ^{1/2} remain compatible once measurement uncertainty is accounted for. This step supports the broader claim that display equalities factor through the units quotient without introducing route-dependent discrepancies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.