FactorsThrough
plain-language theorem explainer
FactorsThrough defines the property that an n-dimensional cost function F factors through a scalar profile G applied to the weighted aggregate of its arguments. Researchers proving uniqueness lifts from scalar to vector costs in Recognition Science would cite this definition when establishing that multi-component functionals are determined by their one-dimensional restrictions. The definition is introduced directly as an existential quantification over the scalar G.
Claim. Let $F : (Fin n) → ℝ$ and $α : (Fin n) → ℝ$. Then $F$ factors through $α$ if there exists a scalar function $G : ℝ → ℝ$ such that $F(x) = G( exp(α · log x) )$ for all $x$, where · is the dot product and the exponential aggregate is taken componentwise.
background
The Cost.Ndim.Uniqueness module develops the uniqueness lift theorem for the n-dimensional extension of cost functionals. Vec n is the type of n-component real vectors, realized as functions Fin n → ℝ. The aggregate operation computes the weighted multiplicative mean via exp(∑ α_i log x_i), serving as the reduction map from vector to scalar arguments. The module states that if a candidate factors through this aggregate and the scalar factor is uniquely fixed to Jcost on positive reals, then the full multi-component functional is forced to JcostN.
proof idea
This is a one-line definition that introduces the existential quantifier over a scalar function G such that F equals G composed with aggregate α.
why it matters
FactorsThrough supplies the hypothesis type for the downstream theorem forced_of_factorization, which states the existential version of the forcing theorem. It fills the step that lifts scalar uniqueness results to n dimensions, consistent with the Recognition Science forcing chain from J-uniqueness through the phi-ladder to the eight-tick octave. The definition closes the interface between the scalar FunctionalEquation and the vector Core constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.