reparamDiagonal

formal source

  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