topologicalDefectCert
plain-language theorem explainer
This definition assembles a certificate confirming that precisely four topological defect types exist in three-dimensional space according to homotopy classification. Cosmologists modeling early-universe phase transitions would cite it to connect the defect count directly to the spatial dimension fixed by the Recognition Science forcing chain. The construction is a direct record that populates the cardinality field from the defect enumeration theorem and the power-of-two field from the dimension identity theorem.
Claim. The definition constructs an instance of the certificate structure asserting that the cardinality of the set of topological defects equals 4 and that this number satisfies the identity $4 = 2^{2}$, by supplying the defect enumeration result for the first field and the dimension-derived equality for the second.
background
The module establishes that four canonical topological defects arise in 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, with the count satisfying 4 = 2^(D-1) at D = 3. The referenced structure TopologicalDefectCert packages two requirements: the cardinality of the defect set equals 4, and the numerical identity 4 = 2^2 holds. Upstream, the theorem topologicalDefect_count establishes the cardinality equality by direct computation, while four_eq_2pow_Dm1 proves the power relation by decision.
proof idea
The definition is a direct structure instantiation. It assigns the cardinality field from the upstream defect count theorem and the power-of-two field from the upstream dimension identity theorem.
why it matters
This definition closes the local enumeration of topological defects within the Recognition Science framework. It directly implements the relation 4 = 2^(D-1) that follows from T8 fixing D = 3 spatial dimensions, thereby linking the homotopy classification to the eight-tick octave of the forcing chain. No downstream theorems are recorded, leaving open whether the certificate will be invoked in later derivations of defect stability or formation rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.