pith. sign in
module module high

IndisputableMonolith.CostUniqueness

show as:
view Lean formalization →

CostUniqueness delivers the complete T5 uniqueness theorem for the J-cost under an explicit functional-identity hypothesis. Researchers reconstructing physics from the Recognition Composition Law cite this result to fix the form of the cost function before deriving phi and the forcing chain. The argument combines strict convexity of J, composition-law identities, and coercivity bounds from the Law of Existence.

claimUnder the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, with $J$ strictly convex on $R_+$, normalized by $J(1)=0$, and positive, the unique solution is $J(x) = (x + x^{-1})/2 - 1$.

background

The module sits inside the Closed Observable Framework, which encodes positive-valued observables, a ratio interface, and conservation as structure fields. It draws the convexity of $Jlog(t) = cosh t - 1$ on $R$ and of $Jcost(x) = 1/2(x + x^{-1}) - 1$ on $R_+$ from the Convexity module. FunctionalEquation supplies the algebraic identities needed for T5, while LawOfExistence contributes the projection-defect inequality and coercivity factorization that control uniqueness.

proof idea

The module imports convexity, functional-equation lemmas, and the Law of Existence. It first certifies regularity, normalization, and reciprocity of Jcost, then applies the composition law together with defect bounds to reach uniqueness. The central result T5_uniqueness_complete is obtained by algebraic reduction under the explicit functional-identity hypothesis.

why it matters in Recognition Science

This module supplies the uniqueness proof imported by CostAxioms, which formalizes the three primitive axioms from which logical coherence emerges. It completes the T5 step of the forcing chain, where J-uniqueness is required before phi is forced as the self-similar fixed point and before the eight-tick octave and D=3 are derived.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (10)