IsLogicalContradiction
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive classical logic from cost; classical logic is used in the metalanguage.
- Does not compute an explicit numerical cost value for the configuration.
- Does not apply outside the Recognition Science J-cost framework.
- Does not claim that contradictory ratios are physically realizable.
formal statement (Lean)
152def IsLogicalContradiction (c : ContradictionConfig) : Prop :=
proof body
Definition body.
153 c.ratio_P = 1 ∧ c.ratio_notP = 1
154
155/-- **THEOREM 2**: Logical contradictions are classically impossible.
156
157 If both P and ¬P are true (ratio = 1, cost = 0), then P ∧ ¬P holds.
158 But P ∧ ¬P = False.
159
160 This shows: the cost framework respects classical logic.
161 Contradictions can't stabilize because they can't exist. -/