extra_dim_eq_flip_variants
plain-language theorem explainer
The number of extra dimensions equals the count of flip variants of the 3-cube by direct arithmetic evaluation. Researchers linking Recognition Science to superstring compactifications would cite this when identifying the seven extra dimensions with 2^3 - 1. The proof is a one-line decision procedure that confirms the identity after substituting the fixed values D = 3 and critical dimension 10.
Claim. Let $D = 3$ be the spatial dimension. Let the superstring critical dimension be 10. Then the number of extra dimensions, defined as $10 - D$, equals $2^D - 1$.
background
In Recognition Science the spatial dimension is fixed at 3 by the eight-tick octave (T7) and the uniqueness result for three dimensions (T8). The module observes that superstring theory requires critical dimension 10, yielding seven compactified dimensions that match the flip-variant count of the 3-cube. Upstream definitions set rsDimension to 3 in both the differential-geometry and linear-algebra modules and define the extra-dimension count as critical dimension minus rsDimension.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the equality after the definitions of extraDimensions and rsDimension are unfolded.
why it matters
This result supplies the flip_variant_match component of the superstringCert bundle, which records the structural match between extra dimensions and flip variants. It realizes the module observation that 10 - 3 = 7 = 2^3 - 1 and thereby connects the T8 result D = 3 to superstring theory. The link remains an observation rather than a derivation of string theory from RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.