stringCompactificationCert
plain-language theorem explainer
stringCompactificationCert constructs a certificate that string compactification reduces ten dimensions to four while satisfying Recognition Science numerical constraints on families and partitions. Physicists modeling string compactification or RS-derived dimensional reduction would cite it to confirm the match to five families and the 3+2+1 rank sum. The definition is a direct structure constructor that substitutes the decided theorems compactFamily_count, ten_minus_four, and six_eq_rank_sum into the three fields.
Claim. Let $C$ be the structure requiring $|CompactificationFamily|=5$, $10-4=6$, and $6=3+2+1$. Then stringCompactificationCert is the instance of $C$ obtained by substituting the theorems that establish these three equalities.
background
The module frames string compactification as the reduction from ten to four macroscopic dimensions, leaving six internal directions. These six directions are identified with the rank sum of B3, decomposed as three color axes plus two weak axes plus one hypercharge. The structure StringCompactificationCert packages the three facts: the cardinality of the set of five canonical families (Calabi-Yau, torus, orbifold, warped, brane-world), the equality 10-4=6, and the partition 6=3+2+1. Upstream results supply the three equalities by direct decision: compactFamily_count for the family count, ten_minus_four for the dimensional reduction, and six_eq_rank_sum for the rank decomposition.
proof idea
The definition is a direct structure constructor. It populates the five_families field with compactFamily_count, the internal_dims field with ten_minus_four, and the six_partitions field with six_eq_rank_sum. No tactics beyond the pre-decided proofs in the referenced declarations are used.
why it matters
This definition supplies the concrete certificate that string compactification from ten to four dimensions is consistent with the Recognition Science requirement that the six internal dimensions equal the rank sum 3+2+1 of B3. It completes the local verification inside Physics.StringCompactificationFromRS, which treats compactification as removal of six internal directions matching the cube face count. The construction sits downstream of the eight-tick octave and the forcing of D=3 spatial dimensions, providing a numerical anchor between string theory and the RS-derived partition of internal space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.