linearAlgebraOpCount
plain-language theorem explainer
The inductive type of linear algebra operations on the D=3 recognition lattice contains exactly five elements. Researchers confirming the dimension of the operation space in Recognition Science would cite this cardinality when assembling the linear algebra certificate. The proof is a one-line decision procedure that enumerates the constructors of the inductive definition.
Claim. The set of canonical linear algebra operations on the three-dimensional recognition space has cardinality five: $5 = |$ {addition, scalar multiplication, inner product, outer product, tensor product} $|$.
background
The module defines a linear algebra structure on the recognition lattice for D=3. The recognition space is identified with ℝ³, so dimension equals 3, with a basis of three vectors and an orthogonal complement of three vectors. Five operations are introduced by the inductive type with constructors addition, scalar multiplication, inner product, outer product, and tensor product; this count equals configDim D. The underlying lattice is the three-dimensional vector space over F₂ whose order is 8, matching the recognition period 2³.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes the cardinality directly from the derived Fintype instance on the inductive type by counting its five constructors.
why it matters
This result populates the five_ops field of the linearAlgebraCert definition, which also records the dimension-3 and F₂³-size-8 facts. It supports the claim that the recognition lattice carries a natural linear algebra structure with exactly five operations when D=3, aligning with the T8 forcing step that fixes three spatial dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.