q3Size
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.