pith. machine review for the scientific record. sign in
def definition def or abbrev high

consistent_cost

show as:
view Lean formalization →

consistent_cost assigns to each ConsistentConfig the defect of its ratio. Researchers deriving logic from cost minimization in Recognition Science cite this when establishing that stable propositions reach zero cost. It is a direct one-line wrapper around the upstream defect function.

claimFor a consistent configuration $c$ with proposition $P$ and positive ratio $r$, the cost is $defect(r)$, where $defect(x) := J(x)$ and $J$ is the recognition cost functional.

background

ConsistentConfig is a structure pairing a proposition $P$ with a positive real ratio $r$, representing a configuration without its negation asserted. The defect function, imported from LawOfExistence, is defined as $defect(x) := J(x)$ for positive $x$, measuring deviation from unity. The module establishes that logical consistency emerges as the minimum-cost state in the Recognition Science framework, where cost minimization selects stable configurations. Upstream, defect_at_one shows $defect(1) = 0$, and defect_nonneg establishes non-negativity for positive arguments.

proof idea

This is a one-line wrapper that applies the defect function to the ratio field of the ConsistentConfig structure.

why it matters in Recognition Science

This definition supplies the cost measure used in consistent_minimum_cost, logic_from_cost, and why_logic_is_real, which establish that consistency achieves zero cost while contradictions do not. It fills the role of assigning costs in the cost-minimization derivation of logic, aligning with the framework claim that logic emerges from minimizing J-cost. It supports T5 J-uniqueness by providing the cost for consistent states.

scope and limits

formal statement (Lean)

 191noncomputable def consistent_cost (c : ConsistentConfig) : ℝ := defect c.ratio

proof body

Definition body.

 192
 193/-- **THEOREM 4**: Consistent configurations can have zero cost.
 194
 195    Unlike contradictions, a single proposition can stabilize at ratio = 1.
 196    This is the minimum-cost state for a proposition. -/

used by (5)

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

depends on (9)

Lean names referenced from this declaration's body.