TopologicalDefect
The inductive definition enumerates the four standard topological defects that arise in three-dimensional cosmology. Cosmologists modeling early-universe phase transitions cite this enumeration to fix the defect species count at four. The definition is constructed directly as an inductive type with four cases, from which decidable equality and finite cardinality follow automatically.
claimLet $T$ denote the set of topological defects. Then $T$ consists exactly of the four elements domain wall, cosmic string, monopole and texture.
background
The module presents the four canonical topological defects of cosmology: domain walls, cosmic strings, magnetic monopoles and textures. These correspond to the homotopy groups π_k(M) for k = 0,1,2,3. In three spatial dimensions the count satisfies the relation 4 = 2^{D-1}. The inductive definition supplies the finite set whose cardinality is certified downstream.
proof idea
The declaration is an inductive definition that introduces four constructors and derives the Fintype instance. The derived finite-type structure immediately supplies the cardinality four, which the downstream count theorem extracts by the decide tactic.
why it matters in Recognition Science
This definition supplies the concrete set of defects whose count equals four, matching the relation 4 = 2^{D-1} at D = 3 required by the Recognition Science forcing chain (T8). It feeds the certification structure TopologicalDefectCert and the explicit count theorem that closes the homotopy correspondence in the physics module. The construction touches the framework landmark that spatial dimension equals three.
scope and limits
- Does not derive the defects from the J-functional equation or Recognition Composition Law.
- Does not compute homotopy groups π_k explicitly.
- Does not address stability or formation rates of the defects.
- Does not connect to the phi-ladder mass formula or Berry creation threshold.
formal statement (Lean)
18inductive TopologicalDefect where
19 | domainWall
20 | cosmicString
21 | monopole
22 | texture
23 deriving DecidableEq, Repr, BEq, Fintype
24