Foundation Dalembert Degree Exclusion Tripling Ring

The tripling identity

The declaration tripling_ring is a lemma in the framework's machine-checked library of formal theorems. It states a purely algebraic identity: for any real number a, the expression 2·(4a + 2a³) + 2a + (4a + 2a³)²·a + (4a + 2a³)·a² − a simplifies to 9a + 24a³ + 18a⁵ + 4a⁷. This is not a claim about the physical world; it is a fact about how polynomials combine, verified by the symbolic rule that multiplication distributes over addition.

The identity earns its name because it describes what happens when you triple an input. Suppose a function G obeys a composition law of the form G(t+u) + G(t−u) = 2G(t) + 2G(u) + G(t)²G(u) + G(t)G(u)², with G(0) = 0. Setting u = t gives a formula for G(2t) in terms of G(t). The tripling identity then plugs that doubling formula into the composition law again, with u = 2t, to express G(3t) as a polynomial in G(t). The lemma is the algebraic engine that makes this substitution work.

This engine drives a larger result. The framework proves that no continuous, nonconstant function can satisfy the degree-3 composition law above. The proof evaluates the law at four argument pairs, deriving polynomial expressions for G(2t), G(3t), and G(4t). The tripling identity supplies the middle step. A final comparison at (3t, t) forces a mismatch: the left side has degree 9 in G(t), while the right side has degree 15. The difference vanishes only when G(t) = 0, and continuity then forces G to be identically zero. This closes a gap in the framework's d'Alembert Inevitability Theorem, showing that the degree-2 assumption there is not an extra hypothesis but a forced consequence.

The tripling identity itself proves nothing about physics, space, or time. It is a lemma about polynomial arithmetic. Its role is architectural: it is one of several ring identities that together make the degree-exclusion theorem go through. The framework's significance claim is about the theorem, not about this lemma alone. The identity does not establish that the degree-3 law has no solutions; that is the theorem's job. It does not say anything about what functions G might exist; it only says that if one exists, its tripling behavior must follow this algebraic rule.

What the lemma changes is the proof's structure. Without it, the step from doubling to tripling would require a separate argument each time. With it, the framework has a reusable algebraic fact, checked once, that plugs into the exclusion theorem. The reader can now see the degree-exclusion proof as a chain of polynomial identities, each one simple, that together rule out an entire family of composition laws.

/-- **Ring identity (G(3s))**: Expanding `P(G(2s), G(s)) - G(s)`. -/
lemma tripling_ring (a : ℝ) :
    2 * (4 * a + 2 * a ^ 3) + 2 * a +
    (4 * a + 2 * a ^ 3) ^ 2 * a + (4 * a + 2 * a ^ 3) * a ^ 2 - a =
    9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7 := 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 tripling identity alone does not prove the degree-3 exclusion theorem; it is one algebraic step within that proof. This lemma does not state anything about the physical world, space, or time. The degree-3 exclusion theorem does not claim that all composition laws of degree 3 are impossible, only this specific symmetric form.

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: