K_ratio
plain-language theorem explainer
K_ratio supplies the explicit algebraic form of the universal dimensionless ratio K = 2π/(8 ln φ) that equates recurrence time to base time and kinetic length to base length. Workers deriving constants from the golden ratio in the RRF chain would cite this when scaling τ_rec/τ₀ or λ_kin/ℓ₀. The declaration is a direct noncomputable definition that evaluates the expression using Real.pi and Real.log on phi.
Claim. Define the universal dimensionless ratio by $K := 2π / (8 ln φ)$, where φ denotes the golden ratio. This K satisfies the gate identities τ_rec/τ₀ = K and λ_kin/ℓ₀ = K.
background
The module RRF.Foundation.Constants derives all physical constants from φ through gate identities. The local chain runs φ → E_coh → τ₀ → c → ℏ → G → α⁻¹, with the explicit K-gate stated as τ_rec/τ₀ = λ_kin/ℓ₀ = 2π/(8 ln φ). Upstream, the sibling constant K from IndisputableMonolith.Constants is defined as φ^{1/2}, while the curvature functional K(λ) = λ²/λ_rec² - 1 supplies an algebraic restatement of the balance condition used in the same derivation block.
proof idea
The declaration is a direct noncomputable definition that unfolds to the expression 2 * Real.pi / (8 * Real.log phi). No lemmas are applied; the body is the literal algebraic term.
why it matters
K_ratio supplies the concrete form of the K-gate identity listed in the module doc-comment, feeding the downstream positivity result K_ratio_pos. It closes the scaling step between base and recurrence quantities in the φ-derived constant chain that ultimately produces α⁻¹ inside the interval (137.030, 137.039). The definition therefore anchors the eight-tick octave scaling (T7) and the spatial dimension D = 3 that follow from the same forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.