rsDimension
plain-language theorem explainer
The declaration fixes the recognition dimension at the natural number 3. Workers constructing the F₂³ lattice or the five canonical linear-algebra operations cite this constant to set the spatial rank. The definition is a direct constant assignment that matches the T8 result of the forcing chain.
Claim. The spatial dimension of the recognition space is the natural number $3$.
background
The module shows that the recognition lattice carries a natural linear-algebra structure. The D=3 recognition space is identified with ℝ³, so dimension equals D, the basis has three vectors, and the orthogonal complement also has dimension three. Five canonical operations (addition, scalar multiplication, inner product, outer product, tensor product) therefore total configDim D = 5. The lattice Q₃ = F₂³ is a three-dimensional vector space over F₂ whose cardinality is 2³ = 8, coinciding with the recognition period.
proof idea
The definition is a direct constant assignment of the numeral 3. No lemmas or tactics are invoked; the value is supplied explicitly to satisfy the T8 step of the unified forcing chain.
why it matters
This constant supplies the dimension required by downstream objects such as rsSpacetimeDim := rsDimension + 1, the LinearAlgebraCert structure that records five operations together with dimension 3 and F₂-cube size 8, and the extraDimensions count in the superstring module. It implements the T8 forcing-chain step that fixes D = 3 spatial dimensions. The same numeral appears in the geometry and physics sibling modules, guaranteeing a single source of truth for the rank.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.