topologicalDefect_count
plain-language theorem explainer
The theorem fixes the number of topological defects at exactly four in three spatial dimensions. Cosmologists counting phase-transition relics would cite the count when listing domain walls, cosmic strings, monopoles, and textures. The proof is a one-line decision procedure on the Fintype instance derived from the inductive enumeration of those four cases.
Claim. The finite set of topological defects has cardinality four: $|S| = 4$ where $S = $ {domain walls, cosmic strings, monopoles, textures}.
background
The module states that four canonical topological defects arise in cosmology and that their count equals $2^{D-1}$ at $D=3$. The inductive type enumerates them explicitly as domainWall, cosmicString, monopole, texture and derives the Fintype instance used for cardinality. The upstream result is precisely this inductive definition, which supplies the finite set whose size is asserted.
proof idea
One-line wrapper that applies the decide tactic to the equality Fintype.card TopologicalDefect = 4.
why it matters
The result supplies the four_defects field to the downstream certificate topologicalDefectCert. It realizes the T8 forcing step that D=3 yields exactly four defect types via the relation 4 = 2^(D-1). The module doc-comment ties the count directly to homotopy dimensions 0 through 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.