display_null_condition
plain-language theorem explainer
The theorem establishes that the squared ratio of kinematic display wavelength to recovery display time equals the square of the speed of light for any RSUnits pack with positive fundamental tick duration. Workers deriving dimensionless constants from the Recognition Science forcing chain would cite this to confirm the null condition at the display level. The proof is a direct simplification that applies the prior speed-equality lemma.
Claim. Let $U$ be an RSUnits structure with $0 < U.tau0$. Then $((lambda_kin_display U) / (tau_rec_display U))^2 = U.c^2$.
background
RSUnits is the minimal structure holding the fundamental tick duration tau0, length ell0, and speed c together with the relation c * tau0 = ell0. The functions lambda_kin_display and tau_rec_display come from KDisplayCore and encode the kinematic wavelength and recovery time in the display setting. The module centers on the dimensionless bridge ratio K and the associated display equalities. This result rests on the upstream lemma display_speed_eq_c, which states that the unsquared ratio equals RSUnits.c U under the same positivity hypothesis on tau0.
proof idea
The proof is a one-line wrapper that applies display_speed_eq_c U h and lets simplification finish the squaring step.
why it matters
The declaration supplies the squared null form of the display-level Lorentz relation inside the constants module. It supports the Recognition Science derivation of c as the invariant speed from the T0-T8 forcing chain and the Recognition Composition Law. No downstream uses appear yet, but the result tightens the units equivalence class where c is preserved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.