Foundation Logic As Functional Equation Excluded Middle Implies Continuous

The continuity bridge

The law of excluded middle says every proposition is either true or false, with no third option. In the Recognition Science framework, this classical principle takes a precise mathematical form: it becomes a condition on a comparison operator, a function that assigns a real-valued cost to comparing two positive quantities. The framework's declaration excluded_middle_implies_continuous proves that this condition, stated as continuity of the comparison operator on the domain of positive reals, forces the derived cost function to be continuous as well.

The derived cost is a one-variable function obtained by fixing the second argument of the comparison operator at 1. The theorem shows that if the two-variable comparison operator is continuous on the positive quadrant, then this derived cost is continuous on the positive real line. This is not a deep analytical result in itself, but it is a load-bearing step in the framework's chain: it supplies the regularity condition needed for the later uniqueness theorem that pins down the exact form of the cost function.

The framework models logic as a constraint on comparison. Its library of machine-checked theorems shows that five plain conditions on a comparison operator, including excluded middle, force the cost to equal J(x) = (x + 1/x)/2 - 1. The continuity bridge is one of the lemmas that make this forcing argument work, by guaranteeing that the derived cost is well-behaved enough for the functional equation techniques to apply.

What the declaration does not claim is just as important. It does not prove that excluded middle alone determines the cost function; other conditions are needed. It does not assert that the comparison operator itself is continuous everywhere, only on the positive reals. And it does not say anything about whether the law of excluded middle holds in ordinary logic, which is a separate question entirely.

/-- **Translation lemma 3 (Excluded middle ⇒ Continuity)**: If a comparison
operator is jointly continuous in both arguments on the positive quadrant,
then the derived cost function is continuous on (0, ∞).

The derivedCost C is the composition r ↦ (r, 1) ↦ C(r, 1). The pair-map is
continuous everywhere; the uncurried C is continuous on the positive
quadrant by ExcludedMiddle. The pair-map sends (0, ∞) into the positive
quadrant. Hence the composition is continuous on (0, ∞). -/
theorem excluded_middle_implies_continuous
    (C : ComparisonOperator)
    (hEM : ExcludedMiddle C) :
    ContinuousOn (derivedCost C) (Set.Ioi 0) := by
  -- Pair-map r ↦ (r, 1) is continuous everywhere.
  have h_pair_cont : Continuous (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ)) :=
    continuous_id.prodMk continuous_const
  have h_pair_on : ContinuousOn (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
      (Set.Ioi (0 : ℝ)) :=
    h_pair_cont.continuousOn
  -- Pair-map sends (0,∞) into the positive quadrant.
  have h_maps : Set.MapsTo (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
      (Set.Ioi (0 : ℝ)) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ)) := by
    intro s hs
    refine ⟨?_, ?_⟩
    · exact hs
    · show (0 : ℝ) < 1
      exact one_pos
  -- Compose to get continuity of (uncurry C) ∘ pair on (0,∞).
  have h_comp : ContinuousOn
      ((Function.uncurry C) ∘ fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
      (Set.Ioi (0 : ℝ)) :=
    hEM.comp h_pair_on h_maps
  -- The composition equals derivedCost C definitionally.
  have h_eq : ((Function.uncurry C) ∘ fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
              = derivedCost C := by
    funext s
    rfl
  rw [h_eq] at h_comp
  exact h_comp

/-- Public short name for the continuous positive-ratio Law of Logic.

The longer historical name `SatisfiesLawsOfLogic` remains the underlying
structure used by existing proofs.  This alias is the theorem-facing formula:
a comparison operator satisfies the Law of Logic exactly when it satisfies
identity, non-contradiction, excluded middle/continuity, scale invariance,
route independence, and non-triviality. -/
abbrev LawOfLogic (C : ComparisonOperator) : Prop :=
  SatisfiesLawsOfLogic C

/-- **Law of Logic forces the canonical cost**:
under the canonical RCL normalization and unit log-curvature calibration, the
unique continuous positive-ratio cost satisfying the Law of Logic is
`J(x) = ½(x + x⁻¹) - 1`. -/
theorem law_of_logic_forces_canonical_cost
    (C : ComparisonOperator) (hLogic : LawOfLogic C)
    [Cost.FunctionalEquation.AczelSmoothnessPackage]
    (hRCL : Cost.FunctionalEquation.SatisfiesCompositionLaw (derivedCost C))
    (hCalib : Cost.FunctionalEquation.IsCalibrated (derivedCost C)) :
    ∀ x : ℝ, 0 < x → derivedCost C x = Cost.Jcost x := by
  exact J_is_unique_cost_under_logic C hLogic hRCL hCalib

What this page does not claim

Excluded middle alone does not determine the cost function; other conditions are required. The comparison operator is continuous only on positive reals, not on the whole real line. The declaration says nothing about whether the law of excluded middle holds in ordinary logic.

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/LogicAsFunctionalEquation.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: