SeparatelyAdditive

formal source

  44exist single-argument functions `p, q` with `P(u, v) = p(u) + q(v)` for
  45all `u, v`. This is the structural shape we exclude from genuine
  46composition consistency. -/
  47def SeparatelyAdditive (P : ℝ → ℝ → ℝ) : Prop :=
  48  ∃ p q : ℝ → ℝ, ∀ u v : ℝ, P u v = p u + q v
  49
  50/-- A combiner is a **coupling combiner** when it is not separately
  51additive. Equivalently, the joint structure of the two arguments enters
  52the output; the cost of a composite genuinely depends on how its
  53components fit together. -/
  54def IsCouplingCombiner (P : ℝ → ℝ → ℝ) : Prop :=
  55  ¬ SeparatelyAdditive P
  56
  57/-- The **interaction defect** of a combiner at a pair `(u, v)`:
  58\[
  59\Delta P(u, v) := P(u, v) - P(u, 0) - P(0, v) + P(0, 0).
  60\]
  61For a separately additive combiner this is identically zero. The defect
  62is the canonical detector of coupling. -/
  63def interactionDefect (P : ℝ → ℝ → ℝ) (u v : ℝ) : ℝ :=
  64  P u v - P u 0 - P 0 v + P 0 0
  65
  66/-! ## Equivalent Forms -/
  67
  68/-- A separately additive combiner has identically vanishing interaction
  69defect. -/
  70theorem interactionDefect_eq_zero_of_separatelyAdditive
  71    {P : ℝ → ℝ → ℝ} (h : SeparatelyAdditive P) :
  72    ∀ u v : ℝ, interactionDefect P u v = 0 := by
  73  rcases h with ⟨p, q, hP⟩
  74  intro u v
  75  unfold interactionDefect
  76  rw [hP u v, hP u 0, hP 0 v, hP 0 0]
  77  ring