IndisputableMonolith.CostUniqueness
The CostUniqueness module delivers the full T5 uniqueness theorem for the cost function under an explicit functional-identity hypothesis. Researchers closing the primitive cost axioms in Recognition Science cite this result. The argument assembles convexity of J, functional-equation reductions, and the closed observable framework into a single completeness statement.
claimThe function $J(x) = \frac12(x + x^{-1}) - 1$ on $\mathbb{R}_+$ is the unique solution to the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ that is continuous, positive, normalized at 1, and satisfies the explicit functional-identity hypothesis.
background
The module imports Cost, Convexity (which proves strict convexity of both $J\log(t) = \cosh t - 1$ and $J\cost(x)$), FunctionalEquation (lemmas for T5), LawOfExistence (CPM parts A/B/C), and ClosedObservableFramework (positive observables, ratio interface, and the remaining Regularity Axiom). These supply the structural setting in which cost uniqueness is proved rather than assumed.
Sibling declarations inside the module (T5_uniqueness_complete, unique_cost_on_pos, Jcost_satisfies_composition_law, etc.) together constitute the complete T5 statement with the functional-identity hypothesis made explicit.
proof idea
The module first imports convexity to obtain strict convexity of Jcost, then applies functional-equation helpers to reduce the composition law to a uniqueness statement. It folds in the Coercive Projection Method from LawOfExistence and the regularity supplied by ClosedObservableFramework to reach the full theorem under the explicit hypothesis.
why it matters in Recognition Science
This module feeds the CostAxioms module, which formalizes the three primitive axioms describing the structure of cheap configurations. It completes the T5 step of the forcing chain (T0-T8), allowing the cost function to be derived from the Recognition Composition Law rather than postulated. The downstream CostAxioms documentation states that these axioms are more primitive than logic itself.
scope and limits
- Does not derive the Recognition Composition Law itself.
- Does not relax continuity or positivity assumptions.
- Does not extend uniqueness beyond positive reals.
- Does not address the full forcing chain past T5.
- Does not treat non-convex or non-normalized candidates.