Encyclopedia Foundation Foundation Polynomiality From Logic

ARTICLE 3 claims 3 theorems

Foundation Polynomiality From Logic

A failed attempt to force polynomial equations from pure logic left behind two proved structural facts about how comparisons compose.

Verify this page

Polynomiality from logic

Polynomiality from logic is the question of whether the basic rules of comparison force the combining operation to be a simple polynomial. In the framework's terms, a ledger (a discrete record of events) tracks comparisons between magnitudes. The combining rule takes two comparisons and produces a third. The question is whether the logical laws governing these comparisons, such as the requirement that different routes to the same result agree, force this rule to be a polynomial of degree at most two.

The module IndisputableMonolith.Foundation.PolynomialityFromLogic does not settle that question. Its earlier version assumed that closure under iteration, meaning repeatedly applying the combining rule to its own outputs stays within the same set, would force the rule to be analytic. A counterexample in the library, using the rule Φ(a,b) = 2a + 2b + 12√(ab), is closed on the nonnegative reals but is not analytic at the origin. That counterexample refutes the assumption.

What the module does prove are two structural consequences of closure under iteration. First, the diagonal of the combining rule, meaning the map v ↦ Φ(v,v), is continuous on the range of the comparison function. Second, any finite iterate of the rule on a starting value remains in the range, and the map from the starting value to that iterate is continuous. These are the theorems diagonal_continuous_on_range and iterate_continuous_on_range.

The corrected problem, proving that real-analyticity at the origin forces polynomial degree at most two, is moved to a planned module. The two proved facts remain as the structural content of what "comparisons of comparisons compose consistently" means in this framework.

THEOREM diagonal_continuous_on_range · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
diagonal_continuous_on_range · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean:83 
/-- **The diagonal of Φ on Range(F) is continuous.**  Pure consequence of
joint continuity of Φ on Range(F)². -/
theorem diagonal_continuous_on_range
    (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
    (hClosed : IteratedClosureOnRange F Phi) :
    ContinuousOn (fun v : ℝ => Phi v v) (Set.image F (Set.Ioi 0)) := by
  obtain ⟨hCont, _⟩ := hClosed
  -- The diagonal map v ↦ (v, v) is continuous everywhere; compose with Phi.
  have h_diag_on : ContinuousOn (fun w : ℝ => ((w, w) : ℝ × ℝ))
      (Set.image F (Set.Ioi 0)) :=
    (continuous_id.prodMk continuous_id).continuousOn
  have h_maps : Set.MapsTo (fun w : ℝ => ((w, w) : ℝ × ℝ))
      (Set.image F (Set.Ioi 0))
      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
    intro w hw
    exact ⟨hw, hw⟩
  -- Use ContinuousOn.comp on the explicit lambda form of uncurry.
  have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont
  have h_comp : ContinuousOn
      ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
      (Set.image F (Set.Ioi 0)) :=
    h_phi_on.comp h_diag_on h_maps
  -- Convert the composition into the simpler form.
  have h_eq : ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
              = (fun v : ℝ => Phi v v) := by
    funext w
    rfl
  rw [h_eq] at h_comp
  exact h_comp
THEOREM iterate_continuous_on_range · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
iterate_continuous_on_range · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean:114 
/-- **Iteration produces continuous orbits.**  If we iterate Φ on a starting
element v ∈ Range(F), the n-fold iterate is again in Range(F), and the map
v ↦ Φ^[n](v, v) is continuous on Range(F). -/
theorem iterate_continuous_on_range
    (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
    (hClosed : IteratedClosureOnRange F Phi)
    (n : ℕ) :
    ∃ φₙ : ℝ → ℝ,
      ContinuousOn φₙ (Set.image F (Set.Ioi 0)) ∧
      (∀ v ∈ Set.image F (Set.Ioi 0), φₙ v ∈ Set.image F (Set.Ioi 0)) := by
  -- Define the iterate by recursion on n.  Inductively, each iterate is
  -- a continuous map from Range(F) into Range(F).
  induction n with
  | zero =>
    refine ⟨id, ?_, ?_⟩
    · exact continuousOn_id
    · intro v hv
      exact hv
  | succ k ih =>
    obtain ⟨φₖ, hCont_φₖ, hMap_φₖ⟩ := ih
    refine ⟨fun v => Phi (φₖ v) v, ?_, ?_⟩
    · -- Continuity of v ↦ Phi(φₖ v, v) via ContinuousOn.comp.
      obtain ⟨hCont_Phi, _⟩ := hClosed
      have h_pair_on : ContinuousOn (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ))
          (Set.image F (Set.Ioi 0)) :=
        hCont_φₖ.prodMk continuousOn_id
      have h_maps : Set.MapsTo (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ))
          (Set.image F (Set.Ioi 0))
          ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
        intro w hw
        exact ⟨hMap_φₖ w hw, hw⟩
      have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
          ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont_Phi
      have h_comp : ContinuousOn
          ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘
            (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ)))
          (Set.image F (Set.Ioi 0)) :=
        h_phi_on.comp h_pair_on h_maps
      have h_eq : ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘
                    (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ)))
                  = (fun v : ℝ => Phi (φₖ v) v) := by
        funext w
        rfl
      rw [h_eq] at h_comp
      exact h_comp
    · intro v hv
      obtain ⟨_, hClosure⟩ := hClosed
      exact hClosure (φₖ v) v (hMap_φₖ v hv) hv
THEOREM ClosedUnderIteration · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
ClosedUnderIteration · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean:64 
/-- A combining rule Φ is **closed under iteration** on a set `S ⊆ ℝ` if
applying Φ to two elements of S produces an element of S, and the result is
continuous in both inputs. -/
def ClosedUnderIteration (Phi : ℝ → ℝ → ℝ) (S : Set ℝ) : Prop :=
  ContinuousOn (Function.uncurry Phi) (S ×ˢ S) ∧
  ∀ u v : ℝ, u ∈ S → v ∈ S → Phi u v ∈ S

What this page does not claim

The module does not prove that the combining rule is a polynomial. The module does not prove that closure under iteration forces analyticity. The module does not derive the golden ratio or the eight-tick cycle.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND