bor
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply to real numbers outside the 0/1 constraint.
- Does not claim a complete Boolean algebra without the companion operations band and bnot.
- Does not extend the construction to non-stable or continuous configurations.
formal statement (Lean)
47def bor (a b : StableState) : StableState := by
proof body
Definition body.
48 refine ⟨a.bit + b.bit - a.bit * b.bit, ?_⟩
49 rcases a.is_bit with ha | ha <;> rcases b.is_bit with hb | hb <;> simp [ha, hb]
50
51/-- Arithmetic negation on stable states (`1 - a` on `0/1`). -/