linearAlgebraCert
plain-language theorem explainer
The linearAlgebraCert definition constructs a certificate verifying that the recognition lattice admits exactly five linear algebra operations in three dimensions with the F_2 cube of size eight. Researchers modeling discrete space-time structures from the recognition forcing chain would cite this to confirm the algebraic setup matches D=3 and the eight-tick period. The proof is a direct structure instance that applies the pre-established equality theorems for operation count, dimension, and cube cardinality.
Claim. Let $C$ be the structure asserting that the cardinality of linear algebra operations equals 5, the recognition dimension equals 3, and the size of the $F_2^3$ cube equals 8. The definition supplies the instance of $C$ in which these three assertions hold simultaneously.
background
The module derives a linear algebra structure on the recognition lattice, identifying the space with $D=3$ dimensions, a basis of three vectors, and an orthogonal complement of three vectors. Five operations (addition, scalar multiplication, inner product, outer product, tensor product) arise as the configuration dimension for $D=3$. The lattice $Q_3 = F_2^3$ is treated as a three-dimensional vector space over $F_2$ whose cardinality is $2^3=8$, matching the recognition period.
proof idea
The definition builds the required structure by direct assignment: the operation count is taken from the theorem establishing five operations, the dimension equality is taken from the reflexivity proof that the recognition dimension is three, and the cube size is taken from the decision proof that the $F_2$ cube has eight elements. No further tactics or reductions are applied.
why it matters
This certificate certifies the linear algebra layer required by the recognition framework, directly instantiating the $D=3$ result from forcing step T8 and the eight-element period from the eight-tick octave at T7. It supplies the concrete algebraic object that later developments in the module can reference when connecting the recognition composition law to vector-space operations on the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.