forced_of_factorization
plain-language theorem explainer
If a candidate functional F on n-vectors factors through the weighted aggregate and any scalar profile realizing that factorization must coincide with Jcost on positives, then F equals the n-dimensional lift JcostN. Workers on uniqueness results for cost functionals in the Recognition Science framework cite this existential forcing statement. The proof is a one-line wrapper that destructs the factorization hypothesis and invokes the scalar uniqueness lemma.
Claim. Let $F : (Fin n) → ℝ$ and $α ∈ (Fin n) → ℝ$. Suppose $F$ factors through the weighted aggregate, i.e., there exists $G : ℝ → ℝ$ with $F(x) = G(aggregate(α,x))$ for all $x$. If every such scalar $G$ satisfies $G(u) = Jcost(u)$ whenever $0 < u$, then $F(x) = JcostN(α,x)$ for all $x$.
background
The module develops the uniqueness lift for the n-dimensional cost extension. FactorsThrough asserts that F factors through the weighted multiplicative aggregate: there exists a scalar profile G such that F(x) equals G applied to aggregate(α,x), where aggregate(α,x) = exp(∑ α_i log x_i). JcostN(α,x) is the n-dimensional cost obtained by composing the scalar J-cost with the log-vector map. The local setting is the forcing pattern: factorization plus scalar uniqueness implies the full multi-component functional is forced to JcostN.
proof idea
The term proof first performs rcases on the FactorsThrough hypothesis to extract the witnessing scalar G and the equality hG. It then applies forced_of_scalar_uniqueness directly to F, α, G, hG and the specialized uniqueness assumption obtained by instantiating hscalar_unique at that G.
why it matters
This is the existential version of the forcing theorem that lifts scalar uniqueness to the n-dimensional setting. It closes the uniqueness argument for cost functionals once the scalar case is settled, feeding the broader Recognition Science program of deriving all physics from the single functional equation and the J-uniqueness property (T5). No downstream uses are recorded yet, leaving open whether it will be invoked inside larger uniqueness or dimension-reduction arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.