compactFamily_count
plain-language theorem explainer
The theorem asserts that the set of compactification families in the Recognition Science string model has cardinality exactly five. Physicists verifying the reduction from ten to four dimensions would cite this count when assembling the compactification certificate. The proof is a one-line decision procedure that enumerates the five constructors of the inductive family type.
Claim. The finite set of compactification families (Calabi-Yau, torus, orbifold, warped, brane-world) has cardinality five: $|CompactificationFamily| = 5$.
background
The module frames string compactification as the removal of six internal dimensions when descending from ten to four macroscopic dimensions. These six directions are identified with the rank sum 3+2+1 of the B3 group (three colour axes, two weak axes, one hypercharge). Five canonical families are listed: Calabi-Yau, torus, orbifold, warped (RS1/RS2), and brane-world.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card CompactificationFamily = 5. The inductive definition of CompactificationFamily derives both DecidableEq and Fintype, so the tactic computes the cardinality directly from the five listed constructors.
why it matters
This result supplies the five_families component of the downstream StringCompactificationCert definition, which also records the internal-dimension count (ten minus four) and the six-partition equality. It operationalizes the module claim that five families realize the compactification step, consistent with the eight-tick octave and D = 3 spatial dimensions in the forcing chain (T7-T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.