VortexLatticeType
plain-language theorem explainer
VortexLatticeType enumerates the five lattice configurations that flux lines adopt in type-II superconductors under the Recognition Science J-cost model. Condensed matter physicists modeling vortex pinning and critical currents cite this enumeration when counting distinct arrangements above H_c1. The declaration is a direct inductive type with five constructors that derives Fintype and decidable equality instances automatically.
Claim. The type of vortex lattice configurations in type-II superconductors consists of five elements: Abrikosov lattice, hexagonal lattice, square lattice, disordered state, and coexistence phase, equipped with decidable equality and finite cardinality.
background
Recognition Science associates each vortex with one flux quantum on the single-rung phi-ladder, where the J-cost function satisfies J(1) = 0. The module treats the five lattice structures as a configuration space of dimension 5, linking vortex penetration to the magnetic recognition cost threshold. This setting draws on the J-cost definition imported from the Cost module and the constants module for phi-ladder scaling.
proof idea
The declaration is a direct inductive definition with five constructors that derives DecidableEq, Repr, BEq, and Fintype instances in one step.
why it matters
This definition supplies the finite enumeration required by SuperconductorVortexCert to certify five lattice types and zero J-cost for the flux quantum. It extends the Recognition framework to materials by realizing configDim = 5 for vortex arrangements, consistent with the phi-ladder and J-cost landmarks from the UnifiedForcingChain. The construction closes a materials application without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.