K_gate_eqK
plain-language theorem explainer
The theorem shows that for any RSUnits structure U with nonzero tau0 and ell0, the normalized recurrence display time and kinematic display wavelength both equal the fixed ratio K_gate_ratio. Researchers auditing unit-invariant constants in the Recognition Science constants layer would cite it to confirm the canonical K-gate property. The proof is a one-line wrapper that pairs the two specialized ratio lemmas via exact.
Claim. For any RS unit structure $U$ with nonzero fundamental time unit $U.tau0$ and length unit $U.ell0$, the normalized recurrence display satisfies $(tau_rec_display U)/U.tau0 = K_gate_ratio$ and the normalized kinematic display satisfies $(lambda_kin_display U)/U.ell0 = K_gate_ratio$, where $K_gate_ratio = pi/(4 ln phi)$.
background
The KDisplayCore module supplies clock-side display definitions in RS-native units. The recurrence display time is defined as tau_rec(display) = (2 pi tau0)/(8 ln phi). The structure RSUnits packages the base units tau0, ell0 and speed c satisfying the compatibility relation c tau0 = ell0. The constant K_gate_ratio is defined as pi/(4 log phi). Upstream results supply the fundamental tick duration tau0 (from both Compat and Constants) and the voxel length ell0, together with the RSUnits structure itself.
proof idea
The proof is a one-line wrapper that applies tau_rec_display_ratio U h tau and lambda_kin_display_ratio U h ell. It constructs the required conjunction directly from these two ratio lemmas using the exact tactic with a pair constructor.
why it matters
The result is invoked by single_inequality_audit to reduce a two-route inequality check to a single comparison and by units_quotient_preserves_K to establish invariance under rescaling of the base units. It supplies the canonical K-gate equality inside the KDisplayCore module, linking the eight-tick factor appearing in the display formula to the phi-based constants of the Recognition Science framework. No open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.