bcs_Tc
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^γ/π.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the BCS gap equation from the J-cost functional equation.
- Does not include strong-coupling or retardation corrections to the weak-coupling limit.
- Does not treat the temperature dependence of the gap or the full phase diagram.
formal statement (Lean)
81noncomputable def bcs_Tc (ω_D N₀ V : ℝ) : ℝ :=
proof body
Definition body.
82 1.134 * ω_D * Real.exp (-1 / (N₀ * V))
83
84/-- T_c is positive for positive parameters. -/