pith. sign in
module module moderate

IndisputableMonolith.Mathematics.BooleanAlgebraFromRS

show as:
view Lean formalization →

Module BooleanAlgebraFromRS constructs a Boolean algebra from Recognition Science primitives. It defines BoolOp together with atom counts and certifies an eight-atom structure. The argument uses algebraic identities to match the eight-tick octave and three spatial dimensions.

claimBoolean algebra $B$ with operations $BoolOp$ such that $atomCount(B)=8$ and $atoms(B)cong 2^D$ for $D=3$.

background

The module sits in the Mathematics domain and imports Mathlib. It introduces BoolOp as the Boolean operations, atomCount as the atom enumeration, and BooleanAlgebraCert as the structure certificate. These connect directly to the eight-tick octave (period $2^3$) and the forcing chain step that yields $D=3$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Boolean algebra that feeds T7 (eight-tick octave) and T8 ($D=3$) in the UnifiedForcingChain. It closes the discrete structure needed before continuous limits and mass formulas appear downstream.

scope and limits

declarations in this module (7)