Foundation Pre Logical Cost Stable State

Stable states as bits

A stable state is the simplest object in the Recognition Science account of how a discrete record of events, its ledger, can hold a value that does not drift. The framework defines a pre-logical configuration as a real number between 0 and 1, and assigns it a cost by the formula s(1 − s). That cost is 0 only at the two endpoints, 0 and 1, and positive everywhere in between. The declaration StableState packages exactly those two endpoints: a stable state is a real number that is either 0 or 1, nothing else. The theorem stable_iff_boundary proves this equivalence: a configuration is stable precisely when its value sits on the boundary of the unit interval.

The point of restricting to these two values is that they carry arithmetic. The framework defines three operations on stable states: conjunction as multiplication (0·0 = 0, 0·1 = 0, 1·1 = 1), disjunction as a + b − ab, and negation as 1 − a. Each operation takes a stable state to a stable state, and the theorem stable_forms_boolean_algebra proves that these three operations obey the identities of Boolean algebra. In plain terms, the two stable values 0 and 1, together with these arithmetic operations, form a working two-valued logic. The framework models the birth of Boolean logic as an arithmetic fact about the only two costs that a pre-logical ledger can hold without changing.

What the declaration does not claim is just as important. It does not claim that 0 and 1 are the only numbers that exist, only the only stable ones under this particular cost. It does not claim that the cost function s(1 − s) is forced by the deeper Recognition Science axioms; that forcing happens later in the framework's chain, and this declaration stands before it. And it does not claim that Boolean algebra is the whole of logic, only that this two-valued fragment emerges from stable arithmetic. The declaration is a definitional choice plus a proved equivalence, not a claim about how human reasoning works.

What the declaration changes is the starting point for everything the framework builds afterward. Once stable states are exactly the bits 0 and 1, the framework has a concrete, machine-checked foundation for logical operations that does not assume logic as a primitive. The reader can now see that the framework's first step is not a philosophical assertion about truth, but a proved fact about which configurations survive the cost of recognition.

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

/-- Stable states as arithmetic 0/1 encodings. -/
structure StableState where
  bit : ℝ
  is_bit : bit = 0 ∨ bit = 1

What this page does not claim

The cost function s(1 − s) is not claimed to be forced by deeper Recognition Science axioms in this declaration. The framework does not claim that Boolean algebra is the whole of logic, only that this two-valued fragment emerges from stable arithmetic. The declaration does not claim that 0 and 1 are the only numbers that exist, only the only stable ones under this cost.

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: