ContextualSubstitutivity

formal source

  32`x` and `y`.  This is the minimal invariance principle of a
  33comparison ledger: if two subcomparisons carry the same mismatch
  34cost, they are interchangeable in any compound context. -/
  35structure ContextualSubstitutivity (J : ℝ → ℝ) where
  36  combiner : ℝ → ℝ → ℝ
  37  factors : ∀ x y : ℝ, 0 < x → 0 < y →
  38    J (x * y) + J (x / y) = combiner (J x) (J y)
  39
  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