zero_cost_contradiction_forbidden
plain-language theorem explainer
A contradiction configuration cannot achieve zero total cost without forcing a classical falsehood. Researchers deriving logic from cost minimization in Recognition Science would cite this to show that P and not-P cannot both stabilize. The proof is a direct one-line application of negation elimination on the asserted pair.
Claim. Let $c$ be a contradiction configuration with $P$ a proposition. If the total cost (sum of defects on the two ratios) equals zero and both $P$ and $¬P$ hold, then falsehood follows.
background
The module establishes that logical consistency emerges as the minimum-cost structure within Recognition Science. A ContradictionConfig is the structure carrying a proposition $P$ together with positive ratios for both $P$ and $¬P$, intended to model simultaneous stability of a claim and its negation. The function contradiction_cost sums the defects of those two ratios, so zero cost would require both ratios to equal 1. Upstream results include the consistent predicate from SAT backpropagation and the cost definitions from MultiplicativeRecognizerL4 and ObserverForcing, which supply the non-negative defect functions used here.
proof idea
The proof is a one-line wrapper that applies classical negation elimination: the hypothesis ¬c.P is applied directly to c.P to obtain False.
why it matters
This is Theorem 3 of the LogicFromCost module and completes the local argument that contradictions cannot sit at the cost minimum. It feeds the subsequent claim that consistent configurations achieve zero cost and supports the broader thesis that logic is the structure of cheap configurations rather than an external imposition. The result stays inside the classical metalanguage while showing that cost minimization forbids contradictory object-level assertions, consistent with the eight-tick octave and J-cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.