pith. machine review for the scientific record. sign in
def definition def or abbrev high

extraDimensions

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  27def extraDimensions : ℕ := strCriticalDim - rsDimension

proof body

Definition body.

  28

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.