atomCount_eq_8
plain-language theorem explainer
The theorem states that the number of atoms in the Boolean algebra on the three-dimensional vector space over F₂ equals 8. Researchers verifying the lattice structure of Q₃ in Recognition Science would cite this when confirming the atom count for the D=3 case. The proof is a one-line wrapper that applies the decide tactic to the direct definition of atomCount as 2^3.
Claim. The cardinality of the set of atoms in the Boolean algebra on the vector space $F_2^3$ equals 8.
background
The module treats the recognition lattice Q₃ = {0,1}³ as a Boolean algebra whose atoms number 2^3. The upstream definition sets atomCount to exactly this value 2^3, supplying the base cardinality. The module text notes that the Boolean lattice {0,1}³ has 2^3 = 8 atoms and links this count to the five canonical operations that match configDim D = 5.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic evaluates the equality atomCount = 8 by direct computation from the definition atomCount := 2^3.
why it matters
The result populates the eight_atoms field inside the BooleanAlgebraCert definition, which certifies the Boolean algebra properties derived from RS. It anchors the D = 3 case and the eight-atom count that appears in the eight-tick octave structure of the forcing chain. The module records zero sorries for this verification step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.