atomCount
plain-language theorem explainer
The definition assigns the natural number two to the power three as the count of atoms in the Boolean lattice on the three-dimensional space over F two. Researchers deriving Boolean algebra from the Recognition Science forcing chain cite it to fix the atom count at eight for the lattice Q three. The definition is introduced by direct constant assignment with no computation or lemmas applied.
Claim. The number of atoms in the Boolean algebra on the vector space $F_2^3$ is defined to be $2^3$.
background
The module Boolean Algebra from RS identifies the recognition lattice Q three with the set {0,1} cubed, which carries the structure of a Boolean algebra over F two. It notes that this lattice has eight atoms, matching the cardinality of F two cubed, and links five canonical operations to configDim D equals five. The local setting is the extraction of Boolean algebra directly from the RS framework with zero sorry statements.
proof idea
The definition is a direct constant assignment of two raised to the power three.
why it matters
This supplies the eight_atoms field inside the BooleanAlgebraCert structure, which also records five operations and the equality to two cubed. It anchors the Boolean algebra construction to the eight-tick octave (period 2 cubed) and D equals three spatial dimensions from the forcing chain T7 and T8. The definition closes the base count needed for the certification that the lattice matches the RS-derived Boolean structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.