pq_one_minimal_cost

formal source

 211
 212    This is because J is increasing on [1,∞) and 1 + 1/φ = φ ≈ 1.618
 213    is less than 2 + 1/anything. -/
 214theorem pq_one_minimal_cost :
 215    ∀ k : ℕ, 0 < k → cfracLevelCost 1 ≤ cfracLevelCost k := by
 216  intro k hk
 217  have hk1 : (1 : ℝ) ≤ (k : ℝ) := by
 218    exact_mod_cast (Nat.succ_le_of_lt hk)
 219  have hphi_pos : 0 < phi := phi_pos
 220  have hx1 : 1 ≤ (1 : ℝ) + 1 / phi := by
 221    have : 0 ≤ 1 / phi := by positivity
 222    linarith
 223  have hxy : (1 : ℝ) + 1 / phi ≤ (k : ℝ) + 1 / phi := by
 224    linarith
 225  simpa [cfracLevelCost] using (Jcost_mono_on_one hx1 hxy)
 226
 227/-! ## §4. Rogers-Ramanujan Continued Fraction -/
 228
 229/-- The Rogers-Ramanujan continued fraction R(q) is a q-deformation
 230    of the simple φ-continued fraction.
 231
 232    As q → 0⁺: R(q) → 1 (ground state)
 233    At q = e^{-2π}: R converges to an algebraic expression in φ
 234    At q = e^{-2π√n}: R converges to algebraic expressions in φ for all n
 235
 236    The RS interpretation: q parametrizes the "recognition temperature."
 237    At T = 0 (q = 0): trivial ground state.
 238    At finite T: the partition function involves φ-algebraic expressions
 239    because the cost structure (J) forces φ as the unique fixed point. -/
 240structure RogersRamanujanSpecialValue where
 241  /-- The nome q = e^{-2π√n} for some n -/
 242  n : ℕ
 243  /-- The value is algebraic in φ -/
 244  algebraicInPhi : Prop