topologicalCharge_count
plain-language theorem explainer
The theorem establishes that the inductive enumeration of topological charges contains exactly five elements when the configuration dimension is five. A physicist classifying defects in gauge theories would cite the result to fix the count of winding, vortex, monopole, instanton, and Skyrmion charges. The proof is a single decide tactic that evaluates the Fintype.card expression on the derived instances of the inductive type.
Claim. The set of topological charges has cardinality five: $|T| = 5$ where $T = $ {winding, vortex, monopole, instanton, skyrmion}.
background
The module fixes configuration dimension at five and enumerates five canonical topological charge classes. The inductive type TopologicalCharge is defined with five constructors winding, vortex, monopole, instanton, skyrmion, each tied to a homotopy group: winding from π₁, vortex from π₀ of the broken phase, monopole from π₂, instanton from π₃, and Skyrmion from π₃/π₄. The module documentation states that this yields exactly five classes with Lean status zero sorry and zero axiom.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds directly because the inductive type derives DecidableEq, Repr, BEq, and Fintype, allowing the cardinality computation to reduce to a finite enumeration of the five constructors.
why it matters
The result supplies the five_charges field inside the downstream definition topologicalChargesCert, which certifies the enumeration for the module. It realizes the module claim that five charge classes arise at configDim D = 5. In the Recognition Science setting this count is independent of the spatial dimension D = 3 obtained from the forcing chain T8, yet it supplies the discrete charge types whose conservation is formalized in the upstream structure TopologicalCharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.