boolOpCount
plain-language theorem explainer
The inductive type of Boolean operations induced by the three-bit recognition lattice contains exactly five elements. Researchers verifying the Boolean algebra embedding in Recognition Science cite this count to confirm the operation basis matches configuration dimension D. The proof is a one-line decide tactic that evaluates the derived Fintype instance on the five constructors.
Claim. The finite type of canonical Boolean operations has cardinality five: $|B| = 5$ where $B = $ {AND, OR, NOT, NAND, NOR}.
background
The module shows that the recognition lattice Q₃ = {0,1}³ is a Boolean algebra whose F₂³ structure yields eight atoms. BoolOp is the inductive type whose five constructors are the canonical operations AND, OR, NOT, NAND, NOR; the Fintype instance is derived automatically from this definition. The local setting equates this operation count with configDim D = 5.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic computes the cardinality by enumerating the five constructors of the inductive type and confirming the Fintype.card value equals 5.
why it matters
The result supplies the five_ops field of BooleanAlgebraCert, which certifies the Boolean algebra structure inside the Recognition Science mathematics module. It directly supports the five-operation basis tied to D = 5 and the eight-atom count from the three-dimensional lattice, closing a basic verification step with no open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.