bcsParameterCount
plain-language theorem explainer
The declaration asserts that the BCS parameter type in the Recognition Science superconductor model has exactly five elements. Researchers modeling Cooper pair formation via J-cost minima would reference this cardinality when verifying that the parameter set matches the expected configuration dimension. The proof reduces to a single decision tactic that confirms the enumeration of the five constructors in the inductive definition.
Claim. The finite set of BCS parameters, consisting of the energy gap, coherence length, London penetration depth, critical temperature, and critical magnetic field, has cardinality five: $|$energy gap, coherence length, London depth, critical temperature, critical field$| = 5$.
background
In the BCS superconductor model derived from J-cost, Cooper pairs achieve zero net cost through reciprocal recognition signals, with the gap energy scaled by the phi factor and coherence length following the phi-ladder. The module defines BCSParameter as the inductive type with five constructors: energyGap, coherenceLength, londonDepth, criticalTemp, criticalField. These parameters characterize the superconducting state and equal the configuration dimension D = 5 in the Recognition Science framework.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card computation for the inductive type BCSParameter, which derives its Fintype instance from the five constructors.
why it matters
This result supplies the five_params field in the bcsSuperconductorCert definition, completing the certification of the BCS superconductor model. It aligns with the module statement that five BCS parameters equal configDim D = 5, linking to the broader Recognition Science derivation of physical constants from the J-uniqueness and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.