bcs_ground_state
plain-language theorem explainer
The theorem establishes that the J-cost reaches zero at the unit ratio r=1, marking equilibrium for Cooper pair formation in the RS-BCS model. Condensed matter researchers deriving ground state energies from recognition defects would cite this when confirming the minimum cost condition. The proof is a direct one-line application of the Jcost unit lemma.
Claim. The J-cost function satisfies $J(1) = 0$, where $J(x) = (x-1)^2 / (2x)$.
background
The J-cost is defined as $J(x) = (x-1)^2 / (2x)$, quantifying the recognition defect for a given ratio x. This module recasts BCS theory in Recognition Science terms, mapping Cooper pair formation to the J-cost minimum at reciprocal ratios whose product equals 1, with the five BCS parameters treated as configuration dimension D=5 and gap energy scaled by the phi factor times Debye energy.
proof idea
The proof is a one-line wrapper that directly invokes the Jcost_unit0 lemma from the Cost module. That lemma establishes the same equality by simplification of the J-cost definition at argument 1.
why it matters
This result anchors the BCS superconductor construction by supplying the J=0 ground state at r=1, which corresponds to Cooper pair symmetry. It feeds directly into the bcsSuperconductorCert definition that assembles the five-parameter certificate along with parameter count and pair symmetry. In the framework it realizes the J-cost minimum at the canonical band, connecting the Recognition Composition Law to materials applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.