StringCompactificationCert
plain-language theorem explainer
StringCompactificationCert bundles three numerical identities that certify the reduction from ten to four dimensions under the Recognition Science reading of string compactification. A physicist extracting gauge ranks from internal geometry would cite it to record five families, the removal of six directions, and their partition as three plus two plus one. The declaration is a structure definition containing no proof steps or lemmas.
Claim. A structure whose fields assert that the set of compactification families has cardinality five, that $10-4=6$, and that $6=3+2+1$.
background
The module frames compactification from ten to four macroscopic dimensions as the removal of six internal directions. In the RS interpretation these six directions are identified with three color axes, two weak axes, and one hypercharge direction, matching the rank sum of the gauge algebra B3. The five families are listed as Calabi-Yau, torus, orbifold, warped (RS1/RS2), and brane-world constructions.
proof idea
This is a structure definition that simply declares three fields recording the cardinality of the compactification families, the dimension-reduction identity, and the partition identity. No lemmas are applied and no tactics are used; the structure acts as a container whose fields are later instantiated by the downstream definition stringCompactificationCert.
why it matters
StringCompactificationCert supplies the type instantiated by stringCompactificationCert, thereby certifying the geometric consistency of the compactification scheme. It supplies one of the foundational steps that connect ten-dimensional string geometry to four-dimensional physics inside the Recognition Science framework, consistent with the emergence of three spatial dimensions in the unified forcing chain. It leaves open the dynamical selection among the five families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.