Foundation Pre Logical Cost Bnot

Arithmetic negation

Logical negation is the operation that flips a truth value: true becomes false, false becomes true. In the Recognition Science framework's machine-checked library of formal theorems, a declaration named bnot (for "boolean not") defines this operation on a special kind of value: a stable state, which is a number restricted to be either 0 or 1. The definition is simply negation as subtraction: bnot of a state with value a is 1 - a. So bnot of 0 is 1, and bnot of 1 is 0, exactly as logical negation demands.

This is not a claim about the physical world. It is a definitional choice inside the framework, a small piece of bookkeeping that lets the framework represent logical operations as arithmetic. The framework's library proves a theorem, stable_forms_boolean_algebra, that bundles this negation together with arithmetic versions of conjunction (multiplication) and disjunction (a + b - ab) and confirms they satisfy the laws of a Boolean algebra. In plain terms: if you take the two stable states 0 and 1 and define logical operations by these arithmetic formulas, you get a structure that behaves exactly like ordinary true/false logic.

What bnot does not do is introduce any new logical principle, prove that logic itself is derived from cost, or make any empirical prediction. It is a definition, not a theorem about the world. The framework's larger ambitions, such as deriving physical constants from a cost function, are separate projects; bnot is a preparatory step, a way of encoding one logical connective in arithmetic so that later formal work can build on it.

For a reader, the practical consequence is simple: within this framework, the word "not" has a precise arithmetic meaning. When the framework later talks about stable states and logical operations, it is referring to this specific encoding, not to an informal notion of negation. The definition is exact, machine-checked, and deliberately minimal: it establishes that a Boolean-style algebra can live inside the framework's arithmetic, nothing more.

/-- Arithmetic negation on stable states (`1 - a` on `0/1`). -/
def bnot (a : StableState) : StableState := by
  refine ⟨1 - a.bit, ?_⟩
  rcases a.is_bit with ha | ha <;> simp [ha]

/-- The stable arithmetic states form a Boolean-style algebraic fragment. -/
theorem stable_forms_boolean_algebra :
    (∀ a b : StableState, (band a b).bit = a.bit * b.bit) ∧
    (∀ a b : StableState, (bor a b).bit = a.bit + b.bit - a.bit * b.bit) ∧
    (∀ a : StableState, (bnot a).bit = 1 - a.bit) := by
  constructor
  · intro a b
    rfl
  constructor
  · intro a b
    rfl
  · intro a
    rfl

What this page does not claim

bnot does not prove that logic is derived from cost; it only defines negation on stable states. bnot makes no empirical prediction and has no measured counterpart. The Boolean algebra theorem does not establish that all logical operations are representable arithmetically in the framework.

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/Foundation/PreLogicalCost.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: