Cost Ndim Uniqueness Forced Of Scalar Uniqueness

The uniqueness lift

In mathematics, a cost function assigns a number to each possible choice, measuring how expensive that choice is. Recognition Science studies cost functions that satisfy five plain conditions, and a proved theorem shows that any such scalar cost function must equal J(x) = (x + 1/x)/2 - 1. The question arises: if you have a cost function on several components at once, and each component is combined through a weighted aggregate into a single scalar, does the scalar uniqueness force the whole multi-component function to be unique too?

The declaration forced_of_scalar_uniqueness answers yes. It states: if a candidate multi-component function F factors through a weighted aggregate via some scalar profile G, and if G is already known to equal Jcost on positive reals, then F must equal JcostN, the n-dimensional extension of Jcost. The proof is a short chain of equalities: F applied to a vector equals G applied to the aggregate, which equals Jcost applied to the aggregate, which by definition equals JcostN applied to the vector. A second theorem, forced_of_factorization, packages the same result with the factorization as an explicit hypothesis.

The theorem does not prove that every multi-component cost function factors through a weighted aggregate. That factorization is a premise, not a conclusion. It also does not prove the scalar uniqueness itself; it assumes the scalar profile is already fixed to Jcost. The theorem is a lift: it takes uniqueness in one dimension and transfers it to n dimensions, provided the structural condition holds.

What this changes is practical. If you are building a recognition ledger, a discrete record of events with forced costs, and you have already established the scalar cost, you do not need to re-prove uniqueness for each new dimension. The n-dimensional form follows automatically from the scalar result plus the factorization condition. This is the kind of modular step that lets a large formal library grow without rechecking every base case.

/-- 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

The theorem does not prove that every multi-component cost function factors through a weighted aggregate. The theorem does not prove the scalar uniqueness of Jcost; it assumes it as a hypothesis. The theorem does not establish any empirical claim about physical systems; it is a formal statement about cost functions.

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: