topologicalDefect_count
plain-language theorem explainer
The theorem establishes that the finite type enumerating topological defects has cardinality exactly four. Cosmologists classifying defects by homotopy groups in three spatial dimensions would cite this count when connecting the standard quartet to the Recognition Science derivation of D=3. The proof is a single decide tactic that exhausts the four constructors of the inductive definition.
Claim. The set of topological defects has cardinality four: there are exactly four canonical defects (domain walls, cosmic strings, magnetic monopoles, textures) corresponding to homotopy groups in dimensions 0 through 3.
background
The module classifies four canonical topological defects in cosmology via homotopy groups: domain walls for dimension 0, cosmic strings for 1, monopoles for 2, and textures for 3. The inductive definition TopologicalDefect enumerates these four cases explicitly and derives a Fintype instance from them. The local setting is the Recognition Science treatment of defects, where the count satisfies 4 = 2^(D-1) once D=3 is fixed by the forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance of the inductive type TopologicalDefect. Because the type has precisely four constructors, decide computes the cardinality by exhaustive case analysis and confirms equality to 4.
why it matters
This supplies the defect count to the downstream certificate topologicalDefectCert, which pairs it with the relation four_eq_2pow_Dm1. It closes the link between the homotopy classification and the framework step T8 that forces D=3, yielding the observed four defects without additional hypotheses. The result touches the open question of whether the same count emerges directly from the Recognition Composition Law rather than from the inductive enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.