AbstractAlgebraCert
plain-language theorem explainer
The AbstractAlgebraCert structure bundles three invariants of the recognition lattice Q₃: exactly five algebraic structures (group, ring, field, module, algebra), cardinality 8, and exponent 2. A researcher tracing abstract algebra back to the Recognition Science forcing chain would cite this certificate to lock in the Q₃ group facts before proceeding to ring or module constructions. The declaration is a plain structure definition with no computational body or lemmas.
Claim. Let $Q_3$ be the recognition lattice for configuration dimension $D=3$. The certificate asserts that the inductive type of algebraic structures (group, ring, field, module, algebra) has cardinality 5, that $|Q_3|=8$, and that the exponent of $Q_3$ equals 2.
background
The module shows that the recognition lattice $Q_3$ carries the structure of the abelian group $(ℤ/2ℤ)^3$. Its size is given by the definition q3Size := $2^3$, which equals the eight-tick octave period. The exponent is fixed by q3Exponent := 2, so every non-identity element squares to the identity. AlgebraicStructure is the inductive enumeration of the five canonical structures whose Fintype.card is asserted to be 5 when the configuration dimension is $D=3$ (see the parallel enumeration in AlgebraicStructuresFromConfigDim).
proof idea
This is a structure definition that directly records the three field values. No tactics, reductions, or upstream lemmas are invoked; the body simply states the three equalities using the sibling definitions q3Size, q3Exponent, and Fintype.card of AlgebraicStructure.
why it matters
The certificate supplies the numerical invariants required by the downstream definition abstractAlgebraCert, which constructs an explicit instance. It confirms the module claim that $|Q_3|=8=2^D$ and that five algebraic structures arise for $D=3$, directly instantiating the T7 eight-tick octave and T8 spatial-dimension steps of the forcing chain. No open questions or scaffolding remain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.