rsDimension
plain-language theorem explainer
The definition fixes the spatial dimension D to the integer 3 in the Recognition Science derivation of differential geometry. Researchers building the recognition manifold or spacetime structures from the forcing chain cite this constant when counting dimensions or verifying manifold properties. The declaration is a direct constant assignment with no further computation or lemmas.
Claim. The spatial dimension satisfies $D = 3$.
background
The module DifferentialGeometryFromRS derives differential geometric structures from Recognition Science principles. It posits a smooth 3-manifold as the recognition manifold, with five canonical structures corresponding to configDim D = 5. The RS metric is pseudo-Riemannian, yielding D+1 = 4 dimensional spacetime. This definition aligns with the upstream rsDimension declarations in LinearAlgebraFromRS and SuperstringTheoryFromRS, each setting the same value. The local setting follows the forcing chain where T8 forces D = 3 spatial dimensions.
proof idea
The declaration is a direct definition that assigns the constant value 3 to rsDimension. No lemmas are applied; it serves as a foundational constant shared across modules.
why it matters
This definition supplies the spatial dimension required by downstream constructions such as rsSpacetimeDim, which computes spacetime dimension as rsDimension + 1 = 4, and LinearAlgebraCert, which verifies dimension_3 : rsDimension = 3. It implements the T8 step of the forcing chain, where the eight-tick octave and self-similar fixed point phi force three spatial dimensions. The value anchors the alpha band and mass ladder calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.