bcs_Tc_positive
plain-language theorem explainer
The theorem shows that the BCS critical temperature is strictly positive for any positive Debye frequency, density of states, and attractive interaction strength. Condensed-matter researchers using the Recognition Science derivation of superconductivity would cite it to guarantee a well-defined transition temperature before invoking the universal gap ratio. The proof is a one-line wrapper that unfolds the explicit exponential definition of bcs_Tc and invokes the positivity tactic.
Claim. If the Debye frequency satisfies $0 < ω_D$, the density of states satisfies $0 < N_0$, and the interaction strength satisfies $0 < V$, then the critical temperature $T_c = 1.134 ω_D exp(-1/(N_0 V))$ obeys $T_c > 0$.
background
The module derives BCS superconductivity from J-cost submultiplicativity: time-reversed electron pairs minimize recognition cost to zero. The critical temperature is defined by the upstream declaration bcs_Tc as $k_B T_c = 1.134 ω_D exp(-1/(N_0 V))$, with the numerical prefactor 1.134 arising from $2e^γ/π$ where γ is the Euler-Mascheroni constant. The companion declaration bcs_gap supplies the zero-temperature gap $Δ(0) = 2 ω_D exp(-1/(N_0 V))$. Boltzmann constant definitions are imported from ComputationLimitsStructure and BekensteinHawking, each stating $k_B = 1.380649 × 10^{-23}$ J/K together with the Landauer bound.
proof idea
The proof is a one-line wrapper. It unfolds the definition of bcs_Tc to obtain the explicit product 1.134 × ω_D × exp(-1/(N_0 V)), then applies the positivity tactic, which succeeds because each factor is positive under the three hypotheses.
why it matters
The result guarantees a positive transition temperature, which is a prerequisite for the sibling theorem universal_bcs_ratio that recovers the observed value 2Δ(0)/(k_B T_c) ≈ 3.528. It completes the mean-field stability step in the RS_BCS_Superconductivity paper and sits inside the broader Recognition Science program that obtains pairing from J-cost submultiplicativity (T5 J-uniqueness and the Recognition Composition Law). No open scaffolding remains for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.