CompactificationFamily
plain-language theorem explainer
CompactificationFamily enumerates five families of geometries that reduce ten-dimensional string theory to four observed dimensions in the Recognition Science setting. String theorists verifying the internal dimension count would cite this enumeration when constructing certificates for the 10-4=6 reduction. The definition lists the five cases explicitly and derives finite-type and equality instances.
Claim. Let $F$ be the finite set of compactification families. Then $F = $ {Calabi-Yau, torus, orbifold, warped, brane-world}, where each element labels a distinct mechanism for compactifying six internal dimensions while preserving the observed gauge ranks.
background
The module situates string compactification inside Recognition Science by equating the removal of six internal directions with the gauge rank sum 3 + 2 + 1. This partition corresponds to the three color axes, two weak axes, and one hypercharge of the standard model. Five canonical families classify the geometries that achieve the reduction from ten to four macroscopic dimensions.
proof idea
The declaration is a direct inductive definition that introduces five constructors. Deriving clauses attach DecidableEq, Repr, BEq, and Fintype automatically; no lemmas or tactics are required.
why it matters
The definition supplies the finite set whose cardinality is asserted to be five in the downstream theorem compactFamily_count and is recorded inside the structure StringCompactificationCert. That structure encodes the dimension reduction 10-4=6 together with the partition 3+2+1. It therefore anchors the string-theoretic origin of the three spatial dimensions that appear at step T8 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.