extraDimensions
plain-language theorem explainer
The definition computes the number of extra dimensions as the arithmetic difference between the superstring critical dimension of 10 and the RS spatial dimension of 3. Researchers examining the structural correspondence between Recognition Science and superstring theory cite it when matching the seven compactified dimensions to the flip variants of the three-cube. It is realized as a direct subtraction of the two dimension constants already fixed in sibling modules.
Claim. The number of extra dimensions is defined by the subtraction $d_ {extra} := d_{crit} - D_{RS}$, where $d_{crit} = 10$ is the critical dimension required by superstring theory and $D_{RS} = 3$ is the spatial dimension fixed by Recognition Science.
background
Recognition Science fixes the spatial dimension at three via the forcing chain T0-T8, recorded in the rsDimension definition that appears identically in the DifferentialGeometryFromRS, LinearAlgebraFromRS, and SuperstringTheoryFromRS modules. Superstring theory supplies the critical dimension ten through the sibling constant strCriticalDim. The module documentation states that both frameworks require a total of ten dimensions yet RS enforces three non-compact ones, leaving seven compactified.
proof idea
The definition is a one-line wrapper that subtracts the value of rsDimension from strCriticalDim.
why it matters
This definition supplies the numerical value asserted equal to seven in the downstream theorem extra_dim_eq_7 and equal to $2^3 - 1$ in extra_dim_eq_flip_variants. It closes the structural observation that the seven compactified dimensions equal the flip-variant count of the three-cube, linking T8 (D=3) to the superstring critical dimension. The SuperstringCert structure packages the equality together with the flip match as a certificate for the RS-string correspondence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.