combiner_unit_diagonal

formal source

 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;
 125encoded here as a hypothesis on the combiner). -/
 126def ledger_forces_regrouping
 127    (J : ℝ → ℝ) (hJ0 : J 1 = 0)
 128    (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
 129    (P : ℝ → ℝ → ℝ)
 130    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
 131      J (x * y) + J (x / y) = P (J x) (J y))
 132    (hSurj : ∀ a : ℝ, ∃ x : ℝ, 0 < x ∧ J x = a)
 133    (hAffine : ∀ u, ∃ α β, ∀ v, P u v = α * v + β)
 134    (hP11 : P 1 1 = 6) :
 135    RegroupingInvariance J :=
 136  { combiner := P
 137    factors := hComp
 138    symmetric := combiner_symmetric J hSym P hComp hSurj
 139    zero_boundary := combiner_zero_boundary J hJ0 P hComp hSurj
 140    unit_diagonal := hP11
 141    right_affine := hAffine }
 142
 143/-- The regrouping-invariance package produces a