contradiction_cost
plain-language theorem explainer
The declaration defines the total cost of a contradiction configuration as the sum of defect values on the ratios for a proposition and its negation. Researchers deriving logic from cost minimization in Recognition Science cite it to quantify instability of inconsistent states. The definition is a direct sum that applies the upstream defect functional to the two ratios supplied by ContradictionConfig.
Claim. For a contradiction configuration $c$ with proposition $P$, ratio $r_P > 0$ for $P$, and complementary ratio $r_{¬P} > 0$ for $¬P$, the total cost equals defect$(r_P)$ + defect$(r_{¬P})$, where defect$(x) = J(x)$ is the recognition cost functional.
background
The module establishes that logical consistency emerges as the structure of cost-minimizing configurations within Lean's classical metalanguage. A proposition is true when its configuration stabilizes (defect approaches zero) and false when it diverges. ContradictionConfig is the structure that simultaneously asserts both $P$ and $¬P$ with complementary positive ratios, which the module treats as the object-level signature of inconsistency.
proof idea
This is a one-line definition that sums the defect values on the two ratios supplied by the ContradictionConfig structure. It directly invokes the defect definition from LawOfExistence, which equals the J-cost functional on positive reals.
why it matters
The definition supplies the cost measure used by contradiction_positive_cost to show contradictions cannot achieve zero cost and by logic_from_cost to conclude that stable configurations are precisely the logically consistent ones. It occupies the step in the Recognition Science chain where J-cost minima enforce non-contradiction, consistent with the Recognition Composition Law and the emergence of logic from cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.