logical_contradiction_impossible
plain-language theorem explainer
The theorem shows that a ContradictionConfig cannot have both its proposition P and the negation of P hold at once, as this immediately produces falsehood. Researchers building cost-based accounts of logical consistency cite it to confirm that the framework inherits classical negation rules without extra axioms. The proof is a direct one-step application of the negation hypothesis to the asserted proposition.
Claim. Let $c$ be a contradiction configuration. If the proposition $P$ asserted by $c$ holds and its negation also holds, then falsehood follows.
background
A ContradictionConfig is the structure that simultaneously asserts a proposition $P$ together with its negation, each equipped with a positive ratio. The module works inside Lean's classical metalanguage to show that cost-minimizing configurations cannot occupy both sides of a negation. The core claim is that any configuration assigned positive cost cannot be simultaneously asserted and negated; contradictions therefore cannot stabilize.
proof idea
The term proof applies the hypothesis that the negation holds directly to the hypothesis that the proposition holds, discharging the goal in one step.
why it matters
It supplies the classical-impossibility step that lets the module conclude consistency is the minimum-cost structure. The surrounding argument (quoted in the module) states that contradictions have infinite effective cost while consistency is the cost-minimizing state, thereby linking the cost landscape to logical rules without circularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.