IsStable
A propositional configuration is stable exactly when its cost is zero. Researchers tracing how logical consistency emerges from J-cost minimization in Recognition Science cite this when linking zero-defect states to stable propositions. The declaration is a direct one-line abbreviation of the zero-cost condition via the prop_cost function.
claimA propositional configuration $c$ is stable precisely when its cost equals zero, where the cost is defined as the defect of the ratio component of $c$.
background
PropConfig is the structure pairing a proposition with a positive real ratio that encodes its presence: ratio = 1 for balanced stable truth, ratio near 0 for absence, and ratio to infinity for instability. prop_cost is the noncomputable map sending such a configuration to the defect of its ratio, inheriting the J-cost semantics from upstream recognizer and observer modules. The module establishes that logical consistency is the cost-minimizing structure within Lean's classical metalanguage, with contradictions assigned infinite effective cost.
proof idea
One-line definition that equates IsStable c to the atomic proposition prop_cost c = 0, where prop_cost unfolds directly to defect of the ratio.
why it matters in Recognition Science
This supplies the stability predicate consumed by DiscretenessForcing.IsStable and PreLogicalCost.IsStable (and its stable_iff_boundary theorem) to close the cost-to-logic bridge. It realizes the module claim that consistency is the minimum-cost configuration, aligning with the Recognition Science forcing chain where J-minima produce the eight-tick octave and D = 3 geometry.
scope and limits
- Does not derive classical logic itself from cost; operates inside Lean's ambient classical logic.
- Does not compute explicit numerical values for prop_cost beyond the defect function.
- Does not treat interactions among multiple propositions or higher-order configurations.
formal statement (Lean)
82def IsStable (c : PropConfig) : Prop := prop_cost c = 0
proof body
Definition body.
83
84/-- A configuration is unstable if its cost is positive. -/