pith. sign in
module module high

IndisputableMonolith.Foundation.PreLogicalCost

show as:
view Lean formalization →

The PreLogicalCost module defines pre-logical configuration values as real numbers constrained to the closed unit interval. It supplies the basic objects and operations that enable the later derivation of logical consistency from cost minimization. Researchers tracing the emergence of Boolean structure from physical costs cite this setup. The module contains only definitions with no proofs or theorems.

claimPre-logical costs are real numbers $c$ satisfying $0leq cleq 1$, with associated stable states and Boolean-like operations on configurations.

background

This module introduces the pre-logical layer of the Recognition Science foundation. It defines PreState as the set of pre-logical configurations, preCost as the cost function restricted to the unit interval, IsStable as the predicate for stable states, and the operations band, bor, bnot together with the theorem stable_forms_boolean_algebra. These objects prepare the ground for cost-based logic without yet invoking the J-cost or phi-ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the pre-logical cost objects required by the downstream LogicFromCost module, which proves that logical consistency is a cost-minimizing state. It occupies the initial position in the chain that later reaches the Recognition Composition Law and the eight-tick octave. The parent result asserts that configurations assigned positive cost cannot be simultaneously asserted.

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)