BooleanAlgebraCert
plain-language theorem explainer
BooleanAlgebraCert packages the cardinality facts for the Boolean algebra on the recognition lattice Q₃: five operations from the inductive type BoolOp and eight atoms equal to 2³. Researchers verifying the lattice structure in Recognition Science mathematics would cite it when confirming the match to the eight-tick octave. The declaration is a plain structure that aggregates the atomCount definition and the Fintype instance on BoolOp.
Claim. A structure asserting that the set of Boolean operations has cardinality 5, the atom count equals 8, and the atom count equals $2^3$.
background
The module derives Boolean algebra structure on the recognition lattice Q₃ = {0,1}³. BoolOp is the inductive type with constructors AND, OR, NOT, NAND, NOR. atomCount is defined as 2^3 to count the atoms of the three-dimensional lattice.
proof idea
This is a structure definition that directly records the three cardinality statements. It relies on the upstream definition of atomCount as 2^3 and the inductive definition of BoolOp with five constructors. No tactics are applied.
why it matters
The structure is instantiated by booleanAlgebraCert to witness the Boolean algebra properties. It connects to T8 in the forcing chain where D=3 yields the eight-tick octave period 2^3 and five operations matching configDim D=5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.