Foundation Logic As Functional Equation Logic Laws L To Real

The bridge to real numbers

The declaration lawsL_to_real in the Recognition Science library is a bridge. It states that if a comparison operation satisfies four structural laws in a special number system called LogicReal, then the same operation, translated to ordinary real numbers, satisfies the corresponding laws there. The four laws are identity (comparing a number with itself gives zero), non-contradiction (the order of comparison does not matter), scale invariance (scaling both inputs leaves the result unchanged), and non-triviality (the operation is not constantly zero). The theorem is a formal statement in a machine-checked library of formal theorems, meaning its proof has been verified step by step.

The significance is that it connects two levels of the framework. The special number system LogicReal is where the framework's structural laws are stated natively. The real numbers are where the framework's analytic results, such as continuity and the polynomial-combiner theorem, already live. The theorem lawsL_to_real transports the structural laws across this bridge. It shows that the four laws over LogicReal imply the corresponding laws over the reals, so that the full set of laws, structural and analytic, holds on the real-number surface. This is what the docstring calls the recovered-real Law of Logic.

The theorem does not itself prove the uniqueness of the cost function. That work is done by a separate theorem, RCL_is_unique_functional_form_of_logicL, which builds on lawsL_to_real and the already-verified real theorem. The bridge theorem is a necessary step, not the destination. It also does not claim that the four structural laws are the only laws of logic, nor that they are sufficient by themselves. The analytic regularity conditions, continuity and the polynomial-combiner surface, are transported separately and are required for the uniqueness result.

In plain terms, the declaration says: if you have a comparison operation that behaves well in the special number system, then it behaves well in the ordinary real numbers too. The framework's library proves this formally. What it does not claim is that the special number system itself is the real numbers, or that the four laws exhaust the properties of logic. Those are separate questions, and the theorem is silent on them.

/-- The recovered-real Law of Logic transports to the existing real theorem
surface. -/
theorem lawsL_to_real {C : ComparisonOperatorL} (h : SatisfiesLawsOfLogicL C) :
    LogicAsFunctionalEquation.SatisfiesLawsOfLogic (transportComparison C) :=
  h.transported_real_laws

/-- Identity over recovered reals. -/
def IdentityL (C : ComparisonOperatorL) : Prop :=
  ∀ x : LogicReal, (0 : LogicReal) < x → C x x = fromReal 0

/-- Non-contradiction / reciprocal symmetry over recovered reals. -/
def NonContradictionL (C : ComparisonOperatorL) : Prop :=
  ∀ x y : LogicReal, (0 : LogicReal) < x → (0 : LogicReal) < y → C x y = C y x

/-- Scale invariance over recovered reals. -/
def ScaleInvariantL (C : ComparisonOperatorL) : Prop :=
  ∀ x y lam : LogicReal, (0 : LogicReal) < x → (0 : LogicReal) < y → (0 : LogicReal) < lam →
    C (lam * x) (lam * y) = C x y

/-- Non-triviality over recovered reals. -/
def NonTrivialL (C : ComparisonOperatorL) : Prop :=
  ∃ x : LogicReal, (0 : LogicReal) < x ∧ derivedCostL C x ≠ fromReal 0

/-- The recovered-real Law of Logic transports to the existing real theorem
surface. -/
theorem lawsL_to_real {C : ComparisonOperatorL} (h : SatisfiesLawsOfLogicL C) :
    LogicAsFunctionalEquation.SatisfiesLawsOfLogic (transportComparison C) :=
  h.transported_real_laws

/-- RCL is forced for recovered-real logic, by transport through the existing
real theorem. -/
theorem RCL_is_unique_functional_form_of_logicL
    (C : ComparisonOperatorL) (h : SatisfiesLawsOfLogicL C) :
    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
      DAlembert.Inevitability.HasMultiplicativeConsistency
        (LogicAsFunctionalEquation.derivedCost (transportComparison C)) P ∧
      (∀ u v, P u v = 2*u + 2*v + c*u*v) :=
  LogicAsFunctionalEquation.RCL_is_unique_functional_form_of_logic
    (transportComparison C) (lawsL_to_real h)

What this page does not claim

The theorem does not prove the uniqueness of the cost function by itself. The theorem does not claim that the four structural laws are the only laws of logic. The theorem does not identify LogicReal with the real numbers.

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