f2CubeSize_eq_8
plain-language theorem explainer
f2CubeSize_eq_8 establishes that the cardinality of the three-dimensional vector space over F₂ equals eight. Researchers certifying the linear algebra structure of the Recognition Science lattice cite it when packaging dimension and period facts. The proof is a one-line wrapper that applies the decide tactic to evaluate the definition directly.
Claim. $|F_2^3| = 8$, where $F_2^3$ is the three-dimensional vector space over the field with two elements and the dimension equals the recognition space dimension D.
background
The module equips the recognition lattice with a natural linear algebra structure over the D=3 recognition space identified with ℝ³. Dimension equals D=3, with basis and orthogonal complement each of size D. The D=3 lattice Q₃ = F₂³ forms a three-dimensional vector space over F₂ whose cardinality is 2³ = 8, matching the recognition period. This rests on the upstream definition f2CubeSize := 2 ^ rsDimension.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality f2CubeSize = 8. The definition f2CubeSize := 2 ^ rsDimension reduces the claim to the concrete computation 2^3 = 8, which decide verifies without further lemmas.
why it matters
The result is used inside linearAlgebraCert to certify five canonical operations, dimension three, and F₂-cube size eight. It fills the verification of the eight-tick octave period 2³ and D=3 spatial dimensions in the Recognition Science forcing chain (T7, T8). The module records zero sorry and zero axiom for this linear algebra setup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.