computeRatios
plain-language theorem explainer
This definition computes the normalized clock and length ratios for a given RSUnits pack by dividing the recursive display values by the base units and converting to Float. K-gate certificate auditors cite it to extract the diagnostic data needed for invariance checks. The body consists of two structure projections, divisions in the reals, and Real.toFloat coercions.
Claim. For an RS units structure $U$, return the pair of floats obtained from $ ( {tau_rec_display}(U) / U.{tau0} , {lambda_kin_display}(U) / U.{ell0} ) $.
background
RSUnits is the structure holding base units tau0, ell0, c satisfying the relation c * tau0 = ell0. The display functions tau_rec_display and lambda_kin_display are supplied by the KDisplayCore module and implement the time-first and length-first representations. This definition lives inside the Units/K-gate Audit Certificate module, whose goal is to evaluate the K-gate identities on canonical and rescaled packs so that the resulting quotients remain dimensionless and invariant under admissible rescalings. Upstream, ell0 is defined as 1 in native units and tau0 as the fundamental tick duration.
proof idea
The definition is a direct computation: it projects tau_rec_display and lambda_kin_display from the input U, divides each by the corresponding base field of U, and applies Real.toFloat to the resulting real numbers. No lemmas or tactics are invoked beyond the structure accessors and the coercion.
why it matters
It supplies the base ratios that the UnitsKGateCert structure consumes to assemble the full certificate. This supports the K-gate audit that confirms dimensionless invariance, consistent with the Recognition Science requirement that physical ratios are scale-independent. It contributes to verification of the phi-based scaling (K = phi^{1/2}) and the fundamental units used throughout the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.