bcsSuperconductorCert
plain-language theorem explainer
The definition assembles an explicit certificate that the BCS superconductor satisfies the five-parameter count, J-cost zero at unit ratio, and reciprocal symmetry for Cooper pairs. Condensed-matter modelers in Recognition Science would cite it to anchor phonon-mediated pairing to the J-cost minimum. It is a direct structure construction that references the pre-proved count, equilibrium lemma, and symmetry result.
Claim. The BCS superconductor certificate is the structure instance with five parameters, ground state $J(1)=0$, and Cooper-pair symmetry $J(r)=J(r^{-1})$ for all $r>0$, where $J$ is the recognition cost function.
background
In the Recognition Science treatment of BCS superconductivity, Cooper pair formation is the J-cost minimum at reciprocal ratios, with five parameters (gap, coherence length, London depth, critical temperature, critical field) matching config dimension 5. The structure BCSSuperconductorCert encodes exactly these three properties: the finite-type cardinality equals 5, the ground state satisfies J-cost zero at ratio one, and the cost is invariant under inversion. This rests on the upstream lemmas Jcost 1 = 0 (from the unit-zero theorem) and Jcost r = Jcost r^{-1} for r > 0 (from the reciprocal-symmetry theorem), together with the explicit five-parameter count obtained by decide.
proof idea
The definition is a direct structure instantiation of BCSSuperconductorCert. It populates the five-parameter field from the cardinality theorem, the ground-state field from the unit-zero lemma, and the symmetry field from the reciprocal-cost theorem.
why it matters
This supplies the concrete certificate for the BCS mechanism inside the J-cost framework, confirming the five-dimensional parameter space and pairing symmetry required for the superconductor gap. It closes the local module with zero axioms or sorrys, aligning with the Recognition Science derivation of materials properties from the forcing chain. No downstream uses are recorded, leaving open its integration into larger condensed-matter derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.