Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PreLogicalCost

show as:
view Lean formalization →

Defines pre-logical configurations as values in the unit interval and a cost functional on them. Stable (zero-cost boundary) states are shown to carry Boolean operations and form a Boolean algebra. Cited by anyone deriving classical logic from cost minimization. The module is definitional plus elementary stability and algebra lemmas.

claimA pre-logical state is a configuration $s$ with value in $[0,1]$. A cost $C(s)\ge 0$ is assigned; $s$ is stable when $C(s)=0$, equivalently when $s$ lies on the boundary $\{0,1\}$. On stable states one defines meet, join, and complement, and these operations make the stable set a Boolean algebra.

background

Recognition Science treats logical consistency as an emergent, cost-minimizing property rather than a primitive. Before any object-language connectives exist, one needs a bare configuration space and a real-valued cost that can select preferred states.

This module supplies that layer. A pre-state is a configuration valued in the unit interval. The pre-cost functional marks interior points as costly and the endpoints ${0,1}$ as free. Stability is the zero-cost condition; an equivalence lemma identifies stable states with the Boolean boundary.

Boolean meet, join, and negation are then defined only on that stable set. The construction is deliberately pre-logical: no inference rules are assumed, only a cost and its minimizers.

proof idea

Most of the file is definitional: pre-state, pre-cost, the stability predicate, and the three Boolean operations on stable states. The main theorem content is an iff linking stability to the boundary ${0,1}$, then a short verification that the stable set with those operations satisfies the Boolean algebra axioms. No deep analytic machinery; the argument is elementary real arithmetic on $[0,1]$ plus algebraic checks.

why it matters in Recognition Science

Feeds the parent module LogicFromCost, whose thesis is that logical consistency is a cost-minimizing state. That module needs a concrete configuration space, a cost, and a proof that zero-cost states already carry Boolean structure; this file is that substrate.

In the broader forcing chain, cost uniqueness (T5, the $J$-functional) and the Recognition Composition Law sit upstream of any logical layer. PreLogicalCost is the bridge that turns a numeric cost into an emergent Boolean algebra, so later work can treat classical tautologies as minimizers rather than axioms. Without it, the claim that logic emerges from cost has no formal carrier.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (9)