falsifier_K_gate_mismatch
plain-language theorem explainer
A physicist checking consistency of the dimensionless bridge ratio K would cite this definition to express disagreement between time-first and length-first routes beyond tolerance. It supplies the concrete falsifiable condition for K-gate validation that follows from the Recognition Composition Law and the phi-ladder. The definition is a direct one-line negation of the validation predicate with no lemmas or reductions.
Claim. Let $m$ be a K-gate measurement recording recurrence time $τ_{rec}$, kinematic length $λ_{kin}$, an RS units pack, and uncertainties $σ_τ$, $σ_λ$. The proposition asserts that the absolute difference between the two independent estimates of the bridge ratio $K$ exceeds the tolerance determined by those uncertainties and units.
background
The KDisplay module develops equalities for the dimensionless bridge ratio K that arise from alternative measurement routes. KGateMeasurement packages the measured recurrence time, measured kinematic length, RS units for normalization, and the two uncertainty values. validateKGate asserts that the absolute difference of the two K estimates lies below a tolerance computed from the sigmas and units.
proof idea
This is a one-line definition that sets the proposition to the logical negation of validateKGate applied to the input measurement. No lemmas are applied and no tactics are used.
why it matters
The definition supplies a falsification criterion for K-gate agreement that supports the display speed equalities and units invariance results in the same module. It sits in the constants layer where c = 1 and other values derive from the T5 J-uniqueness through T8 forcing of three dimensions. With zero downstream dependencies it leaves open whether an observed mismatch would require revision of the tolerance or indicate a breakdown in the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.