152theorem cooper_pair_binding_exceeds_thermal 153 (n : ℤ) (hn : 0 ≤ n) : 154 1 ≤ T_c_rung n := by
proof body
Term-mode proof.
155 unfold T_c_rung 156 rcases hn.lt_or_eq with hn' | hn' 157 · exact (one_lt_zpow₀ one_lt_phi hn').le 158 · simp [hn'.symm] 159 160/-! ## §V. Coherence Condition: φ-Phonon Coupling -/ 161 162/-- RS predicts: superconductivity occurs when the electron-phonon coupling 163 places the system on the φ-ladder. The coupling constant g must satisfy: 164 g = φ^(-k) for some integer k ≥ 0. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.