four_eq_2pow_Dm1
plain-language theorem explainer
The equality 4 = 2^2, equivalently 2^(D-1) at D=3, supplies the numerical link between the count of topological defect types and spatial dimensions in three-dimensional space. Cosmologists classifying defects via homotopy groups would cite this identity to justify exactly four defect categories. The proof is a direct numerical verification by decision procedure.
Claim. $4 = 2^{2} = 2^{D-1}$ for $D=3$.
background
The module identifies four canonical topological defects in cosmology: domain walls, cosmic strings, magnetic monopoles, and textures. These correspond to the homotopy groups π_k(M) for k=0,1,2,3. The local setting states that the defect count equals 2 raised to (D-1) when the spatial dimension D is fixed at 3.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the numerical equality 4 = 2^2 by direct computation.
why it matters
This identity is referenced by the TopologicalDefectCert definition to bundle the defect count with the dimensional relation. It supports the framework step that forces D=3 and accounts for the four defect types through homotopy classification in three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.