superconductorVortexCert
plain-language theorem explainer
The declaration builds a certificate that type-II superconductors host exactly five vortex lattice types with zero recognition cost on the unit flux quantum. Materials modelers in Recognition Science would cite it when mapping Abrikosov lattices to the phi-ladder single-rung quantum. The construction is a direct field assignment that pulls the lattice count from a decide tactic and the cost from the unit theorem.
Claim. A certificate for superconductor vortices asserts that the number of distinct vortex lattice types equals five and that the recognition cost of the unit flux quantum vanishes: $Fintype.card(VortexLatticeType)=5$ and $Jcost(1)=0$.
background
The module treats type-II superconductors in Recognition Science by identifying Abrikosov vortex lattices with the single-rung phi-ladder quantum. Each vortex carries flux quantum Φ₀ corresponding to J-cost zero at rung 1. The structure SuperconductorVortexCert packages two facts: the cardinality of vortex lattice types equals five (matching configDim D=5) and the minimal recognition cost Jcost(1)=0. Upstream, vortexLatticeCount proves the cardinality by decision procedure while flux_quantum_minimal reduces Jcost(1)=0 to the unit theorem Jcost_unit0.
proof idea
The definition populates the two fields of the SuperconductorVortexCert structure by direct assignment: the lattice count field receives the result of vortexLatticeCount and the cost field receives flux_quantum_minimal.
why it matters
It supplies the concrete certificate that closes the local superconductor model inside the materials section, linking J-cost directly to the five lattice configurations and the zero-cost flux quantum. The construction supports the claim that Recognition Science recovers vortex phenomenology from the recognition composition law and the phi-ladder without additional electromagnetic postulates. No downstream theorems yet reference it, leaving open whether it will feed into a larger derivation of H_c1 or pinning energies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.