bnot
plain-language theorem explainer
Arithmetic negation on stable states maps each 0/1 bit value to its complement via subtraction from 1. Researchers constructing Boolean fragments from pre-logical cost minima cite this definition when verifying algebraic closure. The definition builds the output StableState directly and discharges the bit-stability obligation by case analysis on the input disjunction.
Claim. For a stable state $a$ whose bit lies in the set {0,1}, the negation is the stable state whose bit equals $1 - a.bit$.
background
StableState is the structure whose field bit is a real number together with the proposition is_bit asserting that bit equals 0 or 1. The module treats these objects as pre-logical configuration values constrained to the unit interval. The sole upstream dependency is the StableState structure itself, which supplies the carrier for the arithmetic operations band, bor and bnot.
proof idea
The definition is a one-line wrapper that refines the StableState constructor with bit value 1 - a.bit and then applies rcases to the is_bit disjunction, followed by simp on each case to confirm the resulting bit remains 0 or 1.
why it matters
bnot supplies the missing negation required by the theorem stable_forms_boolean_algebra, which states that the stable arithmetic states form a Boolean-style algebraic fragment. It is also invoked inside prelogical_boolean_fragment to establish that pre-logical arithmetic cost minima induce Boolean-style stable operations. In the Recognition Science chain this completes the pre-logical fragment before the lift to full logic from cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.