f2CubeSize
plain-language theorem explainer
The definition assigns to f2CubeSize the cardinality of the F₂ lattice over the recognition space as two raised to the recognition dimension. Researchers working on the linear algebra layer of the recognition lattice cite this when confirming the eight-element period. It is realized as a direct abbreviation that substitutes the fixed dimension constant.
Claim. Let $D$ be the recognition dimension. The cardinality of the lattice $Q_D = F_2^D$ is defined as $2^D$.
background
The module LinearAlgebraFromRS equips the recognition lattice with vector space structure over F₂. The space is identified with R³, so the lattice Q₃ = F₂³ is a three-dimensional vector space whose cardinality equals the recognition period. The upstream definition rsDimension fixes this dimension at three in the mathematics, differential geometry, and superstring modules.
proof idea
The definition is a one-line abbreviation that directly applies exponentiation to the constant rsDimension.
why it matters
This definition supplies the lattice cardinality required by the downstream LinearAlgebraCert structure and the theorem f2CubeSize_eq_8. It encodes the eight-tick octave (period 2³) of the recognition framework and closes the link between D = 3 and the F₂³ lattice size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.