cooper_criterion
plain-language theorem explainer
The Cooper criterion asserts that for any x > 0 with x ≠ 1 the J-cost of a time-reversed pair equals zero while the sum of the separate J-costs is strictly positive. Condensed matter physicists modeling superconductivity would cite this as the abstract J-cost version of Cooper's 1956 instability. The proof is a term-mode construction that directly supplies the zero and positive costs then discharges the inequality by linear arithmetic on the zero-cost and pairing-lowers-cost lemmas.
Claim. For any real $x > 0$ with $x ≠ 1$, there exist real numbers $c_p$ and $c_u$ such that $c_p = 0$, $c_u = J(x) + J(x^{-1})$, and $c_p < c_u$, where $J$ is the J-cost function on positive reals.
background
In the Recognition Science module on BCS superconductivity the J-cost function quantifies the recognition cost of a multiplicative state. Time-reversed pairs satisfy J(x · x^{-1}) = J(1) = 0 by the recognition composition law. The module documentation states: 'The Cooper pair instability follows directly from J-cost submultiplicativity: time-reversed electron pairs minimize J-cost to zero.' Upstream lemmas establish that J-cost is the derived cost of multiplicative recognizers and that recognition events carry non-negative J-cost.
proof idea
The proof is a term-mode construction. It refines the existential to the concrete pair (0, Jcost x + Jcost x^{-1}), supplies reflexivity for the two equalities, then applies linear arithmetic to the lemmas time_reversed_pair_zero_cost and pairing_lowers_cost to obtain the strict inequality.
why it matters
This theorem supplies the base Cooper criterion that the same module uses to derive the BCS gap equation, the universal ratio 2Δ/kT_c ≈ 3.52, and the Meissner effect. It realizes J-cost submultiplicativity inside the Recognition Science forcing chain and connects directly to the phi-ladder structure. The result is presented in the paper RS_BCS_Superconductivity.tex as the energetic foundation for pair formation before the saddle-point derivation of the gap parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.