SpectralViability
plain-language theorem explainer
SpectralViability D packages the three conditions needed for spectral emergence in dimension D: D equals 3, at least three face pairs, and lcm of 2^D with 45 equals 360. Researchers deriving gauge groups and three generations from the binary cube Q3 cite this structure. It is introduced as a direct structure definition whose fields match the requirements stated in the module documentation.
Claim. A natural number $D$ satisfies the spectral viability conditions when $D=3$, the number of opposite face pairs on the $D$-cube obeys $3leq D(D-1)/2$, and the least common multiple of $2^D$ and 45 equals 360.
background
The SpectralEmergence module starts from the forced datum D=3 (T8) and shows that the binary cube Q3 simultaneously produces the gauge content SU(3) x SU(2) x U(1), exactly three generations, and 48 fermionic states. The local face_pairs definition counts opposite face pairs as $D(D-1)/2$; for D=3 this yields exactly three pairs, matching the three generations required by the ParticleGenerations.face_pairs result. Upstream results supply auxiliary lists (seven plot families, eight kinship systems, seven Greek modes) but the core algebraic dependencies are the two face_pairs definitions and the module's own Q3 constructions.
proof idea
This is a structure definition with an empty proof body. The three fields are introduced directly from the requirements listed in the doc-comment; no lemmas or tactics are applied.
why it matters
The structure is instantiated in D3_viable to certify that D=3 works and is extended in SpectralEmergenceCert to record the full emergence of gauge sectors, generations, and fermion count from Q3. It closes the step from T8 (D=3) to the numerical coincidences |Aut(Q3)|=48 and three face pairs, while leaving open whether other dimensions could satisfy the lcm condition under relaxed gap assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.