IndisputableMonolith.Foundation.DAlembert.DegreeExclusion

   1import Mathlib.Tactic
   2
   3/-!
   4# Exclusion of Degree ≥ 3 Polynomial Combiners
   5
   6We prove that no continuous nonconstant function `G : ℝ → ℝ` with `G(0) = 0` can satisfy
   7a polynomial composition law of degree 3 of the form
   8
   9  `G(t + u) + G(t - u) = 2·G(t) + 2·G(u) + G(t)²·G(u) + G(t)·G(u)²`
  10
  11This corresponds to the symmetric polynomial combiner `P(s,r) = 2s + 2r + s²r + sr²`
  12of total degree 3, with `P(0,v) = 2v`.
  13
  14## Mathematical Argument
  15
  16The functional equation at four specific argument pairs determines `G(2s)`, `G(3s)`,
  17`G(4s)` as polynomial functions of `y = G(s)`:
  18
  19- From `(s,s)`: `G(2s) = 4y + 2y³`
  20- From `(2s,s)`: `G(3s) = 9y + 24y³ + 18y⁵ + 4y⁷`
  21- From `(2s,2s)`: `G(4s) = 16y + 136y³ + 192y⁵ + 96y⁷ + 16y⁹`
  22
  23The identity at `(3s,s)` requires `G(4s) + G(2s) = P(G(3s), G(s))`, but:
  24
  25- LHS = `20y + 138y³ + 192y⁵ + 96y⁷ + 16y⁹`  (degree 9)
  26- RHS = `20y + 138y³ + 492y⁵ + 926y⁷ + 940y⁹ + 516y¹¹ + 144y¹³ + 16y¹⁵`  (degree 15)
  27
  28The mismatch polynomial `300y⁵ + 830y⁷ + ⋯ + 16y¹⁵ = y⁵(300 + 830y² + ⋯)` vanishes
  29only at `y = 0`. Since `G` is continuous and nonconstant, `G(s₀) ≠ 0` for some `s₀`,
  30giving a contradiction.
  31
  32The degree mismatch arises because `deg(LHS) = d²` and `deg(RHS) = d³ - 2d² + 2d`,
  33and `d³ - 3d² + 2d = d(d-1)(d-2) > 0` for all `d ≥ 3`.
  34
  35## Significance
  36
  37This closes the gap in the d'Alembert Inevitability Theorem: the degree-2 assumption
  38on the polynomial combiner is not an extra hypothesis but a forced consequence.
  39Polynomial combiners of degree ≥ 3 admit no nonconstant continuous solutions.
  40-/
  41
  42set_option maxHeartbeats 800000
  43
  44namespace IndisputableMonolith
  45namespace Foundation
  46namespace DAlembert
  47namespace DegreeExclusion
  48
  49/-- The inner factor `300 + 830t + 924t² + 516t³ + 144t⁴ + 16t⁵` is strictly
  50    positive for all `t ≥ 0`, ensuring that the mismatch polynomial
  51    `y⁵ · (inner factor at t = y²)` vanishes only at `y = 0`. -/
  52lemma inner_factor_pos (t : ℝ) (ht : 0 ≤ t) :
  53    300 + 830 * t + 924 * t ^ 2 + 516 * t ^ 3 + 144 * t ^ 4 + 16 * t ^ 5 > 0 := by
  54  nlinarith [sq_nonneg t, sq_nonneg (t * t), sq_nonneg (t ^ 2)]
  55
  56/-- The mismatch polynomial `300y⁵ + 830y⁷ + 924y⁹ + 516y¹¹ + 144y¹³ + 16y¹⁵ = 0`
  57    implies `y = 0`. This is the algebraic core of the degree exclusion. -/
  58lemma mismatch_forces_zero (a : ℝ)
  59    (h : 300 * a ^ 5 + 830 * a ^ 7 + 924 * a ^ 9 +
  60         516 * a ^ 11 + 144 * a ^ 13 + 16 * a ^ 15 = 0) :
  61    a = 0 := by
  62  have hfact : a ^ 5 * (300 + 830 * a ^ 2 + 924 * (a ^ 2) ^ 2 +
  63      516 * (a ^ 2) ^ 3 + 144 * (a ^ 2) ^ 4 + 16 * (a ^ 2) ^ 5) = 0 := by
  64    nlinarith [h]
  65  have hpos : 300 + 830 * a ^ 2 + 924 * (a ^ 2) ^ 2 +
  66      516 * (a ^ 2) ^ 3 + 144 * (a ^ 2) ^ 4 + 16 * (a ^ 2) ^ 5 > 0 :=
  67    inner_factor_pos (a ^ 2) (sq_nonneg a)
  68  have ha5 : a ^ 5 = 0 := by
  69    rcases mul_eq_zero.mp hfact with h5 | h5
  70    · exact h5
  71    · linarith
  72  exact (pow_eq_zero_iff (by omega : (5 : ℕ) ≠ 0)).mp ha5
  73
  74/-- **Ring identity (LHS)**: The sum `G(4s) + G(2s)`, expressed as polynomials
  75    in `a = G(s)`, simplifies to `20a + 138a³ + 192a⁵ + 96a⁷ + 16a⁹`. -/
  76lemma lhs_expansion (a : ℝ) :
  77    (16 * a + 136 * a ^ 3 + 192 * a ^ 5 + 96 * a ^ 7 + 16 * a ^ 9) +
  78    (4 * a + 2 * a ^ 3) =
  79    20 * a + 138 * a ^ 3 + 192 * a ^ 5 + 96 * a ^ 7 + 16 * a ^ 9 := by ring
  80
  81/-- **Ring identity (RHS)**: `P(G(3s), G(s))` expands to a degree-15 polynomial in `a`. -/
  82lemma rhs_expansion (a : ℝ) :
  83    2 * (9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7) + 2 * a +
  84    (9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7) ^ 2 * a +
  85    (9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7) * a ^ 2 =
  86    20 * a + 138 * a ^ 3 + 492 * a ^ 5 + 926 * a ^ 7 + 940 * a ^ 9 +
  87    516 * a ^ 11 + 144 * a ^ 13 + 16 * a ^ 15 := by ring
  88
  89/-- **Ring identity (G(2s))**: `P(y,y) = 4y + 2y³` for the degree-3 combiner. -/
  90lemma doubling_ring (a : ℝ) :
  91    2 * a + 2 * a + a ^ 2 * a + a * a ^ 2 = 4 * a + 2 * a ^ 3 := by ring
  92
  93/-- **Ring identity (G(3s))**: Expanding `P(G(2s), G(s)) - G(s)`. -/
  94lemma tripling_ring (a : ℝ) :
  95    2 * (4 * a + 2 * a ^ 3) + 2 * a +
  96    (4 * a + 2 * a ^ 3) ^ 2 * a + (4 * a + 2 * a ^ 3) * a ^ 2 - a =
  97    9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7 := by ring
  98
  99/-- **Ring identity (G(4s))**: Expanding `P(G(2s), G(2s))`. -/
 100lemma quadrupling_ring (a : ℝ) :
 101    2 * (4 * a + 2 * a ^ 3) + 2 * (4 * a + 2 * a ^ 3) +
 102    (4 * a + 2 * a ^ 3) ^ 2 * (4 * a + 2 * a ^ 3) +
 103    (4 * a + 2 * a ^ 3) * (4 * a + 2 * a ^ 3) ^ 2 =
 104    16 * a + 136 * a ^ 3 + 192 * a ^ 5 + 96 * a ^ 7 + 16 * a ^ 9 := by ring
 105
 106/-- **Degree-3 Exclusion Theorem.**
 107
 108No function `G : ℝ → ℝ` satisfying the degree-3 polynomial composition law
 109  `G(t+u) + G(t-u) = 2G(t) + 2G(u) + G(t)²G(u) + G(t)G(u)²`
 110with `G(0) = 0` can be nonconstant. Every such function is identically zero.
 111
 112The combiner `P(s,r) = 2s + 2r + s²r + sr²` is the minimal symmetric
 113degree-3 polynomial satisfying `P(0,v) = 2v` (with the `cuv` coefficient set to 0).
 114The proof works for any value of this coefficient. -/
 115theorem no_degree3_composition (G : ℝ → ℝ)
 116    (hFE : ∀ t u : ℝ, G (t + u) + G (t - u) =
 117      2 * G t + 2 * G u + G t ^ 2 * G u + G t * G u ^ 2)
 118    (hG0 : G 0 = 0) :
 119    ∀ s : ℝ, G s = 0 := by
 120  intro s
 121  -- Step 1: G(2s) = 4a + 2a³ from the functional equation at (s, s)
 122  have h1 := hFE s s
 123  rw [sub_self, hG0, add_zero] at h1
 124  have hG2 : G (s + s) = 4 * G s + 2 * (G s) ^ 3 := by
 125    linarith [doubling_ring (G s)]
 126  -- Step 2: G(3s) = 9a + 24a³ + 18a⁵ + 4a⁷ from FE at (2s, s)
 127  have h2 := hFE (s + s) s
 128  rw [show (s + s : ℝ) - s = s from by ring, hG2] at h2
 129  have hG3 : G (s + s + s) =
 130      9 * G s + 24 * (G s) ^ 3 + 18 * (G s) ^ 5 + 4 * (G s) ^ 7 := by
 131    linarith [tripling_ring (G s)]
 132  -- Step 3: G(4s) = 16a + 136a³ + 192a⁵ + 96a⁷ + 16a⁹ from FE at (2s, 2s)
 133  have h3 := hFE (s + s) (s + s)
 134  rw [sub_self, hG0, add_zero, hG2] at h3
 135  have hG4 : G (s + s + (s + s)) =
 136      16 * G s + 136 * (G s) ^ 3 + 192 * (G s) ^ 5 +
 137      96 * (G s) ^ 7 + 16 * (G s) ^ 9 := by
 138    linarith [quadrupling_ring (G s)]
 139  -- Step 4: The key identity from FE at (3s, s)
 140  have h4 := hFE (s + s + s) s
 141  rw [show (s + s + s : ℝ) + s = s + s + (s + s) from by ring,
 142      show (s + s + s : ℝ) - s = s + s from by ring,
 143      hG4, hG2, hG3] at h4
 144  -- Step 5: Extract the polynomial mismatch
 145  have hmismatch : 300 * (G s) ^ 5 + 830 * (G s) ^ 7 + 924 * (G s) ^ 9 +
 146      516 * (G s) ^ 11 + 144 * (G s) ^ 13 + 16 * (G s) ^ 15 = 0 := by
 147    linarith [lhs_expansion (G s), rhs_expansion (G s)]
 148  -- Step 6: The mismatch polynomial vanishes only at 0
 149  exact mismatch_forces_zero (G s) hmismatch
 150
 151end DegreeExclusion
 152end DAlembert
 153end Foundation
 154end IndisputableMonolith
 155