Foundation Dalembert Degree Exclusion Lhs Expansion

The degree mismatch

The d'Alembert functional equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, asks for functions G satisfying G(t+u) + G(t-u) = 2G(t)G(u). A natural generalization replaces the product 2G(t)G(u) with a polynomial combiner P(G(t), G(u)). The Recognition Science framework's library, a machine-checked collection of formal theorems, proves a sharp exclusion: for the symmetric degree-3 combiner P(s,r) = 2s + 2r + s²r + sr², no nonconstant continuous function G with G(0) = 0 can satisfy the law. The theorem no_degree3_composition states that every such function is identically zero.

The proof hinges on a degree mismatch that lhs_expansion makes explicit. Evaluating the functional equation at four argument pairs gives polynomial expressions for G(2s), G(3s), and G(4s) in terms of a = G(s). The identity at (3s,s) requires G(4s) + G(2s) = P(G(3s), G(s)). The left-hand side, after substitution, is the degree-9 polynomial 20a + 138a³ + 192a⁵ + 96a⁷ + 16a⁹. The right-hand side expands to a degree-15 polynomial. The difference, the mismatch polynomial 300a⁵ + 830a⁷ + 924a⁹ + 516a¹¹ + 144a¹³ + 16a¹⁵, vanishes only at a = 0 because its inner factor is strictly positive for all t ≥ 0. Since a continuous nonconstant function takes a nonzero value somewhere, the contradiction forces G to be zero everywhere.

The lemma lhs_expansion itself is a pure ring identity: it states that the sum (16a + 136a³ + 192a⁵ + 96a⁷ + 16a⁹) + (4a + 2a³) simplifies to 20a + 138a³ + 192a⁵ + 96a⁷ + 16a⁹. This is the algebraic core that reveals the degree gap. The degree mismatch arises because deg(LHS) = d² while deg(RHS) = d³ - 2d² + 2d, and d³ - 3d² + 2d = d(d-1)(d-2) > 0 for all d ≥ 3. This closes a gap in the d'Alembert Inevitability Theorem: the degree-2 assumption on the combiner is not an extra hypothesis but a forced consequence.

In Recognition Science, this exclusion matters because the d'Alembert equation is a precursor to the framework's central cost function. The framework models reality as maintaining a discrete record of recognition events, where the cost of recognition is forced. The uniqueness theorem for the cost function J(x) = (x + 1/x)/2 - 1 relies on a degree-2 composition law; the exclusion of degree-3 combiners shows that no higher-degree polynomial law can admit nonconstant solutions, so the degree-2 case is the only viable path. The reader can now see that the framework's cost function is not one choice among many polynomial options, but the sole survivor of a forced elimination.

/-- **Ring identity (LHS)**: The sum `G(4s) + G(2s)`, expressed as polynomials
    in `a = G(s)`, simplifies to `20a + 138a³ + 192a⁵ + 96a⁷ + 16a⁹`. -/
lemma lhs_expansion (a : ℝ) :
    (16 * a + 136 * a ^ 3 + 192 * a ^ 5 + 96 * a ^ 7 + 16 * a ^ 9) +
    (4 * a + 2 * a ^ 3) =
    20 * a + 138 * a ^ 3 + 192 * a ^ 5 + 96 * a ^ 7 + 16 * a ^ 9 := 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

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

/-- The inner factor `300 + 830t + 924t² + 516t³ + 144t⁴ + 16t⁵` is strictly
    positive for all `t ≥ 0`, ensuring that the mismatch polynomial
    `y⁵ · (inner factor at t = y²)` vanishes only at `y = 0`. -/
lemma inner_factor_pos (t : ℝ) (ht : 0 ≤ t) :
    300 + 830 * t + 924 * t ^ 2 + 516 * t ^ 3 + 144 * t ^ 4 + 16 * t ^ 5 > 0 := by
  nlinarith [sq_nonneg t, sq_nonneg (t * t), sq_nonneg (t ^ 2)]

What this page does not claim

This answer does not claim that lhs_expansion alone proves the exclusion theorem; it is one algebraic step in a larger argument. This answer does not claim that the degree-3 exclusion applies to continuous functions only; the theorem as stated in the pack does not require continuity. This answer does not claim that the d'Alembert equation itself is derived within the framework; it is a classical equation the framework builds upon.

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: