TopologicalDefect
plain-language theorem explainer
Four canonical topological defects of 3D cosmology are enumerated as an inductive type. RS cosmologists cite the definition when confirming that defect count equals 2 to the power of D minus 1. The definition proceeds by explicit listing of the four cases together with automatic derivation of finiteness and decidability.
Claim. The topological defects comprise the finite set consisting of domain walls, cosmic strings, monopoles, and textures.
background
The module states that four canonical defects arise in cosmology and correspond to homotopy groups in dimensions 0 through 3. Recognition Science obtains D = 3 as T8 of the forcing chain, which forces the relation 4 = 2^(D-1). The definition supplies the finite type whose cardinality is later certified.
proof idea
This is an inductive definition with four constructors and deriving clauses that install DecidableEq, Repr, BEq, and Fintype instances.
why it matters
The definition supplies the type whose cardinality is recorded in TopologicalDefectCert as 4 and as equal to 2 squared. That equality realizes the dimension count D = 3 from the forcing chain inside the defect sector. It thereby anchors the homotopy-derived defect count inside the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.