f2CubeSize_eq_8
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 in Recognition Science
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.
scope and limits
- Does not derive rsDimension from Recognition Science axioms.
- Does not prove properties of the five linear algebra operations.
- Does not connect to physical constants or mass formulas.
Lean usage
example : f2CubeSize = 8 := f2CubeSize_eq_8formal statement (Lean)
35theorem f2CubeSize_eq_8 : f2CubeSize = 8 := by decide
proof body
36