q3Size
The definition assigns the cardinality of the recognition lattice Q₃ the value 8. Researchers deriving algebraic structures from Recognition Science cite this when confirming that (ℤ/2)³ has order 2^D. It is introduced by direct assignment matching the eight-tick octave.
claimThe cardinality of the recognition lattice $Q_3$ is defined as $8$.
background
The module shows that the recognition lattice Q₃ carries natural algebraic structure as the group (ℤ/2)³. Key facts listed are that its cardinality equals 8, which is 2^3 and also 2^D for D=3 spatial dimensions, that the group is abelian, and that its exponent is 2. The module further notes five canonical algebraic structures (group, ring, field, module, algebra) corresponding to configDim D = 5.
proof idea
One-line definition that directly sets the natural number q3Size to 2^3.
why it matters in Recognition Science
This definition supplies the concrete cardinality required by AbstractAlgebraCert to certify five algebraic structures on Q₃ together with q3Size = 8. It aligns with the eight-tick octave (T7) and D = 3 from the forcing chain. The sibling theorem q3Size_eq_8 then confirms the value by decision.
scope and limits
- Does not prove the isomorphism of Q₃ to (ℤ/2)³.
- Does not derive the five algebraic structures.
- Does not invoke the Recognition Composition Law.
- Does not address constants such as alpha or mass formulas.
Lean usage
theorem q3Size_eq_8 : q3Size = 8 := by decideformal statement (Lean)
29def q3Size : ℕ := 2 ^ 3