q3Size_eq_8
plain-language theorem explainer
The theorem establishes that the recognition lattice Q₃ has cardinality exactly 8. Researchers extracting algebraic structure from the recognition lattice would cite this when confirming the 2^D count for D=3. The proof is a one-line decision procedure that reduces the equality directly from the definition of q3Size as 2^3.
Claim. The cardinality of the recognition lattice $Q_3$ equals 8.
background
In the Recognition Science framework the recognition lattice Q₃ is introduced as the abelian group (ℤ/2)³. The sibling definition q3Size sets this cardinality explicitly to 2^3. The module derives five canonical algebraic structures (group, ring, field, module, algebra) from the lattice and notes that the count equals 2^D with D=3 the spatial dimension fixed by the forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality q3Size = 8, which holds immediately by unfolding the definition q3Size := 2^3.
why it matters
This supplies the size component inside the abstractAlgebraCert definition that bundles the five structures together with the Q₃ properties. It directly instantiates the framework landmark that D=3 yields an eight-element group (2^D) and closes the cardinality fact needed for the abstract-algebra extraction step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.