TopologicalCharge
plain-language theorem explainer
Enumerates the five topological charge species that arise for configuration dimension five: winding, vortex, monopole, instanton, and skyrmion. Researchers classifying conserved quantities in variational field theories cite this list to instantiate the general integer-valued charge structure. The declaration is a bare inductive type whose deriving clauses supply decidable equality, representation, and finiteness with no further obligations.
Claim. The topological charges are the five classes winding number ($π_1$), vortex charge ($π_0$ of broken symmetry), monopole charge ($π_2$), instanton charge ($π_3$), and Skyrmion charge ($π_3/π_4$).
background
Recognition Science ties topological charges to configuration dimension D=5, producing exactly these five homotopy classes. The upstream structure TopologicalCharge(N) from Foundation.TopologicalConservation defines a charge as an integer-valued map from configurations to ℤ that remains invariant under any variational successor. The winding definition from Masses.Ribbons supplies the net winding on the eight-tick clock as the sum of +1 or −1 per directed step.
proof idea
Direct inductive definition that enumerates the five constructors and derives DecidableEq, Repr, BEq, and Fintype automatically. No lemmas or tactics are invoked; the type is introduced as primitive data.
why it matters
This enumeration supplies the concrete carriers required by the conservation theorems in TopologicalConservation, including addCharges, charge_at_any_tick, and conservation_is_unconditional. It realizes the five classes stated in the module documentation for configDim D=5 and links them to the homotopy groups listed there. The definition therefore closes the interface between the general charge structure and the specific physics content without imposing extra symmetry hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.