booleanAlgebraCert
plain-language theorem explainer
The declaration supplies a concrete certificate confirming that the Boolean algebra on the three-dimensional recognition lattice has five canonical operations and eight atoms. A mathematician modeling discrete recognition structures would cite this to verify the algebraic counts match the RS lattice Q₃. It is assembled by direct assignment of the operation count from boolOpCount and the atom equalities from the decidable theorems atomCount_eq_8 and atoms_eq_2cubeD.
Claim. Let BoolOp denote the set of Boolean operations on the lattice and atomCount the number of atoms in Q₃ = {0,1}³. The structure BooleanAlgebraCert is witnessed by the assignments card(BoolOp) = 5, atomCount = 8, and atomCount = 2³.
background
The module shows that the recognition lattice Q₃ = {0,1}³ is a Boolean algebra whose elements are vectors over F₂. It has exactly eight atoms because |F₂³| = 8 = 2³, and it supports five canonical operations (AND, OR, NOT, NAND, NOR) whose count equals configDim D = 5. The structure BooleanAlgebraCert packages these three facts into a single record whose fields are five_ops : Fintype.card BoolOp = 5, eight_atoms : atomCount = 8, and atoms_2cubeD : atomCount = 2³.
proof idea
The definition constructs the BooleanAlgebraCert record by assigning the five_ops field to the theorem boolOpCount, the eight_atoms field to atomCount_eq_8, and the atoms_2cubeD field to atoms_eq_2cubeD. It is a direct structure construction that relies on the prior decidable proofs for each count.
why it matters
This definition supplies the concrete certificate that the Boolean algebra on Q₃ satisfies the expected operation and atom counts, directly supporting the claim that the lattice is Boolean with |F₂³| = 8 atoms and five operations. It fills the algebraic-count step in the module's treatment of the recognition lattice and aligns with the eight-tick octave and D = 3 landmarks of the forcing chain. No downstream uses are recorded, leaving open its later application to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.