flux_quantum_minimal
plain-language theorem explainer
The result states that the recognition cost of a single flux quantum is zero. Materials physicists working on type-II superconductors would cite it to fix the minimal J-cost anchor for Abrikosov vortices in the Recognition Science model. The proof is a one-line wrapper that invokes the unit lemma Jcost_unit0.
Claim. $J(1) = 0$, where $J$ is the recognition cost function $J(x) = (x-1)^2/(2x)$ applied to a unit vortex.
background
The module treats type-II superconductors in Recognition Science terms, where each vortex carries one flux quantum corresponding to the single-rung phi-ladder step. The J-cost function is defined as the squared ratio $J(x) = (x-1)^2/(2x)$ and supplies the recognition cost for magnetic configurations. Upstream the lemma Jcost_unit0 establishes the unit case by direct simplification of that definition. The local setting also records five vortex lattice structures as configDim D = 5.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module (and its JcostCore sibling). That lemma itself reduces to simp [Jcost] on the squared-ratio definition.
why it matters
This supplies the flux_quantum_cost field inside the superconductorVortexCert definition, which certifies the full vortex lattice package. It closes the basic J-cost interface for the materials module and links the single-rung phi-ladder quantum to the observed flux quantum. The result sits inside the broader forcing chain that derives spatial dimensions and constants from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.