floatAbs
plain-language theorem explainer
floatAbs supplies an inline wrapper around Float.abs for absolute differences in floating-point arithmetic. It is invoked inside approximate-equality checks when verifying that K-gate ratios remain dimensionless under admissible rescalings of RS units packs. The definition is a direct one-line alias to the standard library operation. Engineers auditing the time-first versus length-first display identities cite this helper when constructing tolerance-based certificates.
Claim. The absolute-value helper on floating-point numbers is defined by $floatAbs(x) := |x|$.
background
The UnitsKGate module evaluates K-gate identities on canonical RS units packs, comparing time-first and length-first displays and confirming that the resulting quotient is dimensionless and invariant under rescaling. The upstream structure for from UniversalForcingSelfReference records the structural properties required for meta-realization of orbit and step coherence axioms. floatAbs is introduced as a lightweight helper to support floating-point comparisons inside these invariance checks.
proof idea
one-line wrapper that applies Float.abs
why it matters
The definition feeds directly into approxEq, which performs the tolerance test for dimensionless invariance in the K-gate audit certificate. It therefore supports the overall claim that RS units packs satisfy the required quotient properties derived from the forcing chain. No open questions are closed by this helper itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.