display_ratio_scale_invariant
plain-language theorem explainer
The theorem establishes that the ratio of kinematic display length to recursive display time is unchanged when both quantities are multiplied by the same positive real factor α. Researchers deriving dimensionless constants or K-gate ratios in Recognition Science would cite this invariance when confirming scale independence of display quantities. The short tactic proof cancels the common factor α after invoking nonzeroness of α and of the base tau_rec_display term.
Claim. Let $U$ be an RS unit structure with fundamental tick duration satisfying $0 < U.τ_0$. For any real $α > 0$, the scaled kinematic display length and recursive display time satisfy $λ' / τ' = λ_{kin display}(U) / τ_{rec display}(U)$, where $τ' := α · τ_{rec display}(U)$ and $λ' := α · λ_{kin display}(U)$.
background
The module treats dimensionless bridge ratios K together with display equalities. RSUnits is the structure carrying the minimal RS-native units: tau0 (fundamental tick duration), ell0 (fundamental length), and c (speed), obeying the relation c · tau0 = ell0. lambda_kin_display is the length-side kinematic display quantity defined by (2π · ell0) / (8 ln φ). tau_rec_display is the matching time-side recursive display quantity. The upstream lemma tau_rec_display_ne_zero states that tau_rec_display U is nonzero whenever U.tau0 > 0.
proof idea
The tactic proof first introduces the scaled variables tau' and lambda'. It obtains α ≠ 0 from the positivity hypothesis via ne_of_gt, and obtains tau_rec_display U ≠ 0 from the upstream lemma tau_rec_display_ne_zero. After simp on the let-bindings it rewrites the quotient using mul_div_mul_left on the nonzero factor α, which directly yields the desired equality.
why it matters
The result supplies a basic scale-invariance property for the display ratios that feed into K-gate checks and display-speed equalities inside the constants module. It supports the Recognition Science construction of dimensionless quantities built from the phi-ladder and the eight-tick octave. With zero recorded downstream uses the lemma functions as an auxiliary invariance fact rather than a terminal claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.