Encyclopedia Foundation Foundation Dalembert Degree Exclusion Inner Factor Pos

ARTICLE 3 claims 3 theorems

Foundation Dalembert Degree Exclusion Inner Factor Pos

A small polynomial inequality, checked by machine, is the algebraic keystone that rules out entire families of candidate laws in the framework's foundational proof.

Verify this page

The positivity lemma

The declaration inner_factor_pos is a lemma in the machine-checked library of formal theorems behind Recognition Science. It states a plain algebraic fact: for any real number t that is zero or positive, the polynomial 300 + 830t + 924t² + 516t³ + 144t⁴ + 16t⁵ is strictly greater than zero. In other words, that six-term expression never dips to zero or below when its input is nonnegative.

Why care about one polynomial? The lemma sits inside a larger argument about the d'Alembert functional equation, a classical equation from 1747 that characterizes the cosine function. The framework studies generalized versions where the right-hand side is a polynomial combiner P(s,r). The degree-2 case yields the familiar cosine law. The question is whether degree 3 or higher could also admit nonzero continuous solutions. The answer, proved in the library, is no: no continuous nonconstant function G with G(0)=0 satisfies the degree-3 composition law G(t+u)+G(t-u)=2G(t)+2G(u)+G(t)²G(u)+G(t)G(u)². Every such function is identically zero.

The positivity lemma is the algebraic core of that exclusion. The proof evaluates the functional equation at four argument pairs, producing polynomial expressions for G(2s), G(3s), and G(4s). Comparing the two sides at (3s,s) yields a mismatch polynomial that must vanish. That polynomial factors as y⁵ times the inner factor above, with t replaced by y². Since the inner factor is strictly positive for all nonnegative t, the only way the product vanishes is y=0. Continuity then forces G to be constant everywhere, and G(0)=0 pins that constant to zero.

What the lemma does not claim is just as important. It does not assert anything about degree-2 combiners, which remain the viable case. It does not claim that the degree-3 equation has no solutions at all; the zero function satisfies it trivially. It does not say that the positivity holds for negative t, where the polynomial can indeed take negative values. And it does not, by itself, establish the full d'Alembert inevitability theorem; it is one ingredient, the algebraic keystone, within that larger proof.

THEOREM inner_factor_pos · IndisputableMonolith/Foundation/DAlembert/DegreeExclusion.lean
inner_factor_pos · IndisputableMonolith/Foundation/DAlembert/DegreeExclusion.lean:49 
/-- 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)]
THEOREM no_degree3_composition · IndisputableMonolith/Foundation/DAlembert/DegreeExclusion.lean
no_degree3_composition · IndisputableMonolith/Foundation/DAlembert/DegreeExclusion.lean:106 
/-- **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
THEOREM mismatch_forces_zero · IndisputableMonolith/Foundation/DAlembert/DegreeExclusion.lean
mismatch_forces_zero · IndisputableMonolith/Foundation/DAlembert/DegreeExclusion.lean:56 
/-- 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 lemma says nothing about degree-2 combiners, which remain the viable case. The lemma does not claim the degree-3 equation has no solutions at all; the zero function satisfies it trivially. The positivity statement does not extend to negative t, where the polynomial can take negative values.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND