TopologicalChargesCert
plain-language theorem explainer
TopologicalChargesCert is a structure that records the assertion of exactly five topological charge classes arising when configuration dimension equals five. Researchers enumerating conserved defects in gauge theories or condensed matter would cite it to fix the complete set of integer-valued invariants. The structure is realized by a single field that equates the cardinality of the enumerated charge types to five.
Claim. Let $T$ be the finite set of topological charges consisting of the winding-number, vortex, monopole, instanton, and Skyrmion classes. The certificate asserts that the cardinality of $T$ equals five: $|T| = 5$.
background
In the Recognition Science framework a topological charge is an integer-valued function on configurations that remains invariant under variational dynamics, as introduced in the foundational conservation structure. The present module enumerates five canonical classes tied directly to configuration dimension five: winding number from the first homotopy group, vortex charge from the zeroth homotopy group of the broken phase, monopole charge from the second homotopy group, instanton charge from the third homotopy group, and Skyrmion charge from the third or fourth homotopy groups.
proof idea
The structure is introduced by a single field whose type is the proposition that the cardinality of the inductive enumeration of the five charge types equals five. No lemmas are invoked; the equality is immediate from the Fintype instance derived on the inductive type.
why it matters
This certificate supplies the enumeration required by the downstream definition that constructs an explicit instance using the count of topological charges. It fills the slot documenting how five charges emerge from configDim equal to five, linking to the broader derivation of physics from the unified forcing chain. It touches the open question of how these charges interact with the phi-ladder mass formula and the fixed spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.