97theorem phi_ladder_unbounded (T : ℝ) (hT : 0 < T) : 98 ∃ n : ℤ, T < T_c_rung n := by
proof body
Term-mode proof.
99 unfold T_c_rung 100 -- phi⁻¹ < 1 since phi > 1, so phi⁻¹^k → 0 as k → ∞ 101 -- equivalently phi^k → ∞ 102 obtain ⟨n, hn⟩ := pow_unbounded_of_one_lt T one_lt_phi 103 exact ⟨(n : ℤ), by rw [zpow_natCast]; exact hn⟩ 104 105/-! ## §III. Superconducting Gap -/ 106 107/-- The superconducting gap function Δ in RS. 108 Δ is proportional to E_coh reduced by the thermal competition ratio. 109 When T < T_c, gap Δ > 0 (superconducting); when T ≥ T_c, Δ = 0 (normal). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.