q3Exponent_eq_2
plain-language theorem explainer
The theorem states that the exponent of the recognition lattice Q₃ equals 2. Researchers verifying the algebraic properties of Q₃ as (ℤ/2)³ in Recognition Science derivations would cite this result. The proof is a one-line reflexivity wrapper on the definition of q3Exponent.
Claim. The exponent of the group $Q_3$ equals 2, where $Q_3$ denotes the recognition lattice of dimension 3.
background
The module introduces the recognition lattice Q₃ with natural algebraic structure as the group (ℤ/2)³. Key facts include |Q₃| = 8 = 2^3 = 2^D, that (ℤ/2)³ is abelian, and that the exponent equals 2 (every element has order 1 or 2). This supports five canonical algebraic structures (group, ring, field, module, algebra) for dimension D = 3.
proof idea
This is a one-line wrapper that applies reflexivity to the definition q3Exponent : ℕ := 2.
why it matters
The result feeds directly into abstractAlgebraCert, which packages the algebraic certification for Q₃ including q3_exp_2. It supports the framework landmark that |Q₃| = 2^D with exponent 2, consistent with the eight-tick octave and D = 3 spatial dimensions. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.