single_inequality_audit
The theorem establishes that for any RSUnits structure U with nonzero tau0 and ell0, the ratio of the recursive tau display to tau0 is at most the ratio of the kinematic lambda display to ell0. Researchers deriving dimensionless constants from the Recognition Science forcing chain would cite this to confirm that one inequality route suffices when the K-gate equality holds. The proof is a one-line wrapper that applies K_gate_eqK and rewrites both sides.
claimLet $U$ be an RSUnits structure with fundamental time unit $U.tau0$ and length $U.ell0$ both nonzero. Then $ (tau_rec_display U) / U.tau0 ≤ (lambda_kin_display U) / U.ell0 $.
background
RSUnits is the minimal structure holding the fundamental tick duration tau0, voxel length ell0, and speed c satisfying c * tau0 = ell0. The dimensionless bridge ratio K is defined non-circularly as phi to the power 1/2. The module KDisplay treats display equalities that connect recursive and kinematic routes through this K. Upstream results include the definition of tau0 as the fundamental tick duration, ell0 as the voxel length in RS-native units, and the lemma K_gate_eqK that equates the two normalized display ratios.
proof idea
The proof is a one-line wrapper. It obtains the pair of equalities from K_gate_eqK applied to U together with the nonzero hypotheses, then rewrites both sides of the target inequality using those equalities.
why it matters in Recognition Science
This audit shows that a single inequality check is enough once the K-gate equality is available, supporting consistency of the bridge ratio K = sqrt(phi) inside the constants derivation. It fills a verification step in the dimensionless bridge ratio section of the Recognition Science framework and aligns with the forcing chain landmarks that fix D = 3 and the eight-tick octave. No open scaffolding remains here; the result is fully discharged.
scope and limits
- Does not prove the numerical value of either display ratio.
- Does not apply when tau0 or ell0 vanishes.
- Does not derive the K-gate equality itself.
- Does not compare more than these two display routes.
formal statement (Lean)
75theorem single_inequality_audit (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
76 (tau_rec_display U) / U.tau0 ≤ (lambda_kin_display U) / U.ell0 := by
proof body
Term-mode proof.
77 have h := K_gate_eqK U hτ hℓ
78 rw [h.1, h.2]
79
80/-- Tolerance band for K-gate measurement -/