IsUnstable
plain-language theorem explainer
A propositional configuration is unstable precisely when the defect of its ratio exceeds zero. Researchers deriving logic from cost minimization in Recognition Science would cite this to separate stable minima from positive-cost states. The declaration is a direct one-line abbreviation of the inequality between prop_cost and zero.
Claim. A configuration $c$ consisting of a proposition paired with a positive real ratio $r$ is unstable when the defect of $r$ is strictly positive.
background
The module shows that logical consistency is the minimum-cost configuration in a recognition setting. A PropConfig pairs any proposition with a positive real ratio that encodes its balance: ratio exactly 1 for stable truth, ratio near 0 for absence, and ratio diverging to infinity for instability. The cost of such a configuration is defined as the defect of its ratio, inheriting the non-negative J-cost structure from upstream recognition events. Upstream results supply the active edge count A and the cost maps from multiplicative recognizers and observer forcing, both of which evaluate to non-negative reals on positive ratios.
proof idea
This is a direct one-line definition that equates instability to the predicate prop_cost c > 0.
why it matters
The definition supplies the positive-cost side of the stability dichotomy used to show that contradictions cannot both stabilize. It therefore supports the module's core claim that consistency is the global minimum of J-cost and that logic emerges as the structure of cheap configurations. It sits immediately before the contradiction-cost lemmas in the same file and aligns with the Recognition Science thesis that cost minimization precedes logical structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.