display_rate_matches_structural_rate
plain-language theorem explainer
The equality establishes that the kinematic display wavelength divided by recursive display time equals the structural ell0 over tau0 ratio for any RSUnits structure. Researchers deriving rate transformations in the Recognition Science constants module would cite it to confirm invariance of the bridge ratio K under display mappings. The proof is a tactic sequence that unfolds the two display definitions then cancels the shared 2 pi over 8 log phi factor via ring rewrites and a nonzero multiplier lemma.
Claim. For any RSUnits structure $U$, $$frac{lambda_{kin,display}(U)}{tau_{rec,display}(U)} = frac{ell_0(U)}{tau_0(U)}$$.
background
RSUnits is the structure that packages the fundamental length ell0, fundamental time tau0, and speed c together with the defining relation c * tau0 = ell0. The functions lambda_kin_display and tau_rec_display appear in the sibling module KDisplayCore and are given explicitly as 2 pi ell0 over 8 log phi and 2 pi tau0 over 8 log phi. The present module treats dimensionless bridge ratio K and the associated display equalities that convert structural constants into display-level rates.
proof idea
simp unfolds lambda_kin_display and tau_rec_display. Separate have statements establish 0 < log phi from one_lt_phi, nonzeroness of 8 log phi and of 2 pi, and the two ring rewrites that factor out the common multiplier 2 pi over 8 log phi. The nonzero factor is shown to be nonzero, after which mul_div_mul_right cancels it to leave ell0 over tau0.
why it matters
The result confirms that the display kinematic ratio remains null, matching the structural c and thereby supporting the display-level Lorentz structure noted in the module. It supplies one of the concrete equalities required by the K bridge construction in Constants.KDisplay. No downstream uses are recorded yet, but the equality closes a necessary step for any later rate-transformation lemmas that rely on display derivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.