X_opt
plain-language theorem explainer
Optimal recognition ratio X_opt equals φ/π, the balance point between recognition cost and geometric constraint in RS inflation. Cosmologists computing phi-attractor predictions cite it when fixing the log-periodic modulation frequency Ω₀ = 2π/ln(π/φ) ≈ 9.47. The value enters as a direct noncomputable definition with no lemmas or hypotheses.
Claim. The optimal recognition ratio is defined by $X_ {rm opt} = φ/π$, where φ is the golden ratio.
background
The Inflation from phi module formalizes RS inflationary predictions from the phi-ladder and cost-functional self-similarity. The α-attractor parameter is set to φ², which replaces the generic slow-roll parameter and yields n_s ≈ 1 - 2/N together with r ≈ 12φ²/N². The optimal recognition ratio X_opt = φ/π supplies the scale for the log-periodic modulation Ω₀ = 2π/ln(1/X_opt).
proof idea
This declaration is a one-line definition that directly sets X_opt to the quotient of phi and Real.pi. No lemmas or tactics are applied.
why it matters
X_opt anchors the parameter-free inflationary chain by fixing the modulation frequency that distinguishes RS predictions. It is referenced by r_in_detectable_range, which places the tensor-to-scalar ratio inside the LiteBIRD/CMB-S4 window for N ∈ [50,60], and by X_opt_pos, which confirms positivity. The definition closes the link from the T6 phi fixed point to observable Ω₀ ≈ 9.47.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.