stringTheoryCount
plain-language theorem explainer
The theorem establishes that the inductive enumeration of canonical superstring theories has finite cardinality exactly five. Researchers reducing the string landscape to J-cost minima would cite this count when identifying the recognition vacuum at r=1. The proof is a direct decidable computation on the finite type via the decide tactic.
Claim. The set of string theory variants has cardinality five: $|S| = 5$, where $S$ consists of Type I, Type IIA, Type IIB, SO(32) heterotic, and E$_8$×E$_8$ heterotic.
background
The module filters the string landscape of roughly 10^500 vacua by the J-cost function J(r) on moduli space, retaining only those with minimum cost zero at the recognition vacuum r=1. StringTheoryVariant is the inductive type whose five constructors list the canonical superstring theories. This count is paired with the vacuum definition from the Yang-Mills mass gap module, which sets every gauge bond to rung zero.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance derived by the inductive type StringTheoryVariant, which has exactly five constructors.
why it matters
This supplies the five_variants field to the stringTheoryCert definition that certifies the landscape reduction. It fills the chain step mapping the five canonical theories plus M-theory to config dimension five, matching the RS ledger count of five bulk plus one boundary equaling six. It touches the open question of how J-cost minimization collapses the full 10^500 vacua to these five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.