display_null_condition
plain-language theorem explainer
The theorem establishes that for RS units with positive fundamental tick duration, the squared ratio of kinematic display wavelength to recurrence display time equals the square of the speed of light. Researchers deriving dimensionless bridge ratios K or verifying display-level Lorentz invariance in Recognition Science would cite this result. The proof is a one-line simplification that applies the prior lemma equating the unsquared ratio to c.
Claim. For an RS units structure $U$ with $0 < U.tau0$, $((lambda_kin_display U) / (tau_rec_display U))^2 = U.c^2$.
background
The module treats dimensionless bridge ratio K and display equalities. RSUnits is the structure holding fundamental time unit tau0, length unit ell0, and speed c with the relation c * tau0 = ell0. The functions lambda_kin_display and tau_rec_display come from the core module and represent the kinematic wavelength display and recurrence time display, respectively.
proof idea
The proof is a one-line term-mode simplification applying the lemma display_speed_eq_c. That lemma states that lambda_kin_display(U) / tau_rec_display(U) equals c under the same positivity hypothesis on tau0, so the squared form follows by direct algebraic reduction.
why it matters
This result supplies the null condition (lambda/tau)^2 = c^2 at the display level, supporting the K-gate units invariance and speed equalities in the same module. It contributes to the constants derivation that sets c = 1 in RS-native units and maintains the dimensionless ratios required by the Recognition framework. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.