BCSParameter
plain-language theorem explainer
BCSParameter enumerates the five standard observables of BCS superconductivity reinterpreted as J-cost minima for Cooper pairs in Recognition Science. Condensed matter modelers verifying superconductor certification would cite this enumeration when confirming the configuration dimension equals five. The declaration is a direct inductive type with automatic derivation of decidable equality and finiteness.
Claim. The inductive type enumerating BCS parameters consists of five constructors: the energy gap, the coherence length, the London depth, the critical temperature, and the critical field.
background
The module maps BCS theory to Recognition Science by equating Cooper pair formation with J-cost minima where reciprocal ratios achieve zero cost. Upstream, energyGap is the excess energy above the Newtonian ground state, proportional to the integral of squared gradients plus potential terms. Critical temperature is defined on the phi-ladder as phi raised to rung k.
proof idea
Direct inductive definition introducing five constructors, with DecidableEq, Repr, BEq, and Fintype derived automatically.
why it matters
This enumeration is used by bcsParameterCount to prove cardinality five and by BCSSuperconductorCert to require Jcost(1) = 0 together with cooper pair symmetry for all positive r. It supplies the parameter list for the BCS mechanism step, aligning with configuration dimension D = 5 and the phi-ladder scaling for critical temperature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.