Foundation Pre Logical Cost Band

The pre-logical band

A recognition event, in the Recognition Science framework, is a discrete record of something being noticed, and the framework's central claim is that the cost of noticing is forced, not chosen. The declaration band is the framework's first step: it defines a pre-logical configuration as a real number between 0 and 1, and assigns it a cost by the formula s(1 − s). This is a parabola that opens downward, so its minima sit at the two ends of the interval, at 0 and at 1.

The framework proves that a configuration is stable exactly when it sits at one of those two boundary values. In plain words, the only configurations that cost nothing are the two extremes, and every interior point costs something positive. The framework then names those two stable states bits, and shows that they carry the usual logical operations: multiplication gives conjunction, a + b − ab gives disjunction, and 1 − a gives negation. The machine-checked library of formal theorems verifies that these operations on the two stable states form a Boolean-style algebraic fragment, meaning they behave like the familiar truth tables of classical logic.

What the band does not claim is just as important. It does not claim that logic emerges from physics, or that the framework has derived the fine-structure constant, or that the Riemann Hypothesis is proved. The band is a definitional choice, a model of how a pre-logical cost could give rise to two-valued logic; it is not a derivation of that logic from something deeper. The framework's larger forcing chain, which derives the golden ratio and the number of spatial dimensions, is a separate set of theorems; the band does not by itself force those results.

What the band changes is the starting point: it gives a concrete, minimal picture of how a cost function can single out exactly two stable states, and those two states are enough to carry Boolean logic. A reader can now see the framework's first step as a deliberate modeling choice, with its scope clearly marked, rather than as a claim about the ultimate nature of logic.

/-- Pre-logical configuration value constrained to the unit interval. -/
structure PreState where
  val : ℝ
  in_unit_interval : 0 ≤ val ∧ val ≤ 1

/-- Pre-logical cost landscape on `[0,1]`: minima occur at the boundary states. -/
noncomputable def preCost (s : PreState) : ℝ := s.val * (1 - s.val)

/-- 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 band does not derive classical logic from physics; it defines a model whose stable states happen to carry Boolean operations. The band does not by itself force the golden ratio, the eight-tick cycle, or three spatial dimensions. The band says nothing about the fine-structure constant or the Riemann Hypothesis.

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: