Foundation Pre Logical Cost Stable Forms Boolean Algebra

Stable states as Boolean algebra

Boolean algebra is the mathematics of true and false, usually written as 1 and 0. It underlies every digital circuit and every logical argument. The classical operations are conjunction (AND), disjunction (OR), and negation (NOT), with truth tables that are familiar to any programmer. What is less familiar is that these operations can be reconstructed from a purely numerical starting point, without ever mentioning truth values.

Start with a number that is allowed to lie anywhere between 0 and 1, inclusive. Define the cost of that number as the product of the number and its complement: cost = x(1 - x). The cost is zero exactly at the two endpoints, 0 and 1, and positive in between. A stable configuration is one that sits at a minimum of the cost, so stability picks out precisely the two boundary values. This is a theorem, proved in the machine-checked library of formal theorems: a state is stable if and only if its value is 0 or 1.

Now restrict attention to those stable states. On the set {0, 1}, define three operations by ordinary arithmetic: AND as multiplication (a AND b = a·b), OR as a + b - a·b, and NOT as 1 - a. These are the standard formulas for Boolean operations when truth is encoded as 1 and falsehood as 0. The framework's declaration stable_forms_boolean_algebra establishes, as a proved theorem, that these arithmetic definitions do indeed match the Boolean truth tables: the AND of two stable states equals their product, the OR equals a + b - a·b, and the NOT equals 1 - a. In plain language, the stable states of this cost function form a Boolean algebra.

In Recognition Science, this result is a small but load-bearing step. The framework models reality as a ledger, a discrete record of recognition events, and derives physical constants from a forced cost function. The pre-logical cost here is a simpler precursor: it shows that before any logical structure is assumed, the mere requirement that costs be minimized forces a two-valued, Boolean-compatible space. The theorem does not claim that this cost function is the same as the full recognition cost J(x) = (x + 1/x)/2 - 1; it is a separate, earlier construction. Nor does it claim that Boolean algebra is the only possible logic, only that this particular cost structure yields it.

What the result changes is the conceptual order. Instead of taking logic as a primitive, one can derive a Boolean fragment from a cost-minimization principle. The step from stable 0/1 states to full Boolean algebra, including properties like associativity and distributivity, remains a target for formalization; the current theorem covers only the three basic operations.

/-- Stability is equivalent to the two boundary values `0` and `1`. -/
theorem stable_iff_boundary (s : PreState) :
    IsStable s ↔ s.val = 0 ∨ s.val = 1 := by
  unfold IsStable preCost
  constructor
  · intro h
    have hfact : s.val * (1 - s.val) = 0 := h
    rcases mul_eq_zero.mp hfact with h0 | h1
    · exact Or.inl h0
    · right
      linarith
  · intro h
    rcases h with h0 | h1
    · simp [h0]
    · simp [h1]

/-- 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

This theorem does not prove that the pre-logical cost is the same as the recognition cost J(x). It does not establish that Boolean algebra is the only possible logic. It does not derive the full set of Boolean algebra laws, only the three basic operations.

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: