atoms_eq_2cubeD
plain-language theorem explainer
The Boolean lattice on the recognition space Q₃ = {0,1}³ has exactly eight atoms. Researchers formalizing the Boolean algebra embedding in Recognition Science cite this equality to confirm the atom count matches the dimension of F₂³. The proof reduces immediately to reflexivity on the definition of atomCount.
Claim. The number of atoms in the Boolean lattice on the vector space $F_2^3$ equals $2^3$.
background
The module constructs Boolean algebra directly from the recognition lattice Q₃ identified with {0,1}³. The definition atomCount : ℕ := 2 ^ 3 encodes the eight elements of F₂³ as atoms of the lattice. This matches the framework derivation of D = 3 from the eight-tick octave in the forcing chain T7-T8.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of atomCount.
why it matters
This supplies the atoms_2cubeD field inside the BooleanAlgebraCert definition, which certifies five operations together with eight atoms. It anchors the lattice structure on Q₃ inside Recognition Science and aligns with the recognition composition law. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.