TopologicalDefectCert
plain-language theorem explainer
TopologicalDefectCert packages the assertion that exactly four topological defect types exist in three spatial dimensions, with the count satisfying 4 = 2^2. Cosmologists working in the Recognition Science framework cite it to connect homotopy classification to the standard quartet of defects. The declaration is a bare structure definition whose two fields directly record the cardinality and the numerical identity.
Claim. Let $TopologicalDefect$ be the inductive type whose constructors are domainWall, cosmicString, monopole, and texture. A $TopologicalDefectCert$ is a structure whose fields assert that the cardinality of this type equals 4 and that $4 = 2^2$.
background
The module enumerates four canonical topological defects in cosmology: domain walls, cosmic strings, magnetic monopoles, and textures. These arise as the homotopy groups π_k(M) for k = 0,1,2,3 when the manifold M is taken in D = 3 spatial dimensions, yielding the relation 4 = 2^(D-1). The upstream inductive definition TopologicalDefect supplies the four constructors and derives Fintype, DecidableEq, and Repr instances.
proof idea
The declaration is a structure definition containing two fields. The first field states Fintype.card TopologicalDefect = 4. The second field states the identity (4 : ℕ) = 2 ^ 2. No tactics or lemmas are invoked; the structure simply records the count and the power relation already established by the module's homotopy correspondence.
why it matters
The structure is instantiated by the downstream definition topologicalDefectCert, which supplies concrete values for both fields. It encodes the Recognition Science claim that the homotopy count in D = 3 produces precisely four defect types, consistent with the eight-tick octave and the forcing of three spatial dimensions (T8). The definition closes the enumeration step without adding new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.