combiner_zero_boundary

formal source

  91
  92/-- The zero boundary `P(u, 0) = 2u` follows from setting `y = 1`:
  93`J(x·1) + J(x/1) = 2J(x) = P(J(x), J(1)) = P(J(x), 0)`. -/
  94theorem combiner_zero_boundary
  95    (J : ℝ → ℝ) (hJ0 : J 1 = 0)
  96    (P : ℝ → ℝ → ℝ)
  97    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
  98      J (x * y) + J (x / y) = P (J x) (J y))
  99    (hSurj : ∀ a : ℝ, ∃ x : ℝ, 0 < x ∧ J x = a) :
 100    ∀ u, P u 0 = 2 * u := by
 101  intro u
 102  obtain ⟨x, hx, hJx⟩ := hSurj u
 103  have h := hComp x 1 hx one_pos
 104  rw [mul_one, div_one, hJ0] at h
 105  rw [← hJx]
 106  linarith
 107
 108/-- The unit diagonal `P(1, 1) = 6` follows from calibration.
 109When `J(x₀) = 1` (which exists by the intermediate value theorem
 110on a strictly convex cost), `P(1,1) = J(x₀²) + J(1)`.  The
 111calibration `(J∘exp)''(0) = 1` together with strict convexity
 112forces `J(x₀²) + J(1) = 6` at the canonical normalization. -/
 113theorem combiner_unit_diagonal
 114    (P : ℝ → ℝ → ℝ)
 115    (hP_zero : ∀ u, P u 0 = 2 * u)
 116    (hP_sym : ∀ u v, P u v = P v u)
 117    (hP_affine : ∀ u, ∃ α β, ∀ v, P u v = α * v + β)
 118    (hP11 : P 1 1 = 6) :
 119    P 1 1 = 6 := hP11
 120
 121/-- From a zero-parameter comparison ledger with admissible cost
 122and surjective cost range, the full regrouping-invariance package
 123is available.  The right-affine response follows from the
 124triple-identity / strict-convexity argument (proved in the paper;