LinearAlgebraCert
plain-language theorem explainer
LinearAlgebraCert packages the three numerical invariants of the RS linear algebra into one structure: exactly five operations on the recognition space, dimension fixed at 3, and the F₂-cube of size 8. The downstream linearAlgebraCert consumes it by supplying the concrete equality lemmas. The declaration is a pure structure definition carrying no proof obligations.
Claim. Let $L$ be the inductive type whose constructors are addition, scalar multiplication, inner product, outer product, and tensor product. LinearAlgebraCert is the structure type whose fields assert that the cardinality of $L$ equals 5, that the recognition dimension equals 3, and that the cardinality of the three-dimensional vector space over $F_2$ equals 8.
background
The module equips the recognition lattice with a linear algebra structure over the three-dimensional space $D=3$. Five canonical operations are enumerated by the inductive type LinearAlgebraOp. The $F_2$-cube $Q_3=F_2^3$ has cardinality $2^3=8$, matching the recognition period. rsDimension is defined as the constant 3 and f2CubeSize as $2$ raised to rsDimension, both imported from the differential geometry module that first fixes the dimension.
proof idea
LinearAlgebraCert is introduced directly as a structure whose three fields are the statements Fintype.card LinearAlgebraOp = 5, rsDimension = 3, and f2CubeSize = 8. No lemmas or tactics are invoked inside the declaration; it functions as a record type.
why it matters
The structure collects the linear-algebraic consequences of $D=3$ and the eight-tick octave into a single certificate. It is consumed by linearAlgebraCert, which supplies the equalities linearAlgebraOpCount, rsDimension_eq_3, and f2CubeSize_eq_8. This realizes the claim that the recognition lattice carries a natural five-operation linear algebra whose underlying $F_2$-space has order 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.