cooper_pair_symmetry
plain-language theorem explainer
J-cost is invariant under inversion for positive reals, licensing zero net cost for reciprocal electron pairs in the BCS construction. Materials physicists building Recognition Science models of superconductors cite this when certifying the ground state. The proof is a one-line wrapper invoking the core J-cost symmetry lemma.
Claim. For every real number $r > 0$, the J-cost satisfies $J(r) = J(r^{-1})$.
background
The module constructs a BCS superconductor from the J-cost function, where Cooper pairs form when two electrons carry reciprocal recognition ratios and achieve net J-cost zero. J-cost itself is the recognition defect $J(x) = (x + x^{-1})/2 - 1$. The local setting equates five BCS parameters (gap, coherence length, London depth, critical temperature, critical field) to config dimension D = 5 and links gap energy to a phi-scaled Debye frequency.
proof idea
One-line wrapper that applies the Jcost_symm lemma from the Cost module, passing the positivity hypothesis hr directly.
why it matters
The theorem supplies the cooper_pair_sym field inside bcsSuperconductorCert, completing the certification of the BCS ground state. It realizes the module claim that reciprocal pairing yields J = 0, consistent with T5 J-uniqueness and the phi-ladder in the forcing chain. No open questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.