SuperconductorVortexCert
plain-language theorem explainer
SuperconductorVortexCert packages the claim that exactly five vortex lattice geometries are admitted together with the vanishing J-cost of a single flux quantum. Condensed-matter modelers working in the Recognition Science setting would cite the structure when certifying the fivefold degeneracy of Abrikosov lattices. The declaration is a bare structure that directly records the Fintype cardinality of the enumerated lattice type and the Jcost evaluation at unity.
Claim. The vortex-lattice certificate structure asserts that the set of admissible vortex lattice geometries has cardinality five and that the recognition cost $J(1)$ of the elementary flux quantum vanishes.
background
In the Recognition Science treatment of materials, type-II superconductors support Abrikosov vortex lattices once the applied field exceeds the lower critical field. Each vortex carries one flux quantum corresponding to the single-rung step on the phi-ladder. The module enumerates five distinct lattice realizations (Abrikosov, hexagonal, square, disordered, and coexistence) and identifies this count with configuration dimension 5. The inductive type VortexLatticeType lists precisely these five constructors. The J-cost function, imported from the Cost module, measures the recognition penalty of a configuration; its evaluation at unity is required to vanish for the minimal flux quantum.
proof idea
The declaration is a direct structure definition whose two fields record the cardinality of the VortexLatticeType inductive type and the Jcost evaluation at 1. No lemmas or tactics are applied; the structure simply bundles the two assertions.
why it matters
SuperconductorVortexCert supplies the type for the concrete certificate constructed from the vortex lattice count and the minimal flux quantum fact. It thereby embeds the fivefold degeneracy of vortex lattices into the Recognition Science account of type-II superconductivity, consistent with configuration dimension 5. The structure closes the interface between the enumerated lattice types and the zero-cost condition on the elementary quantum required by the magnetic recognition cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.