approxEq
plain-language theorem explainer
approxEq supplies a tolerance-based floating-point comparison for verifying invariance in RS unit ratios. K-gate auditors cite it when checking that clock and length quotients stay dimensionless after rescaling. The definition reduces directly to an absolute-difference test against the supplied bound.
Claim. For real numbers $a$, $b$ and tolerance $0 < tol$, approxEq$(a,b,tol)$ holds exactly when $|a-b|leq tol$.
background
The UnitsKGate module evaluates K-gate identities on RS units packs, confirming that time-first and length-first displays yield the same dimensionless quotient under rescaling. RSUnits is the minimal structure containing tau0, ell0 and c satisfying c * tau0 = ell0. floatAbs is the absolute-value helper that supplies the left-hand side of the comparison.
proof idea
One-line wrapper that applies floatAbs to the difference a - b and compares the result against the tolerance parameter.
why it matters
The definition supports the UnitsKGateCert structure that records diagnostic ratios for the K-gate audit. It enables verification that the quotient remains invariant, consistent with the Recognition Science requirement that admissible rescalings preserve dimensionless quantities in the RSUnits relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.