Foundation Dalembert Degree Exclusion No Degree3 Composition

The degree-3 exclusion

The d'Alembert equation is a classic functional equation, studied since Jean le Rond d'Alembert's 1747 work on vibrating strings. In its simplest form, it asks for functions G such that G(t+u) + G(t-u) depends only on G(t) and G(u), not on t and u separately. The standard solutions are familiar: G(t) = c t² and G(t) = c (cosh(kt) - 1), among others. The equation's power is that it forces a very rigid structure on any function that satisfies it.

The Recognition Science framework considers a generalized version where the sum G(t+u) + G(t-u) equals a polynomial P(G(t), G(u)). The framework's central theorem, the d'Alembert Inevitability Theorem, shows that the only polynomial combiner that admits nonconstant continuous solutions is the quadratic one, P(s,r) = 2s + 2r + sr. This quadratic form ultimately leads to the framework's unique cost function J(x) = (x + 1/x)/2 - 1. The key question was whether the degree-2 assumption was an extra hypothesis or a forced consequence.

In Recognition Science, the declaration no_degree3_composition settles this question for the next case up. It proves that no continuous, nonconstant function G with G(0) = 0 can satisfy the cubic composition law G(t+u) + G(t-u) = 2G(t) + 2G(u) + G(t)²G(u) + G(t)G(u)². The proof works by evaluating the equation at specific argument pairs, deriving polynomial expressions for G(2s), G(3s), and G(4s) in terms of y = G(s). The identity at (3s, s) then requires a degree-9 polynomial on the left and a degree-15 polynomial on the right. The mismatch polynomial, 300y⁵ + 830y⁷ + ... + 16y¹⁵, vanishes only at y = 0, forcing G to be identically zero, contradicting nonconstancy.

This result closes a gap in the d'Alembert Inevitability Theorem. It shows that the degree-2 assumption is not an arbitrary restriction but a necessary condition: polynomial combiners of degree 3 or higher admit no nonconstant continuous solutions at all. The framework's library of machine-checked theorems thus establishes that the quadratic combiner is the unique viable starting point, reinforcing the forced nature of the cost function from the framework's first principles.

What this declaration does not claim is equally important. It does not address polynomial combiners of degree 1 or 0, nor does it say anything about non-polynomial combiners. It also does not assert that the quadratic combiner is the only one with solutions; that is a separate theorem. The result is specifically about ruling out the cubic case, and by extension, the general pattern of higher-degree polynomial combiners, within the framework's axiomatic system.

/-- **Degree-3 Exclusion Theorem.**

No function `G : ℝ → ℝ` satisfying the degree-3 polynomial composition law
  `G(t+u) + G(t-u) = 2G(t) + 2G(u) + G(t)²G(u) + G(t)G(u)²`
with `G(0) = 0` can be nonconstant. Every such function is identically zero.

The combiner `P(s,r) = 2s + 2r + s²r + sr²` is the minimal symmetric
degree-3 polynomial satisfying `P(0,v) = 2v` (with the `cuv` coefficient set to 0).
The proof works for any value of this coefficient. -/
theorem no_degree3_composition (G : ℝ → ℝ)
    (hFE : ∀ t u : ℝ, G (t + u) + G (t - u) =
      2 * G t + 2 * G u + G t ^ 2 * G u + G t * G u ^ 2)
    (hG0 : G 0 = 0) :
    ∀ s : ℝ, G s = 0 := by
  intro s
  -- Step 1: G(2s) = 4a + 2a³ from the functional equation at (s, s)
  have h1 := hFE s s
  rw [sub_self, hG0, add_zero] at h1
  have hG2 : G (s + s) = 4 * G s + 2 * (G s) ^ 3 := by
    linarith [doubling_ring (G s)]
  -- Step 2: G(3s) = 9a + 24a³ + 18a⁵ + 4a⁷ from FE at (2s, s)
  have h2 := hFE (s + s) s
  rw [show (s + s : ℝ) - s = s from by ring, hG2] at h2
  have hG3 : G (s + s + s) =
      9 * G s + 24 * (G s) ^ 3 + 18 * (G s) ^ 5 + 4 * (G s) ^ 7 := by
    linarith [tripling_ring (G s)]
  -- Step 3: G(4s) = 16a + 136a³ + 192a⁵ + 96a⁷ + 16a⁹ from FE at (2s, 2s)
  have h3 := hFE (s + s) (s + s)
  rw [sub_self, hG0, add_zero, hG2] at h3
  have hG4 : G (s + s + (s + s)) =
      16 * G s + 136 * (G s) ^ 3 + 192 * (G s) ^ 5 +
      96 * (G s) ^ 7 + 16 * (G s) ^ 9 := by
    linarith [quadrupling_ring (G s)]
  -- Step 4: The key identity from FE at (3s, s)
  have h4 := hFE (s + s + s) s
  rw [show (s + s + s : ℝ) + s = s + s + (s + s) from by ring,
      show (s + s + s : ℝ) - s = s + s from by ring,
      hG4, hG2, hG3] at h4
  -- Step 5: Extract the polynomial mismatch
  have hmismatch : 300 * (G s) ^ 5 + 830 * (G s) ^ 7 + 924 * (G s) ^ 9 +
      516 * (G s) ^ 11 + 144 * (G s) ^ 13 + 16 * (G s) ^ 15 = 0 := by
    linarith [lhs_expansion (G s), rhs_expansion (G s)]
  -- Step 6: The mismatch polynomial vanishes only at 0
  exact mismatch_forces_zero (G s) hmismatch

/-- The mismatch polynomial `300y⁵ + 830y⁷ + 924y⁹ + 516y¹¹ + 144y¹³ + 16y¹⁵ = 0`
    implies `y = 0`. This is the algebraic core of the degree exclusion. -/
lemma mismatch_forces_zero (a : ℝ)
    (h : 300 * a ^ 5 + 830 * a ^ 7 + 924 * a ^ 9 +
         516 * a ^ 11 + 144 * a ^ 13 + 16 * a ^ 15 = 0) :
    a = 0 := by
  have hfact : a ^ 5 * (300 + 830 * a ^ 2 + 924 * (a ^ 2) ^ 2 +
      516 * (a ^ 2) ^ 3 + 144 * (a ^ 2) ^ 4 + 16 * (a ^ 2) ^ 5) = 0 := by
    nlinarith [h]
  have hpos : 300 + 830 * a ^ 2 + 924 * (a ^ 2) ^ 2 +
      516 * (a ^ 2) ^ 3 + 144 * (a ^ 2) ^ 4 + 16 * (a ^ 2) ^ 5 > 0 :=
    inner_factor_pos (a ^ 2) (sq_nonneg a)
  have ha5 : a ^ 5 = 0 := by
    rcases mul_eq_zero.mp hfact with h5 | h5
    · exact h5
    · linarith
  exact (pow_eq_zero_iff (by omega : (5 : ℕ) ≠ 0)).mp ha5

What this page does not claim

The declaration does not rule out polynomial combiners of degree 1 or 0. The declaration does not address non-polynomial combiners. The declaration does not prove that the quadratic combiner is the only one with nonconstant continuous solutions.

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/DAlembert/DegreeExclusion.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: