universal_bcs_ratio
plain-language theorem explainer
The universal BCS ratio theorem establishes that twice the zero-temperature gap divided by the critical temperature equals 4/1.134, reproducing the numerical value 3.528. Condensed matter physicists cite it to recover the standard weak-coupling BCS prediction from the J-cost model. The proof unfolds the explicit exponential expressions for gap and Tc then cancels common factors through algebraic rewriting.
Claim. $2Delta(0)/(k_B T_c)=4/1.134$ where $Delta(0)=2omega_Dexp(-1/(N_0V))$ and $k_BT_c=1.134omega_Dexp(-1/(N_0V))$, for positive parameters $omega_D,N_0,V$.
background
In the Recognition Science treatment of BCS superconductivity the Cooper pair instability follows from J-cost submultiplicativity, allowing time-reversed electron pairs to reach zero recognition cost. The module defines the gap parameter via bcs_gap as $2omega_Dexp(-1/(N_0V))$, the recognition cost barrier for pair breaking at zero temperature. The critical temperature is given by bcs_Tc as $1.134omega_Dexp(-1/(N_0V))$, where the prefactor approximates $2e^gamma/pi$ with gamma the Euler-Mascheroni constant.
proof idea
The term-mode proof first unfolds bcs_gap and bcs_Tc to expose identical exponential factors. It establishes non-zero denominators via ne_of_gt applied to the positive parameters and the exponential positivity. It then rewrites the ratio equality with div_eq_div_iff and reduces the resulting polynomial identity with the ring tactic.
why it matters
This theorem confirms the universal ratio $2Delta(0)/(k_BT_c)approx3.528$ inside the J-cost derivation of BCS theory. It completes one of the four core results enumerated in the module documentation for RS_BCS_Superconductivity.tex. The result rests on the Recognition Composition Law through the submultiplicative property of J that forces zero-cost pairing and is independent of the specific inflaton or spectral V definitions appearing in the dependency list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.