bor
plain-language theorem explainer
The bor definition equips StableState with arithmetic disjunction, returning the state whose bit equals a.bit + b.bit - a.bit * b.bit. Researchers deriving Boolean fragments from pre-logical cost minima cite it when assembling the arithmetic operations that satisfy the 0/1 constraint. The construction refines the StableState pair and verifies stability by exhaustive case split on the two is_bit disjunctions followed by simplification.
Claim. For stable states $a$ and $b$ whose bits lie in the set ${0,1}$, the disjunction $a$ OR $b$ is the stable state whose bit value equals $a.bit + b.bit - a.bit · b.bit$.
background
StableState is the structure whose field bit : ℝ carries an arithmetic 0/1 encoding together with the predicate is_bit : bit = 0 ∨ bit = 1. The module PreLogicalCost treats these objects as pre-logical configuration values constrained to the unit interval. The definition bor builds directly on this structure to supply the missing disjunction operation.
proof idea
One-line wrapper that refines a new StableState whose bit component is the arithmetic expression a.bit + b.bit - a.bit * b.bit. The proof obligation is discharged by rcases on both is_bit fields followed by simp on the resulting 0/1 cases.
why it matters
bor supplies the disjunction clause required by the downstream theorems stable_forms_boolean_algebra and prelogical_boolean_fragment. The latter states that pre-logical arithmetic cost minima induce Boolean-style stable operations; the former asserts that the three operations band, bor and bnot together form a Boolean-style algebraic fragment. This places the definition at the interface between the Recognition Science cost function and the emergence of classical logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.