Cost Ndim Uniqueness Factors Through

The factorization lift

The declaration FactorsThrough names a simple structural condition on a cost function that takes several inputs at once. A cost function here means a rule that assigns a real number to a vector of positive weights, measuring the price of recognizing a compound event. The condition says the function depends on its inputs only through a single weighted aggregate, a weighted sum of the inputs with fixed coefficients. In symbols, a function F factors through the aggregate when there exists a scalar profile G such that F(x) = G(aggregate(x)) for every input vector x. The aggregate itself is a weighted sum, so the condition means all the multi-input detail collapses into one number before the cost is applied.

The surrounding theorem, forced_of_scalar_uniqueness, turns that condition into a uniqueness result. The framework's library already proves that any scalar cost function satisfying five plain conditions must equal Jcost(u) = (u + 1/u)/2 - 1 on positive reals. The theorem says: if a multi-component function factors through the weighted aggregate, and the scalar profile is uniquely fixed to Jcost on positive inputs, then the whole multi-component function is forced to equal JcostN, the n-dimensional extension of Jcost. The proof is a short chain: the factorization gives F(x) = G(aggregate(x)), the scalar uniqueness gives G(u) = Jcost(u) for positive u, and a definitional identity identifies Jcost(aggregate(x)) with JcostN(x). The existential version, forced_of_factorization, packages the same argument for the case where the factorization is given as an assumption.

What the declaration does not claim matters as much as what it proves. FactorsThrough is a definition, not a theorem; it merely states the factorization condition. The theorems that use it require the scalar uniqueness as a separate hypothesis, so the declaration alone forces nothing. The result also does not say that every multi-component cost function factors through the aggregate, nor that the aggregate itself is unique, nor that the n-dimensional extension JcostN is the only possible cost function without the factorization condition. The theorem works only for functions that already satisfy the factorization structure, and it inherits the scalar uniqueness theorem's own hypotheses about the five plain conditions on the scalar profile.

In plain terms, the declaration is a bridge. It connects a one-dimensional uniqueness result to a multi-dimensional one, but only when the multi-dimensional function is already known to collapse through a single weighted sum. The payoff is that the framework's forcing chain, which establishes Jcost on positive reals, extends to vector inputs without a new proof of uniqueness from scratch. The cost of that payoff is the factorization hypothesis, which must be checked case by case. A reader should take away that the n-dimensional result is a lift of the scalar theorem, not an independent derivation.

/-- `F` factors through the weighted aggregate via some scalar profile `G`. -/
def FactorsThrough {n : ℕ} (F : Vec n → ℝ) (α : Vec n) : Prop :=
  ∃ G : ℝ → ℝ, ∀ x : Vec n, F x = G (aggregate α x)

/-- Main forcing theorem: scalar uniqueness forces the `n`-dimensional lift. -/
theorem forced_of_scalar_uniqueness {n : ℕ}
    (F : Vec n → ℝ) (α : Vec n) (G : ℝ → ℝ)
    (hfactor : ∀ x : Vec n, F x = G (aggregate α x))
    (hscalar : ∀ {u : ℝ}, 0 < u → G u = Jcost u) :
    ∀ x : Vec n, F x = JcostN α x := by
  intro x
  calc
    F x = G (aggregate α x) := hfactor x
    _ = Jcost (aggregate α x) := hscalar (aggregate_pos α x)
    _ = JcostN α x := by simp [JcostN_eq_Jcost_aggregate]

/-- Existential version of the forcing theorem. -/
theorem forced_of_factorization {n : ℕ}
    (F : Vec n → ℝ) (α : Vec n)
    (hfac : FactorsThrough F α)
    (hscalar_unique : ∀ G : ℝ → ℝ,
      (∀ x : Vec n, F x = G (aggregate α x)) →
      (∀ {u : ℝ}, 0 < u → G u = Jcost u)) :
    ∀ x : Vec n, F x = JcostN α x := by
  rcases hfac with ⟨G, hG⟩
  exact forced_of_scalar_uniqueness F α G hG (hscalar_unique G hG)

What this page does not claim

FactorsThrough alone forces any function: it is a definition, and the forcing theorems require the scalar uniqueness hypothesis as a separate assumption. Every multi-component cost function factors through the weighted aggregate, or the aggregate is unique. The n-dimensional cost function JcostN is derived without the factorization condition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/Uniqueness.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: