K_ratio_pos
plain-language theorem explainer
The universal ratio K defined as 2π over 8 times the natural log of φ is strictly positive. Researchers deriving constants in the Recognition Science framework cite this to confirm signs in recurrence-time and kinetic-length ratios. The proof is a term-mode reduction that unfolds the definition and chains real-number positivity lemmas for multiplication and division.
Claim. Let $K := 2π / (8 ln φ)$. Then $K > 0$.
background
The RRF Foundation module derives all constants from φ via gate identities. The derivation chain runs φ → E_coh → τ₀ → c → ℏ → G → α⁻¹. Key identities include the K-Gates: τ_rec/τ₀ = λ_kin/ℓ₀ = 2π/(8 ln φ). K_ratio is the noncomputable definition 2 * Real.pi / (8 * Real.log phi) that encodes this universal dimensionless ratio. Upstream results supply the abstract Constants bundle (with nonnegativity fields) from CPM.LawOfExistence and basic one-elements from logic and QFT modules, while positivity of π and log rely on Mathlib real-analysis facts.
proof idea
The term proof unfolds K_ratio then applies div_pos. The numerator 2 * π is shown positive by mul_pos with norm_num for 2 and Real.pi_pos. The denominator 8 * log φ is shown positive by mul_pos with norm_num for 8 and Real.log_pos applied to phi_gt_one.
why it matters
This result secures the sign of the K ratio inside the gate identities that close the Recognition Science constants derivation. It directly supports the K-Gates step in the φ-to-α⁻¹ chain listed in the module doc-comment. The factor of 8 links to the eight-tick octave (T7) and D=3 spatial dimensions (T8) in the forcing chain. No downstream uses appear yet, but the lemma completes positivity for the full constants bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.