contradiction_positive_cost
plain-language theorem explainer
Contradiction configurations cannot achieve zero total cost in the Recognition Science model. A researcher deriving logic from cost minimization would cite this result to show that asserting both a proposition and its negation forces positive defect sum. The proof splits on whether the ratio for the proposition equals one; the equal-one case forces the complementary ratio to one via the structure definition, while the unequal case invokes defect non-negativity and the zero-defect characterization to obtain strict positivity.
Claim. Let $c$ be a contradiction configuration with positive ratios $r$ for $P$ and $s$ for its negation. Then $J(r) + J(s) > 0$, or else $r = s = 1$, where $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$.
background
A ContradictionConfig is a structure pairing a proposition $P$ with positive real ratios for $P$ and for its negation, together with positivity proofs. The associated cost is the sum of the two defects, each given by the functional $J$. The module works inside Lean's classical metalanguage to establish that cost-minimizing configurations behave like logically consistent ones: contradictions are unstable because they cannot both stabilize at zero defect.
proof idea
The proof performs case analysis on whether the ratio for $P$ equals one. When equality holds, the complementary constraint inside the structure forces the negation ratio to one, yielding the right disjunct. When the ratio differs from one, defect_zero_iff_one supplies that the defect cannot vanish; combined with defect_nonneg this yields strict positivity for the first term, and linarith closes the left disjunct after adding the non-negative second defect.
why it matters
This result supplies the non-zero cost property for contradictions that feeds directly into logic_from_cost, the main theorem establishing that logic is the structure of cost-minimizing states. It also appears in logic_from_cost_summary and mp_from_cost_and_logic. Within the Recognition framework it closes the step showing contradictions carry positive cost, thereby establishing consistency as the zero-cost minimum and aligning with the emergence of logic from the $J$-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.