RegroupingInvariance

formal source

  40/-- Regrouping invariance: the combiner is symmetric and satisfies the
  41boundary and normalization conditions forced by the abelian group
  42structure of `(ℝ₊, ×)` and the calibration of `J`. -/
  43structure RegroupingInvariance (J : ℝ → ℝ) extends ContextualSubstitutivity J where
  44  symmetric : ∀ u v, combiner u v = combiner v u
  45  zero_boundary : ∀ u, combiner u 0 = 2 * u
  46  unit_diagonal : combiner 1 1 = 6
  47  right_affine : ∀ u, ∃ α β, ∀ v, combiner u v = α * v + β
  48
  49/-- Contextual substitutivity is forced by the ledger's comparison
  50structure: if `J(x₁) = J(x₂)`, then for any `y > 0`,
  51
  52  `J(x₁ y) + J(x₁/y) = J(x₂ y) + J(x₂/y)`
  53
  54because the compound cost depends only on the mismatch, not on the
  55specific ratio realizing it.  Therefore the compound cost descends
  56to a function of `(J(x), J(y))`. -/
  57def substitutivity_forces_factorization
  58    (J : ℝ → ℝ) (hJ0 : J 1 = 0)
  59    (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
  60    (P : ℝ → ℝ → ℝ)
  61    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
  62      J (x * y) + J (x / y) = P (J x) (J y)) :
  63    ContextualSubstitutivity J :=
  64  ⟨P, hComp⟩
  65
  66/-- Symmetry of the combiner follows from commutativity of `(ℝ₊, ×)`:
  67`J(xy) + J(x/y) = J(yx) + J(y/x)` because `xy = yx` and
  68`J(x/y) = J(y/x)` by reciprocal symmetry. -/
  69theorem combiner_symmetric
  70    (J : ℝ → ℝ)
  71    (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
  72    (P : ℝ → ℝ → ℝ)
  73    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →