IndisputableMonolith.Foundation.PolynomialityFromLogic

   1/-
   2  PolynomialityFromLogic.lean
   3
   4  Level 3 of three for the Law-of-Logic precursor paper.
   5
   6  Intended canonical location:
   7    reality/IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
   8
   9  Status:
  10    Precise Lean statement of the conjecture and its formal reduction to a
  11    single clean technical question.  Provable parts fully proved.  The
  12    irreducible remaining step is identified, named, and reduced to its
  13    minimal Lean-statable content.
  14
  15  Goal:
  16    Eliminate even the regularity hypothesis of Level 2
  17    (`GeneralizedAczelSmoothnessPackage`) and derive the bilinear family of
  18    combiners from the four Aristotelian laws and a structural
  19    closure-under-iteration condition that is itself a consequence of the
  20    laws of logic at the comparison-of-comparisons level.
  21
  22  Approach:
  23    1. Make precise what closure-under-iteration of comparisons means as a
  24       Lean predicate on the combiner.
  25    2. Show that closure-under-iteration plus continuity forces a strong
  26       regularity property on Φ along a one-parameter family of inputs.
  27    3. State the residual smoothness conjecture as a Lean axiom-class with
  28       the cleanest possible interface, ready for either formalization or
  29       counter-investigation.
  30
  31  References:
  32    - Aczél, Lectures on Functional Equations and Their Applications, 1966.
  33    - Kannappan, Functional Equations and Inequalities with Applications,
  34      Springer 2009.
  35    - Stetkær, Functional Equations on Groups, World Scientific 2013.
  36    - This module's companion paper:
  37      "The Law of Logic as Functional Equation."
  38-/
  39
  40import Mathlib
  41import IndisputableMonolith.Foundation.DAlembert.Inevitability
  42import IndisputableMonolith.Cost.AczelTheorem
  43
  44namespace IndisputableMonolith
  45namespace Foundation
  46namespace PolynomialityFromLogic
  47
  48open Real
  49open IndisputableMonolith.Foundation.DAlembert.Inevitability
  50
  51/-! ## Closure Under Iteration
  52
  53The Aristotelian content of "comparisons of comparisons compose
  54consistently" formalizes as: any finite iterate of the combining rule on
  55elements of `Range(F)` again lies in `Range(F)`, and the iteration is
  56continuous in its inputs.
  57
  58The key structural fact: if Φ is closed under iteration on `Range(F)`,
  59then `Range(F)` is invariant under the dynamical system `(u, v) ↦ Φ(u, v)`,
  60and the orbit structure of this system is the structural content of
  61"composition of comparisons composes."
  62-/
  63
  64/-- A combining rule Φ is **closed under iteration** on a set `S ⊆ ℝ` if
  65applying Φ to two elements of S produces an element of S, and the result is
  66continuous in both inputs. -/
  67def ClosedUnderIteration (Phi : ℝ → ℝ → ℝ) (S : Set ℝ) : Prop :=
  68  ContinuousOn (Function.uncurry Phi) (S ×ˢ S) ∧
  69  ∀ u v : ℝ, u ∈ S → v ∈ S → Phi u v ∈ S
  70
  71/-- The structural closure property derived from the four Aristotelian
  72laws plus the route-independence equation: the combining rule on
  73`Range(F)` is closed under iteration in this technical sense. -/
  74def IteratedClosureOnRange (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ) : Prop :=
  75  ClosedUnderIteration Phi (Set.image F (Set.Ioi 0))
  76
  77/-! ## Provable Consequences
  78
  79The next two lemmas extract regularity properties from closure-under-iteration
  80that are used in the conjecture's proof.  Both are fully proved here.
  81-/
  82
  83/-- **The diagonal of Φ on Range(F) is continuous.**  Pure consequence of
  84joint continuity of Φ on Range(F)². -/
  85theorem diagonal_continuous_on_range
  86    (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
  87    (hClosed : IteratedClosureOnRange F Phi) :
  88    ContinuousOn (fun v : ℝ => Phi v v) (Set.image F (Set.Ioi 0)) := by
  89  obtain ⟨hCont, _⟩ := hClosed
  90  -- The diagonal map v ↦ (v, v) is continuous everywhere; compose with Phi.
  91  have h_diag_on : ContinuousOn (fun w : ℝ => ((w, w) : ℝ × ℝ))
  92      (Set.image F (Set.Ioi 0)) :=
  93    (continuous_id.prodMk continuous_id).continuousOn
  94  have h_maps : Set.MapsTo (fun w : ℝ => ((w, w) : ℝ × ℝ))
  95      (Set.image F (Set.Ioi 0))
  96      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
  97    intro w hw
  98    exact ⟨hw, hw⟩
  99  -- Use ContinuousOn.comp on the explicit lambda form of uncurry.
 100  have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
 101      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont
 102  have h_comp : ContinuousOn
 103      ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
 104      (Set.image F (Set.Ioi 0)) :=
 105    h_phi_on.comp h_diag_on h_maps
 106  -- Convert the composition into the simpler form.
 107  have h_eq : ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
 108              = (fun v : ℝ => Phi v v) := by
 109    funext w
 110    rfl
 111  rw [h_eq] at h_comp
 112  exact h_comp
 113
 114/-- **Iteration produces continuous orbits.**  If we iterate Φ on a starting
 115element v ∈ Range(F), the n-fold iterate is again in Range(F), and the map
 116v ↦ Φ^[n](v, v) is continuous on Range(F). -/
 117theorem iterate_continuous_on_range
 118    (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
 119    (hClosed : IteratedClosureOnRange F Phi)
 120    (n : ℕ) :
 121    ∃ φₙ : ℝ → ℝ,
 122      ContinuousOn φₙ (Set.image F (Set.Ioi 0)) ∧
 123      (∀ v ∈ Set.image F (Set.Ioi 0), φₙ v ∈ Set.image F (Set.Ioi 0)) := by
 124  -- Define the iterate by recursion on n.  Inductively, each iterate is
 125  -- a continuous map from Range(F) into Range(F).
 126  induction n with
 127  | zero =>
 128    refine ⟨id, ?_, ?_⟩
 129    · exact continuousOn_id
 130    · intro v hv
 131      exact hv
 132  | succ k ih =>
 133    obtain ⟨φₖ, hCont_φₖ, hMap_φₖ⟩ := ih
 134    refine ⟨fun v => Phi (φₖ v) v, ?_, ?_⟩
 135    · -- Continuity of v ↦ Phi(φₖ v, v) via ContinuousOn.comp.
 136      obtain ⟨hCont_Phi, _⟩ := hClosed
 137      have h_pair_on : ContinuousOn (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ))
 138          (Set.image F (Set.Ioi 0)) :=
 139        hCont_φₖ.prodMk continuousOn_id
 140      have h_maps : Set.MapsTo (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ))
 141          (Set.image F (Set.Ioi 0))
 142          ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
 143        intro w hw
 144        exact ⟨hMap_φₖ w hw, hw⟩
 145      have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
 146          ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont_Phi
 147      have h_comp : ContinuousOn
 148          ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘
 149            (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ)))
 150          (Set.image F (Set.Ioi 0)) :=
 151        h_phi_on.comp h_pair_on h_maps
 152      have h_eq : ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘
 153                    (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ)))
 154                  = (fun v : ℝ => Phi (φₖ v) v) := by
 155        funext w
 156        rfl
 157      rw [h_eq] at h_comp
 158      exact h_comp
 159    · intro v hv
 160      obtain ⟨_, hClosure⟩ := hClosed
 161      exact hClosure (φₖ v) v (hMap_φₖ v hv) hv
 162
 163/-! ## Corrected Status Statement
 164
 165The earlier version of this module carried a class assumption
 166`IteratedAnalyticityHolds`, claiming that closure under iteration on
 167`Range(F)` forces real-analyticity of the combiner.  The quartic-log
 168counterexample in
 169`IndisputableMonolith.Foundation.LogicAsFunctionalEquation.QuarticLogCounterexample`
 170shows that this is false in general: its combiner
 171`Φ(a,b) = 2a + 2b + 12 sqrt(a*b)` is closed on `[0,∞)` but is not
 172real-analytic at the origin.
 173
 174This module therefore keeps only the structural consequences of closure under
 175iteration that are actually proved:
 176
 177* diagonal continuity on the range;
 178* continuous iterates on the range.
 179
 180The corrected polynomiality problem is moved to the planned
 181`LogicAsFunctionalEquation.Polynomiality` module: assume real-analyticity at
 182the origin directly, then prove polynomial degree at most two.
 183-/
 184
 185end PolynomialityFromLogic
 186end Foundation
 187end IndisputableMonolith
 188