Foundation Logic From Cost Contradiction Positive Cost

The cost of contradiction

A proposition in this framework is not a sentence in a book but a configuration with a positive ratio, a number measuring how present it is. Each configuration carries a cost, a price the framework forces it to pay. The central theorem contradiction_positive_cost says: for any configuration that asserts both P and its negation, either the total cost is positive, or both ratios equal 1. The second branch is the singular point, the one place where the cost function is undefined because its formula divides by zero. So the theorem's real content is that a contradiction cannot have a finite, well-defined cost; it is either too expensive to exist or it falls outside the cost function's domain.

The proof is short. A ContradictionConfig carries two ratios, one for P and one for its negation, and the framework requires their product to be 1. The cost is the sum of the defect function applied to each ratio. The defect function is zero only at ratio 1, and it grows without bound as the ratio approaches zero. If both ratios were 1, their product would be 1, which is allowed by the complementarity condition. But if P holds and not P holds, the framework's own logic, the ambient classical logic it uses to reason, derives a contradiction directly: the theorem logical_contradiction_impossible states that from hP and hnotP you get False. So the only way to have both ratios at 1 is to have already asserted a contradiction, which the ambient logic forbids. Hence the cost must be positive.

This is not a proof that logic itself emerges from cost. The framework uses classical logic in its metalanguage to prove the theorem; it does not derive classical logic from cost, which would be circular. The bootstrapping is explicit. What the theorem establishes is narrower: within a cost-minimizing structure, a configuration that asserts both P and not P cannot be stable, because stability means zero cost, and zero cost for a contradiction is forbidden. The companion theorem zero_cost_contradiction_forbidden states this directly: if the cost is zero and both P and not P hold, you get False. And consistent_zero_cost_possible shows the other side: a consistent configuration, one with ratio 1, can achieve zero cost. So the cost structure separates consistency from contradiction cleanly.

In Recognition Science, this is the bridge from cost to logic. The claim is not that logic is an illusion, but that logical consistency is what a cost-minimizing structure looks like. The machine-checked library of formal theorems proves that contradictions carry positive cost or sit at the singular point, and that consistent configurations can reach zero cost. The philosophical thesis that logic emerges from cost is a structural analogy, not a theorem. The theorem itself is a precise statement about a cost function and the configurations it prices.

/-- **THEOREM 1**: Contradictions cannot have zero total cost.

    If both P and ¬P are stable (cost 0), then both ratios must be 1.
    But complementary ratios with r * s = 1 have r = s = 1 only when
    both equal 1. And if P is true at ratio 1, ¬P cannot also be true.

    More fundamentally: the complementarity constraint r * (1/r) = 1
    means if defect(r) = 0 (so r = 1), then defect(1/r) = defect(1) = 0 too.
    But this is only possible if both assertions coexist at ratio 1,
    which is a logical contradiction. -/
theorem contradiction_positive_cost (c : ContradictionConfig) :
    contradiction_cost c > 0 ∨ (c.ratio_P = 1 ∧ c.ratio_notP = 1) := by
  by_cases h : c.ratio_P = 1
  · -- If ratio_P = 1, then ratio_notP = 1 (from complementarity)
    have hnotP : c.ratio_notP = 1 := by
      have := c.complementary
      rw [h] at this
      simp at this
      exact this
    right
    exact ⟨h, hnotP⟩
  · -- If ratio_P ≠ 1, then defect(ratio_P) > 0
    left
    unfold contradiction_cost
    -- defect(x) = 0 ↔ x = 1, so if x ≠ 1 and x > 0, defect(x) > 0
    have hdef_ne : defect c.ratio_P ≠ 0 := by
      intro heq
      have := (defect_zero_iff_one c.ratio_P_pos).mp heq
      exact h this
    have hdef_nonneg : defect c.ratio_P ≥ 0 := defect_nonneg c.ratio_P_pos
    have hdef : defect c.ratio_P > 0 := lt_of_le_of_ne hdef_nonneg (Ne.symm hdef_ne)
    linarith [defect_nonneg c.ratio_notP_pos]

/-- **THEOREM 3**: Cost-zero contradictions imply classical impossibility.

    If a contradiction config has zero total cost, then:
    - ratio_P = 1 (so P "exists")
    - ratio_notP = 1 (so ¬P "exists")
    - But P ∧ ¬P is impossible

    Therefore: zero-cost contradictions are forbidden by logic itself. -/
theorem zero_cost_contradiction_forbidden (c : ContradictionConfig)
    (_h_zero : contradiction_cost c = 0)
    (hP : c.P) (hnotP : ¬c.P) : False := by
  exact hnotP hP

/-- **THEOREM 4**: Consistent configurations can have zero cost.

    Unlike contradictions, a single proposition can stabilize at ratio = 1.
    This is the minimum-cost state for a proposition. -/
theorem consistent_zero_cost_possible :
    ∃ c : ConsistentConfig, consistent_cost c = 0 := by
  use ⟨True, 1, by norm_num⟩
  unfold consistent_cost
  exact defect_at_one

What this page does not claim

This does not claim that classical logic itself is derived from cost. This does not claim that all contradictions have infinite cost; the theorem allows the singular point as an alternative. This does not claim that the framework's cost function is defined for every possible configuration.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/LogicFromCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: