K_gate_ratio
plain-language theorem explainer
The K-gate ratio constant is defined as π over 4 times the natural logarithm of the golden ratio φ. It supplies the common scaling factor that normalizes both clock-side recurrence time and kinematic length displays in RS units. Researchers working on constant extraction or measurement tolerance bands cite this definition when establishing invariance under unit rescaling. It is introduced as a direct noncomputable definition with no further reduction steps.
Claim. The K-gate ratio is defined by $K = π / (4 ln φ)$, where $φ$ is the golden ratio fixed point.
background
The module introduces clock-side display definitions with the recurrence time given by τ_rec(display) = (2π τ₀) / (8 ln φ). The K-gate ratio extracts the resulting normalization factor π / (4 ln φ) that appears when dividing by the base time unit τ₀. The local setting assumes RSUnits with nonzero base scales and relies on the golden ratio φ arising as the self-similar fixed point in the forcing chain.
proof idea
The declaration is a direct definition that sets the constant equal to π divided by 4 times the natural logarithm of φ. No lemmas or tactics are invoked; the value serves as the reference for the ratio lemmas that follow.
why it matters
This definition supplies the common factor used in K_gate_eqK to equate both display ratios and in K_gate_tolerance for combined uncertainty propagation. It realizes the numerical coefficient from the eight-tick octave (T7) in the forcing chain, since the denominator 8 originates in the period 2³. The constant supports the invariance result in units_quotient_preserves_K under rescaling of base units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.