compactFamily_count
The declaration establishes that the inductive enumeration of compactification families contains exactly five members. Physicists certifying string reductions within the Recognition Science framework cite this count to confirm the removal of six internal dimensions. The proof is a one-line decision procedure that evaluates the cardinality of the finite inductive type directly.
claimThe finite set of canonical compactification families has cardinality five, consisting of Calabi-Yau manifolds, tori, orbifolds, warped geometries, and brane-world configurations.
background
Recognition Science frames string compactification as the reduction from ten to four dimensions, leaving six internal directions. These six directions are identified with the rank sum 3+2+1 of the B3 group, corresponding to three color axes, two weak axes, and one hypercharge. The CompactificationFamily type is introduced as an inductive definition whose five constructors label the distinct families: Calabi-Yau, torus, orbifold, warped, and brane-world.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance automatically derived from the inductive CompactificationFamily type, which computes its cardinality as five.
why it matters in Recognition Science
This cardinality supplies the five_families component of the StringCompactificationCert definition, which aggregates the compactification data together with the internal-dimension reduction and the six-partition identity. It supports the framework's derivation of three spatial dimensions by confirming the standard reduction to four-dimensional spacetime. The result closes the enumeration step in the compactification chain with no remaining open questions inside the module.
scope and limits
- Does not prove these five families exhaust all possible compactifications in full string theory.
- Does not derive the initial ten-dimensional starting point from Recognition Science axioms.
- Does not compute explicit metrics, spectra, or stability conditions for any family.
- Does not address dynamical evolution or moduli stabilization.
Lean usage
example : Fintype.card CompactificationFamily = 5 := compactFamily_countformal statement (Lean)
27theorem compactFamily_count : Fintype.card CompactificationFamily = 5 := by decide
proof body
Term-mode proof.
28
29/-- 10 - 4 = 6 internal dimensions. -/