extra_dim_eq_flip_variants
plain-language theorem explainer
The result equates the number of extra dimensions in the superstring construction to two to the power of the Recognition Science spatial dimension minus one. Workers connecting Recognition Science to string theory cite it to equate the seven compactified dimensions with the flip variants of the three-cube. The proof is a direct numerical check performed by the decide tactic.
Claim. $D_{crit} - D = 2^D - 1$, where $D$ is the spatial dimension fixed at three and $D_{crit}$ is the superstring critical dimension.
background
Recognition Science fixes the spatial dimension at three via the eight-tick octave in the forcing chain. Superstring theory requires a critical dimension of ten, so seven dimensions are extra and compactified. The theorem identifies these seven with the flip variants of the three-cube, since two cubed minus one equals seven. The upstream definitions set rsDimension to three in both mathematics and physics modules and define extraDimensions as the difference between the critical dimension and rsDimension.
proof idea
This is a one-line wrapper that applies the decide tactic to verify the equality after the constants are substituted.
why it matters
It provides the flip_variant_match field in the superstringCert definition, completing the certification that the extra dimensions align with the flip variants. The result ties the T8 step of the forcing chain, which forces three spatial dimensions, to the superstring critical dimension. It confirms the structural observation that ten minus three equals seven equals two to the third minus one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.