IndisputableMonolith.Cost.Ndim.Uniqueness

   1import IndisputableMonolith.Cost.Ndim.Core
   2
   3/-!
   4# Uniqueness lift theorem for the n-dimensional extension
   5
   6This module captures the forcing pattern:
   7if a candidate factors through the weighted multiplicative aggregate and the
   8scalar factor is uniquely fixed to `Jcost` on positive reals, then the whole
   9multi-component functional is forced to be `JcostN`.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Cost
  14namespace Ndim
  15
  16/-- `F` factors through the weighted aggregate via some scalar profile `G`. -/
  17def FactorsThrough {n : ℕ} (F : Vec n → ℝ) (α : Vec n) : Prop :=
  18  ∃ G : ℝ → ℝ, ∀ x : Vec n, F x = G (aggregate α x)
  19
  20/-- Main forcing theorem: scalar uniqueness forces the `n`-dimensional lift. -/
  21theorem forced_of_scalar_uniqueness {n : ℕ}
  22    (F : Vec n → ℝ) (α : Vec n) (G : ℝ → ℝ)
  23    (hfactor : ∀ x : Vec n, F x = G (aggregate α x))
  24    (hscalar : ∀ {u : ℝ}, 0 < u → G u = Jcost u) :
  25    ∀ x : Vec n, F x = JcostN α x := by
  26  intro x
  27  calc
  28    F x = G (aggregate α x) := hfactor x
  29    _ = Jcost (aggregate α x) := hscalar (aggregate_pos α x)
  30    _ = JcostN α x := by simp [JcostN_eq_Jcost_aggregate]
  31
  32/-- Existential version of the forcing theorem. -/
  33theorem forced_of_factorization {n : ℕ}
  34    (F : Vec n → ℝ) (α : Vec n)
  35    (hfac : FactorsThrough F α)
  36    (hscalar_unique : ∀ G : ℝ → ℝ,
  37      (∀ x : Vec n, F x = G (aggregate α x)) →
  38      (∀ {u : ℝ}, 0 < u → G u = Jcost u)) :
  39    ∀ x : Vec n, F x = JcostN α x := by
  40  rcases hfac with ⟨G, hG⟩
  41  exact forced_of_scalar_uniqueness F α G hG (hscalar_unique G hG)
  42
  43end Ndim
  44end Cost
  45end IndisputableMonolith
  46