stable_forms_boolean_algebra
plain-language theorem explainer
Stable states restricted to 0/1 bits satisfy the arithmetic identities for conjunction via multiplication, disjunction via a + b - ab, and negation via 1 - a. Researchers deriving logic from pre-logical cost minima cite this to confirm the algebraic fragment before higher-level theorems. The proof is a direct term-mode verification that unfolds the operation definitions.
Claim. Let $S$ be the set of stable states where each $s$ satisfies $s.bit = 0$ or $s.bit = 1$. The operations then obey $band(a,b).bit = a.bit · b.bit$, $bor(a,b).bit = a.bit + b.bit - a.bit · b.bit$, and $bnot(a).bit = 1 - a.bit$ for all $a,b$ in $S$.
background
The module constrains pre-logical configurations to the unit interval. StableState is the structure pairing a real bit with the disjunction that it equals 0 or 1. The sibling definitions band, bor, and bnot implement arithmetic conjunction (multiplication), disjunction (a + b - ab), and negation (1 - a) while preserving the 0/1 constraint, as shown by their construction via rcases and simp on the is_bit cases.
proof idea
The term proof applies constructor to split the top-level conjunction into three goals. Each goal is handled by intro followed by rfl, which succeeds because the definitions of band, bor, and bnot were built exactly to match the stated bit equalities.
why it matters
This supplies the identities required by the downstream theorem prelogical_boolean_fragment, which states that pre-logical arithmetic cost minima induce Boolean-style stable operations. It anchors the extraction of logic from the cost structure in the foundation layer, prior to the forcing chain (T0-T8) and Recognition Composition Law that later yield dimensions and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.