display_speed_identity
plain-language theorem explainer
The theorem asserts that in any RS units structure the ratio of the kinematic display length to the recurrence display time equals the speed parameter. Researchers confirming the internal consistency of Recognition Science display definitions would cite this identity. The proof is a direct term application of the underlying K-gate equality lemma.
Claim. For an RS units structure $U$, the ratio of the kinematic display length to the recurrence display time equals the speed parameter $c_U$.
background
RSUnits bundles the base constants tau0, ell0, and c together with the defining relation c * tau0 = ell0. The kinematic display length is defined as (2 pi ell0) / (8 ln phi) and the recurrence display time as (2 pi tau0) / (8 ln phi), where phi denotes the golden ratio. This identity sits in the TruthCore.Display module after the imports of Mathlib and Constants. It rests on the KDisplay lemma that establishes the same ratio equality under a positivity assumption on tau0.
proof idea
The proof is a one-line term that invokes the display speed equality lemma from the KDisplay module.
why it matters
This result confirms the speed identity for display quantities and supports the TruthCore layer of the Recognition framework. It aligns with the forcing chain by ensuring display ratios recover c, consistent with RS-native units where c equals 1. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.