six_eq_rank_sum
plain-language theorem explainer
The equality asserts that six equals three plus two plus one as the rank sum of the B3 algebra, partitioning the six internal directions removed when compactifying from ten to four spacetime dimensions. Physicists constructing RS-derived string compactifications cite it to match the gauge factors (three color, two weak, one hypercharge) to the internal count. The proof is a direct numerical verification by the decide tactic.
Claim. $6 = 3 + 2 + 1$, where the right-hand side is the rank sum of the Lie algebra $B_3$ and equals the sum of three color axes, two weak axes, and one hypercharge direction.
background
The module treats string compactification from ten to four macroscopic dimensions as the removal of six internal directions. In the RS framing these directions are identified with the rank sum of $B_3$, decomposed as three color plus two weak plus one hypercharge. The local setting defines five canonical families (Calabi-Yau, torus, orbifold, warped, brane-world) and records that the entire development contains zero sorry statements.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the arithmetic identity by computation.
why it matters
The theorem supplies the six_partitions field inside the stringCompactificationCert definition, which certifies the full compactification data. It directly encodes the rank-sum identity given in the module documentation. The result anchors the internal-dimension count to the gauge-group decomposition required by the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.