UnitsKGateCert
plain-language theorem explainer
The UnitsKGateCert structure packages diagnostic ratios that test whether the K-gate identities remain invariant when an RS units pack is rescaled. A researcher auditing Recognition Science unit consistency would cite it to confirm that the dimensionless quotient from the time-first display equals the one from the length-first display. Construction proceeds by instantiating a canonical RSUnits pack and a doubled pack, invoking computeRatios on each, then verifying four approximate equalities at 1e-6 tolerance.
Claim. A record containing a Boolean flag, tolerance value, base and scaled clock and length ratios, and error list, such that the flag is true precisely when the τ-route ratio equals the λ-route ratio (within tolerance) for both the unit pack and its rescaling, and the base clock ratio also equals 1.
background
RSUnits is the canonical pack of recognition-science units with fundamental tick duration τ₀, voxel length ℓ₀, and speed c set to 1 in native units; the light-cone identity ℓ₀ = c · τ₀ is already established by the upstream lemma c_ell0_tau0. The K-gate compares the τ-route display (clock ratio) against the λ-route display (length ratio) and requires their quotient to be the dimensionless bridge K = φ^{1/2}. The module evaluates this invariance on the canonical pack and on a rescaled pack to certify that admissible rescalings leave the quotient unchanged.
proof idea
The fromSource definition first builds a base RSUnits pack (τ₀=1, ℓ₀=1, c=1) and a scaled pack (τ₀=2, ℓ₀=2, c=1). It calls computeRatios on each to obtain the clock and length ratios, then applies approxEq four times: base clock versus base length, base clock versus 1, scaled clock versus scaled length, and base clock versus scaled clock. The Boolean ok is the conjunction of these four checks; the record fields are populated directly from the computed ratios and the resulting error list.
why it matters
This certificate closes the audit loop for the K-gate identities that appear in the RS constants module, where K is defined as φ^{1/2}. It supports the broader forcing-chain claim that the eight-tick octave and the spatial dimension D=3 remain consistent under unit rescaling. No downstream theorems yet depend on it, so it functions as an executable witness rather than a lemma in a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.