forced_of_factorization
The theorem shows that any functional F on n-vectors factoring through the weighted aggregate via some scalar G must equal the n-dimensional J-cost JcostN whenever G is the unique function agreeing with Jcost on positives. Researchers extending the Recognition Science cost model to multiple dimensions cite this when lifting scalar results. The proof is a direct one-line wrapper that unpacks the factorization existential and applies the scalar uniqueness lemma.
claimLet $F : (Fin n) → ℝ$ and $α : (Fin n) → ℝ$. If there exists a scalar $G : ℝ → ℝ$ such that $F(x) = G(R(α, x))$ for all $x$, where $R$ denotes the exponential aggregate $R(α, x) = exp(α · log x)$, and if every such $G$ satisfies $G(u) = J(u)$ for $u > 0$, then $F(x) = J_N(α, x)$ for all $x$, where $J_N$ is the n-dimensional cost.
background
The module establishes the uniqueness lift for n-dimensional extensions of the cost functional. Vec n is the type of n-component real vectors. FactorsThrough F α is the proposition that F factors through the aggregate, i.e., there exists G such that F x = G(aggregate α x) for all x. The aggregate itself is defined as exp(dot α (logVec x)). JcostN α x is the n-dimensional cost obtained by applying the log-coordinate form JlogN to the logged vector.
proof idea
The term-mode proof first applies rcases to the hypothesis hfac, extracting the witness G and the equality hG. It then invokes the upstream lemma forced_of_scalar_uniqueness on F, α, G, hG together with the uniqueness hypothesis instantiated at that same G.
why it matters in Recognition Science
This supplies the existential form of the forcing theorem inside Cost.Ndim.Uniqueness. It guarantees that scalar uniqueness of Jcost propagates to the full vector functional JcostN once factorization holds. Within the Recognition Science framework the result closes the lift step that follows J-uniqueness (T5) and supports the overall forcing chain to the eight-tick octave and D = 3. No downstream uses are recorded in the current graph.
scope and limits
- Does not establish scalar uniqueness of Jcost on its own.
- Does not apply when the factorization hypothesis fails.
- Does not treat vectors containing non-positive coordinates.
- Does not derive the explicit expression for the scalar Jcost.
formal statement (Lean)
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
proof body
Term-mode proof.
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