Foundation Dalembert Degree Exclusion Rhs Expansion

The degree exclusion

The declaration rhs_expansion is a lemma in the framework's machine-checked library of formal theorems. It establishes a purely algebraic fact: when a certain cubic combination rule is applied to the values G(3s) and G(s), the result expands into a specific degree-15 polynomial in a = G(s). The identity is checked by the computer algebra system's ring tactic, meaning it is a verified equality of polynomial expressions, not an approximation or a numerical check.

This identity is one step in a larger proof, the degree-3 exclusion theorem. The theorem states that no continuous, nonconstant function G : R → R 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 law at specific argument pairs. From (s,s), (2s,s), and (2s,2s), the framework derives polynomial expressions for G(2s), G(3s), and G(4s) in terms of y = G(s). The identity at (3s,s) then requires G(4s) + G(2s) to equal the right-hand side, but the two sides have different degrees: the left side is degree 9, the right side is degree 15. The mismatch polynomial vanishes only at y = 0, contradicting the assumption that G is nonconstant.

The significance lies in what it removes. The d'Alembert Inevitability Theorem, which forces the unique cost function J(x) = (x + 1/x)/2 - 1, previously assumed the composition law was quadratic. This exclusion theorem shows that assumption is not an extra hypothesis but a forced consequence: no cubic or higher-degree polynomial combiner admits any nonconstant continuous solution. The degree-2 case is the only one that can work.

What the declaration does not claim is equally important. It does not assert that the cubic law has no solutions at all; the constant zero function satisfies it. It does not prove the d'Alembert theorem itself, only the exclusion of one class of combiners. And it says nothing about the physical interpretation of the cost function or about any empirical measurements. The lemma is a formal algebraic step, and its power comes from being part of a larger, axiom-clean chain.

/-- **Ring identity (RHS)**: `P(G(3s), G(s))` expands to a degree-15 polynomial in `a`. -/
lemma rhs_expansion (a : ℝ) :
    2 * (9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7) + 2 * a +
    (9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7) ^ 2 * a +
    (9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7) * a ^ 2 =
    20 * a + 138 * a ^ 3 + 492 * a ^ 5 + 926 * a ^ 7 + 940 * a ^ 9 +
    516 * a ^ 11 + 144 * a ^ 13 + 16 * a ^ 15 := by ring

/-- **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

What this page does not claim

The constant zero function is not excluded by the theorem. The declaration does not prove the d'Alembert Inevitability Theorem itself. No physical or empirical claim is made by this algebraic lemma.

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: