BoolOp
plain-language theorem explainer
The inductive definition enumerates the five canonical Boolean operations AND, OR, NOT, NAND, NOR on the recognition lattice Q₃ = F₂³. A researcher formalizing Boolean structure inside the Recognition Science framework would cite it to fix the operation count at five and tie it to configuration dimension D=5. The declaration is a direct inductive enumeration that derives Fintype, DecidableEq, Repr, and BEq instances automatically.
Claim. Let $B$ be the set whose elements are the five operations AND, OR, NOT, NAND, NOR, equipped with decidable equality and finite cardinality.
background
The module treats the recognition lattice Q₃ = {0,1}³ as a Boolean algebra whose underlying vector space is F₂³. This space has cardinality 8 = 2³ and therefore eight atoms; its Boolean operations are taken to number five, matching configuration dimension D=5. The module doc states that the five operations AND, OR, NOT, NAND, NOR supply the concrete generators for this algebra on the three-dimensional lattice.
proof idea
The declaration is an inductive definition that lists the five constructors directly and derives the Fintype, DecidableEq, Repr, and BEq instances via the deriving clause; no lemmas are applied.
why it matters
This definition supplies the five operations required by the downstream BooleanAlgebraCert structure, which records Fintype.card BoolOp = 5 together with the atom count 8 = 2³. It anchors the Boolean construction to spatial dimension D=3 in the forcing chain and to the eight-tick octave. The sibling theorem boolOpCount then proves the cardinality statement by decision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.