IsLogicalContradiction
plain-language theorem explainer
IsLogicalContradiction flags a ContradictionConfig as contradictory exactly when both ratio_P and ratio_notP equal 1. Researchers deriving logical consistency from J-cost minimization cite this predicate to isolate states that cannot stabilize. The definition is the direct conjunction of those two ratio equalities on the input record.
Claim. A contradiction configuration $c$ is logically contradictory when the ratio asserted for proposition $P$ equals 1 and the ratio asserted for its negation also equals 1.
background
The LogicFromCost module shows that logical consistency arises as the structure of minimum-cost configurations inside classical logic. A ContradictionConfig is the record holding a proposition $P$, positive real ratios for $P$ and for its negation, and the positivity proofs. Imported cost functions from MultiplicativeRecognizerL4 and ObserverForcing map recognition events to non-negative J-costs, with zero cost marking stabilization at ratio 1.
proof idea
Direct definition returning the conjunction of the two ratio equalities supplied by the ContradictionConfig record. No lemmas or tactics are invoked; the body simply packages the condition for downstream use.
why it matters
This predicate supplies the object-language marker used in the parent theorem logic_from_cost, which asserts that consistent configurations reach zero cost while contradictions cannot. It supports the module claim that logic emerges from J-cost minimization rather than being presupposed, and is referenced in logic_from_cost_summary and mp_from_cost_and_logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.