topologicalChargesCert
plain-language theorem explainer
This definition supplies a concrete certificate asserting exactly five topological charge classes when the configuration dimension equals five. A physicist classifying solitons or defects via homotopy groups would cite the result to fix the enumeration of stable configurations. The construction is a direct one-line wrapper that populates the required structure field from the decided cardinality theorem.
Claim. Let $TopologicalChargesCert$ be the structure whose sole field requires that the cardinality of the type of topological charges equals five. The definition supplies the witness obtained by setting that field to the theorem establishing the cardinality.
background
The module identifies five canonical topological charge classes when the configuration dimension is five: winding number classified by the fundamental group, vortex charge from the zeroth homotopy of the broken vacuum, monopole charge from the second homotopy group, instanton charge from the third homotopy group, and Skyrmion charge from the quotient of the third and fourth homotopy groups. These classes arise directly from the homotopy classification of maps into the vacuum manifold in five-dimensional configuration space.
proof idea
The definition is a one-line wrapper that directly assigns the result of the topologicalCharge_count theorem to the five_charges field of the TopologicalChargesCert structure.
why it matters
This definition certifies the count of five topological charges required by configuration dimension five inside the Recognition Science framework. It anchors the enumeration of defects that complements the forcing chain steps leading to three spatial dimensions. No downstream theorems yet consume the certificate, leaving open its insertion into explicit charge or mass formulas on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.