vortexLatticeCount
plain-language theorem explainer
Establishes that the inductive type of vortex lattice configurations has cardinality five. Condensed matter theorists modeling type-II superconductors in the Recognition Science framework cite this when deriving Abrikosov lattices from J-cost thresholds. The proof is a one-line decision procedure that computes the cardinality directly from the five-constructor inductive definition of VortexLatticeType.
Claim. The finite cardinality of the vortex lattice type is five: $Fintype.card(VortexLatticeType) = 5$, where VortexLatticeType is the inductive type with constructors abrikosov, hexagonal, square, disordered, and coexistence.
background
The SuperconductorVortexFromJCost module models type-II superconductors via J-cost, the recognition cost of a state. Each vortex carries one flux quantum corresponding to the minimal J(1) = 0 on the phi-ladder. VortexLatticeType is defined as an inductive type with five constructors (abrikosov, hexagonal, square, disordered, coexistence) that derives Fintype, Repr, BEq, and DecidableEq. This realizes configDim D = 5 for lattice structures, with the penetration field H_c1 identified as the J(phi) threshold in magnetic recognition cost.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card VortexLatticeType. The inductive type derives Fintype and enumerates exactly five constructors, so decide reduces the equality to a decidable computation that returns true.
why it matters
This theorem supplies the five_lattice_types field in the downstream SuperconductorVortexCert structure. It fills the module claim that five vortex lattice structures equal configDim D = 5, linking to the forcing chain landmarks T7 (eight-tick octave) and T8 (D = 3 spatial dimensions) through the J-cost model. The result closes a zero-sorry point in the materials application of the Recognition Composition Law and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.