Foundation Pre Logical Cost Stable Iff Boundary

Stability and the boundary

A recognition event, a discrete record of a choice, begins as a value on a line. The framework's pre-logical stage, the stage before any logical structure exists, constrains this value to the unit interval from 0 to 1. The cost of holding a value is defined as the product of the value and its complement: cost = v(1 - v). This is a parabola opening downward, zero at the endpoints and maximal at the midpoint. The declaration stable_iff_boundary, a theorem in the machine-checked library of formal theorems, proves that a configuration is stable exactly when its value is 0 or 1. Stability, defined as zero cost, occurs only at the boundary.

The theorem's content is plain: of all the points on the interval, only the two ends survive the cost constraint. The midpoint, where the cost is highest, is the least stable point. This is not a statement about physics or about any particular system. It is a statement about a cost function and its minima. The proof is a short algebraic check: the product v(1 - v) equals zero if and only if v is zero or one, given that v lies in the unit interval.

In Recognition Science, this boundary result is the seed of logical structure. The stable states, the two endpoints, become arithmetic encodings of truth values. The framework defines a stable state as a value that is either 0 or 1, then builds operations on these states: conjunction as multiplication, disjunction as a + b - ab, and negation as 1 - a. A second theorem, stable_forms_boolean_algebra, proves that these operations satisfy the equations of a Boolean-style algebraic fragment. The cost function's minima, the boundary points, thus carry the structure of logic. The framework models the emergence of logical operations from a cost constraint, not the other way around.

The theorem does not claim that real-world logic is this cost function. It does not claim that the midpoint is forbidden or that any actual process must land on the boundary. It establishes an equivalence within a defined mathematical structure: stability, as defined by this cost, is equivalent to being at the boundary. The step from this algebraic fragment to full logical reasoning, or to any physical system, is not part of the declaration. What the theorem changes is the starting point: logical operations can be derived from a cost minimum, which gives the framework a foundation for structure that is not assumed but forced.

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

The midpoint state is not forbidden or physically impossible; it is merely not a cost minimum. The theorem does not claim that real-world logical systems are governed by this specific cost function. The Boolean-style fragment is not a proof of full logical reasoning, which remains a separate target.

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: