Mathematics Boolean Algebra From Rs Bool Op Count

The five operations

Boolean algebra is the mathematics of truth values: true and false, combined by operations such as AND, OR, and NOT. On a set of truth values, the standard operations are AND, OR, NOT, NAND, and NOR. The first is true only when both inputs are true; the second is true when at least one input is true; NOT flips a single value; NAND is the negation of AND; NOR is the negation of OR. These five are the familiar building blocks of digital logic circuits.

In the Recognition Science framework, the declaration boolOpCount is a machine-checked theorem stating that the set of these five operations has exactly five elements. The proof is a direct computation: it defines the five operations and then verifies by exhaustive checking that no other operations are listed. The framework's library, a machine-checked collection of formal theorems, records this as a proved fact with no unproved assumptions.

The declaration also records that the underlying set of three truth-value positions has 2^3 = 8 atoms, meaning eight possible combinations of three binary choices. This matches the classical fact that a three-variable Boolean function has 2^3 = 8 input rows. The framework packages these two counts together as a certificate: five operations and eight atoms.

What the declaration does not claim is more important. It does not claim that Recognition Science derives or explains Boolean algebra. The theorem merely counts a list of operations that the framework chooses to call the five canonical ones. It does not prove that these are the only possible Boolean operations, nor that the framework's recognition lattice produces Boolean algebra. The count is a definitional choice, not a derivation.

In plain terms: the declaration says "there are five named operations," and that is all. It is a small, exact, machine-checked fact. The classical theory of Boolean algebra, with its laws and completeness theorems, stands independently of this count.

theorem boolOpCount : Fintype.card BoolOp = 5 := by decide

theorem atomCount_eq_8 : atomCount = 8 := by decide

structure BooleanAlgebraCert where
  five_ops : Fintype.card BoolOp = 5
  eight_atoms : atomCount = 8
  atoms_2cubeD : atomCount = 2 ^ 3

What this page does not claim

The declaration does not prove that AND, OR, NOT, NAND, and NOR are the only possible Boolean operations. The declaration does not derive Boolean algebra from Recognition Science principles. The declaration does not establish any connection between the recognition lattice and classical Boolean algebra beyond the counts.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/BooleanAlgebraFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: