IndisputableMonolith.Foundation.LogicAsFunctionalEquation.AnalyticCounterexample

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.QuarticLogCounterexample
   3
   4/-!
   5# Analytic reparameterisation counterexample
   6
   7The corrected Phase 6 conjecture, "real-analytic combiner at the origin
   8implies polynomial degree ≤ 2", is false.
   9
  10This module proves the algebraic core of the counterexample.  Start with the
  11standard RCL variable `K = cosh(t)-1`, and analytically reparameterize the
  12cost coordinate by `f(s) = s+s^2`.  In the reparameterized variable
  13`a = s+s^2`, the diagonal of the induced combiner is
  14
  15`4s + 18s^2 + 16s^3 + 4s^4`.
  16
  17No degree-2 RCL-family combiner with boundary form `Phi(a,0)=2a` can have
  18that diagonal, since `4a + c a^2` gives coefficients
  19`4s + (4+c)s^2 + 2c s^3 + c s^4`.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Foundation
  24namespace LogicAsFunctionalEquation
  25
  26/-- The diagonal of the analytically reparameterized combiner in the local
  27coordinate `s` where `a = s+s^2`. -/
  28def reparamDiagonal (s : ℝ) : ℝ :=
  29  4 * s + 18 * s^2 + 16 * s^3 + 4 * s^4
  30
  31/-- The diagonal of any degree-2 RCL-family combiner with boundary
  32`Phi(a,0)=2a`, written in the same local coordinate `a=s+s^2`. -/
  33def degreeTwoDiagonal (c s : ℝ) : ℝ :=
  34  4 * (s + s^2) + c * (s + s^2)^2
  35
  36/-- The reparameterized analytic combiner diagonal cannot be represented by
  37any degree-2 RCL-family diagonal for all local coordinates `s`. -/
  38theorem reparam_diagonal_not_degree_two :
  39    ¬ ∃ c : ℝ, ∀ s : ℝ, reparamDiagonal s = degreeTwoDiagonal c s := by
  40  intro h
  41  rcases h with ⟨c, hc⟩
  42  have h1 := hc 1
  43  have h2 := hc 2
  44  unfold reparamDiagonal degreeTwoDiagonal at h1 h2
  45  norm_num at h1 h2
  46  -- h1: 42 = 8 + 4c, so c = 17/2.
  47  -- h2: 168 = 24 + 36c, so c = 4.
  48  linarith
  49
  50/-- Equivalently, no coefficient `c` makes
  51`4s + 18s^2 + 16s^3 + 4s^4 = 4(s+s^2) + c(s+s^2)^2` as a function of `s`. -/
  52theorem reparam_coefficients_obstruct_degree_two
  53    (c : ℝ) :
  54    ¬ (∀ s : ℝ, reparamDiagonal s = degreeTwoDiagonal c s) := by
  55  intro h
  56  exact reparam_diagonal_not_degree_two ⟨c, h⟩
  57
  58end LogicAsFunctionalEquation
  59end Foundation
  60end IndisputableMonolith
  61