IndisputableMonolith.Foundation.LogicAsFunctionalEquationLogic

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation
   3import IndisputableMonolith.Cost.JcostLogic
   4
   5/-!
   6  LogicAsFunctionalEquationLogic.lean
   7
   8  Law-of-Logic comparison operators on recovered reals.
   9
  10  This is the recovered-real mirror of
  11  `Foundation.LogicAsFunctionalEquation`.  The analytic regularity fields
  12  (continuity and the polynomial-combiner theorem surface) are transported
  13  through `LogicReal.toReal`; the local structural fields (identity,
  14  symmetry, scale invariance, non-triviality) are stated directly over
  15  `LogicReal`.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace LogicAsFunctionalEquationLogic
  21
  22open RealsFromLogic RealsFromLogic.LogicReal
  23open LogicAsFunctionalEquation
  24open Cost.JcostLogic
  25
  26noncomputable section
  27
  28/-! ## Recovered-real comparison operators -/
  29
  30/-- A comparison operator over recovered reals. -/
  31abbrev ComparisonOperatorL := LogicReal → LogicReal → LogicReal
  32
  33/-- Derived one-argument cost over recovered reals. -/
  34@[simp] def derivedCostL (C : ComparisonOperatorL) : LogicReal → LogicReal :=
  35  fun r => C r (fromReal 1)
  36
  37/-- Transport a recovered-real comparison operator to the existing real
  38comparison-operator surface. -/
  39def transportComparison (C : ComparisonOperatorL) :
  40    LogicAsFunctionalEquation.ComparisonOperator :=
  41  fun x y => toReal (C (fromReal x) (fromReal y))
  42
  43/-- Identity over recovered reals. -/
  44def IdentityL (C : ComparisonOperatorL) : Prop :=
  45  ∀ x : LogicReal, (0 : LogicReal) < x → C x x = fromReal 0
  46
  47/-- Non-contradiction / reciprocal symmetry over recovered reals. -/
  48def NonContradictionL (C : ComparisonOperatorL) : Prop :=
  49  ∀ x y : LogicReal, (0 : LogicReal) < x → (0 : LogicReal) < y → C x y = C y x
  50
  51/-- Scale invariance over recovered reals. -/
  52def ScaleInvariantL (C : ComparisonOperatorL) : Prop :=
  53  ∀ x y lam : LogicReal, (0 : LogicReal) < x → (0 : LogicReal) < y → (0 : LogicReal) < lam →
  54    C (lam * x) (lam * y) = C x y
  55
  56/-- Non-triviality over recovered reals. -/
  57def NonTrivialL (C : ComparisonOperatorL) : Prop :=
  58  ∃ x : LogicReal, (0 : LogicReal) < x ∧ derivedCostL C x ≠ fromReal 0
  59
  60/-- Recovered-real Law of Logic. The structural fields are native to
  61`LogicReal`; the analytic/polynomial regularity surface is explicitly
  62transported to the already-verified real theorem. -/
  63structure SatisfiesLawsOfLogicL (C : ComparisonOperatorL) : Prop where
  64  identity : IdentityL C
  65  non_contradiction : NonContradictionL C
  66  scale_invariant : ScaleInvariantL C
  67  non_trivial : NonTrivialL C
  68  transported_real_laws :
  69    LogicAsFunctionalEquation.SatisfiesLawsOfLogic (transportComparison C)
  70
  71/-! ## Structural transport lemmas -/
  72
  73theorem identityL_to_real (C : ComparisonOperatorL) (h : IdentityL C) :
  74    LogicAsFunctionalEquation.Identity (transportComparison C) := by
  75  intro x hx
  76  unfold transportComparison
  77  have hxL : (0 : LogicReal) < fromReal x := by
  78    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]
  79    exact hx
  80  have hL := congrArg toReal (h (fromReal x) hxL)
  81  simpa [toReal_fromReal] using hL
  82
  83theorem nonContradictionL_to_real (C : ComparisonOperatorL) (h : NonContradictionL C) :
  84    LogicAsFunctionalEquation.NonContradiction (transportComparison C) := by
  85  intro x y hx hy
  86  unfold transportComparison
  87  have hxL : (0 : LogicReal) < fromReal x := by
  88    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hx
  89  have hyL : (0 : LogicReal) < fromReal y := by
  90    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hy
  91  exact congrArg toReal (h (fromReal x) (fromReal y) hxL hyL)
  92
  93theorem scaleInvariantL_to_real (C : ComparisonOperatorL) (h : ScaleInvariantL C) :
  94    LogicAsFunctionalEquation.ScaleInvariant (transportComparison C) := by
  95  intro x y lam hx hy hlam
  96  unfold transportComparison
  97  have hxL : (0 : LogicReal) < fromReal x := by
  98    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hx
  99  have hyL : (0 : LogicReal) < fromReal y := by
 100    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hy
 101  have hlamL : (0 : LogicReal) < fromReal lam := by
 102    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hlam
 103  have hmulx : fromReal lam * fromReal x = fromReal (lam * x) := by
 104    rw [eq_iff_toReal_eq]; simp [toReal_fromReal]
 105  have hmuly : fromReal lam * fromReal y = fromReal (lam * y) := by
 106    rw [eq_iff_toReal_eq]; simp [toReal_fromReal]
 107  have hL := h (fromReal x) (fromReal y) (fromReal lam) hxL hyL hlamL
 108  rw [hmulx, hmuly] at hL
 109  exact congrArg toReal hL
 110
 111theorem nonTrivialL_to_real (C : ComparisonOperatorL) (h : NonTrivialL C) :
 112    LogicAsFunctionalEquation.NonTrivial (transportComparison C) := by
 113  rcases h with ⟨x, hx, hxne⟩
 114  refine ⟨toReal x, ?_, ?_⟩
 115  · simpa [lt_iff_toReal_lt] using hx
 116  · intro hzero
 117    apply hxne
 118    rw [eq_iff_toReal_eq]
 119    have hzero' : toReal (C (fromReal (toReal x)) (fromReal 1)) = 0 := by
 120      simpa [transportComparison, LogicAsFunctionalEquation.derivedCost, toReal_fromReal]
 121        using hzero
 122    rw [fromReal_toReal] at hzero'
 123    simpa [derivedCostL, toReal_fromReal] using hzero'
 124
 125/-- The recovered-real Law of Logic transports to the existing real theorem
 126surface. -/
 127theorem lawsL_to_real {C : ComparisonOperatorL} (h : SatisfiesLawsOfLogicL C) :
 128    LogicAsFunctionalEquation.SatisfiesLawsOfLogic (transportComparison C) :=
 129  h.transported_real_laws
 130
 131/-- RCL is forced for recovered-real logic, by transport through the existing
 132real theorem. -/
 133theorem RCL_is_unique_functional_form_of_logicL
 134    (C : ComparisonOperatorL) (h : SatisfiesLawsOfLogicL C) :
 135    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
 136      DAlembert.Inevitability.HasMultiplicativeConsistency
 137        (LogicAsFunctionalEquation.derivedCost (transportComparison C)) P ∧
 138      (∀ u v, P u v = 2*u + 2*v + c*u*v) :=
 139  LogicAsFunctionalEquation.RCL_is_unique_functional_form_of_logic
 140    (transportComparison C) (lawsL_to_real h)
 141
 142end
 143
 144end LogicAsFunctionalEquationLogic
 145end Foundation
 146end IndisputableMonolith
 147