StringTheoryVariant
plain-language theorem explainer
An enumeration of the five canonical superstring theories is introduced as an inductive type with decidable equality and finite cardinality. Physicists studying vacuum selection via recognition cost would reference this when identifying J-cost zero states with the recognition vacuum at r=1. The definition consists of a direct listing of the five variants with automatic derivation of supporting type classes.
Claim. Let $S$ be the inductive type whose constructors are Type I, Type IIA, Type IIB, SO(32) Heterotic and E8×E8 Heterotic, equipped with decidable equality, representation, Boolean equality and finite type structure.
background
The module frames the string theory landscape of roughly 10^500 vacua through the recognition cost J(r) on moduli space. Vacua attaining minimum J-cost of zero are identified with the recognition vacuum at r=1. The five canonical superstring theories plus M-theory are assigned configDim D=5, which matches the recognition ledger count of five bulk dimensions plus one boundary equaling six.
proof idea
Direct inductive definition of the five cases, deriving DecidableEq, Repr, BEq and Fintype.
why it matters
This supplies the finite set of variants required by the downstream StringTheoryCert structure, which records both Fintype.card=5 and the vacuum condition J(1)=0. It realizes the module claim that the five theories align with RS dimension counting of 5+1=6. The construction touches the T8 step that fixes spatial dimension while extending the ledger to higher-dimensional string configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.