bcs_Tc
plain-language theorem explainer
The BCS critical temperature is defined by the expression 1.134 ω_D exp(-1/(N_0 V)), with ω_D the Debye frequency, N_0 the density of states at the Fermi level, and V the pairing interaction strength. Condensed matter physicists cite this for the onset of superconductivity in the weak-coupling BCS regime. The definition is a direct transcription of the standard formula using the numerical prefactor 1.134 to approximate 2e^γ/π.
Claim. The critical temperature satisfies $k_B T_c = 1.134 ħ ω_D exp(-1/[N(0)V])$, where ω_D is the Debye frequency, N(0) the electronic density of states at the Fermi energy, and V the effective attractive interaction between time-reversed electrons.
background
The module derives BCS superconductivity from J-cost submultiplicativity in the Recognition Science framework, where time-reversed electron pairs minimize J-cost to zero. The Cooper pair instability follows from the Recognition Composition Law applied to pairing, with the eight-tick octave supplying the discrete structure for the exponential gap equation. Upstream results on J-cost core supply the algebraic foundation for the cost function, while the inflaton potential and spectral emergence definitions illustrate the same J-cost form used here for the pairing potential.
proof idea
The declaration is a one-line definition that multiplies the Debye frequency by the exponential factor exp(-1/(N_0 V)). No lemmas or tactics are invoked; it directly encodes the textbook BCS expression with the fixed numerical prefactor 1.134.
why it matters
This definition supplies the critical temperature for the downstream theorems bcs_Tc_positive, isotope_effect, and universal_bcs_ratio. The universal_bcs_ratio result then obtains the ratio 2Δ/k_B T_c = 4/1.134 ≈ 3.528, reproducing the observed BCS value. It links J-uniqueness (T5) and the eight-tick periodicity (T7) to measurable superconductivity parameters, closing one step in the application of the forcing chain to condensed-matter phenomena.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.