forced_of_scalar_uniqueness
plain-language theorem explainer
The theorem shows that if an n-dimensional functional F factors through a scalar G applied to the aggregate of α and x, and G equals Jcost on all positive reals, then F equals the n-dimensional JcostN everywhere. Researchers extending scalar cost functions to vectors in Recognition Science cite it to obtain uniqueness of the lift. The proof is a three-step calculation that substitutes the factorization, invokes positivity of the aggregate to apply the scalar hypothesis, and rewrites via the equivalence JcostN_eq_Jcost_aggregate.
Claim. Let $F : (0,1]^n → ℝ$, $α ∈ (0,1]^n$, and $G : ℝ → ℝ$. Suppose $F(x) = G(aggregate(α,x))$ for every $x$ and $G(u) = Jcost(u)$ for every $u > 0$. Then $F(x) = JcostN(α,x)$ for every $x$.
background
The Cost.Ndim.Uniqueness module develops the forcing pattern for n-dimensional cost functionals. The aggregate is the exponential of the dot product of α with the componentwise logarithm of x, acting as a weighted multiplicative mean that reduces the vector input to a positive scalar. JcostN is the n-dimensional extension of the scalar Jcost, related to it by the identity JcostN α x = Jcost(aggregate α x).
proof idea
The tactic proof introduces an arbitrary vector x and applies a calc chain. The first step rewrites F x as G(aggregate α x) by the factorization hypothesis. The second step replaces G with Jcost by invoking the scalar uniqueness hypothesis on the positive value aggregate α x (using aggregate_pos). The final step rewrites Jcost(aggregate α x) as JcostN α x by simp with the equivalence lemma JcostN_eq_Jcost_aggregate.
why it matters
This is the core forcing theorem that lifts scalar uniqueness to the n-dimensional setting and is invoked by the existential form forced_of_factorization in the same module. It fills the uniqueness step in the Recognition Science forcing chain (T5 J-uniqueness), ensuring that any candidate cost functional agreeing with Jcost on the aggregate is forced to be the full JcostN. The result closes a gap between the scalar functional equation and its multi-component extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.