bcs_gap
plain-language theorem explainer
The BCS gap parameter is defined as twice the Debye frequency multiplied by an exponential suppression set by the product of density of states and pairing strength. Condensed-matter researchers working inside the Recognition Science framework cite this expression when computing zero-temperature Cooper-pair stability from J-cost minimization. The definition is a direct one-line transcription of the saddle-point result of the J-cost landscape.
Claim. The zero-temperature gap is given by $Δ(0) = 2ω_D exp(-1/(N_0 V))$, where $ω_D$ is the Debye frequency, $N_0$ the density of states at the Fermi level, and $V$ the effective attractive interaction.
background
Recognition Science treats the J-cost function $J(x) = (x + x^{-1})/2 - 1$ as the fundamental measure of configuration cost; submultiplicativity of $J$ implies that time-reversed electron pairs incur zero net cost. The module therefore derives Cooper-pair stability directly from this property and places the gap as the recognition-cost barrier to pair breaking. Upstream definitions supply the manifold: the inflaton potential $V(φ_inf) = J(1 + φ_inf)$ and the spectral-emergence vertex count $V(D) = 2^D$ locate the saddle-point evaluation.
proof idea
The declaration is a one-line definition that transcribes the standard BCS zero-temperature gap formula into RS-native variables. No lemmas are applied; the expression follows immediately from the saddle-point statement given in the module documentation.
why it matters
This definition supplies the gap value required by the three immediate downstream theorems: bcs_gap_positive, bcs_Tc_positive, and universal_bcs_ratio. It realizes the module claim that superconductivity emerges from J-cost submultiplicativity and closes the step from the eight-tick octave and phi-ladder to the observed BCS ratio 2Δ/k_B T_c ≈ 3.528. The parent paper reference is RS_BCS_Superconductivity.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.