q3Exponent_eq_2
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish the group isomorphism Q₃ ≅ (ℤ/2)³.
- Does not derive the exponent value from Recognition Science axioms.
- Does not address ring or field structures on Q₃.
Lean usage
example : q3Exponent = 2 := q3Exponent_eq_2formal statement (Lean)
34theorem q3Exponent_eq_2 : q3Exponent = 2 := rfl
proof body
35