214theorem pq_one_minimal_cost : 215 ∀ k : ℕ, 0 < k → cfracLevelCost 1 ≤ cfracLevelCost k := by
proof body
Tactic-mode proof.
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. -/
depends on (25)
Lean names referenced from this declaration's body.