LinearAlgebraOp
LinearAlgebraOp enumerates the five canonical operations on the D=3 recognition space. Researchers establishing the linear algebra structure of the recognition lattice cite this definition when counting operations or certifying dimension. The declaration is a direct inductive type with derived Fintype, Repr, and DecidableEq instances.
claimThe finite type of linear algebra operations on the three-dimensional recognition space consists of addition, scalar multiplication, inner product, outer product, and tensor product.
background
The module states that the recognition lattice carries a natural linear algebra structure with D=3 recognition space identified with ℝ³. This yields a basis of three vectors, an orthogonal complement of dimension three, and exactly five operations matching configDim D=5. The D=3 lattice Q₃ = F₂³ forms a vector space over F₂ with cardinality 2³=8, matching the recognition period.
proof idea
The declaration is an inductive definition that directly lists the five constructors. Automatic derivation of the Fintype instance supplies the cardinality computation used by the downstream linearAlgebraOpCount theorem.
why it matters in Recognition Science
LinearAlgebraOp supplies the five operations required by the LinearAlgebraCert structure, which asserts five_ops = 5, dimension_3 = 3, and f2cube_8 = 8. It anchors the linear algebra foundation for the D=3 case in the forcing chain, where the eight-tick octave appears as |F₂³|=8. The definition supports certification that the recognition lattice admits precisely these operations.
scope and limits
- Does not encode algebraic relations among the five operations.
- Does not derive inner-product properties from the recognition composition law.
- Does not link the operations to the phi-ladder or mass formula.
- Does not address non-D=3 cases.
formal statement (Lean)
25inductive LinearAlgebraOp where
26 | addition | scalarMul | innerProduct | outerProduct | tensorProduct
27 deriving DecidableEq, Repr, BEq, Fintype
28