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 the Recognition Composition Law with an explicit functional-identity hypothesis. Researchers deriving the mass ladder, Berry threshold, or alpha band from Recognition Science axioms cite it to fix the precise form of J. The module assembles convexity, functional-equation lemmas, and the Law of Existence into a chain of supporting results that close the uniqueness argument on positive reals.

claimThe unique function $J: \mathbb{R}_+ \to \mathbb{R}$ satisfying the composition law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, together with $J(x) > 0$ for $x \neq 1$, continuity, $J(1) = 0$, and the reciprocal symmetry $J(x) = J(1/x)$, is given by $J(x) = \frac12(x + x^{-1}) - 1$.

background

The module operates inside the CostUniqueness domain and imports five supporting modules. Cost.Convexity establishes that $J_{\log}(t) = \cosh t - 1$ is strictly convex on $\mathbb{R}$ and that $J_{\rm cost}(x) = \frac12(x + x^{-1}) - 1$ is strictly convex on $\mathbb{R}_+$. Cost.FunctionalEquation supplies the auxiliary lemmas needed for the T5 argument. CPM.LawOfExistence encodes the generic Coercive Projection Method (projection-defect inequality, coercivity factorization, aggregation). ClosedObservableFramework supplies the positive observables, ratio interface, and conservation structure that absorb earlier regularity requirements.

The local theoretical setting is the forcing chain T0-T8 in which T5 isolates the unique cost function compatible with the Recognition Composition Law before T6 forces the self-similar fixed point $\phi$.

proof idea

The module organizes the uniqueness proof as a sequence of intermediate lemmas (Jcost_continuous_pos, Jcost_is_reciprocal, Jcost_is_normalized, Jcost_satisfies_composition_law, Jcost_is_calibrated) that feed unique_cost_on_pos_from_rcl and finally T5_uniqueness_complete. Each lemma applies convexity from Cost.Convexity and the functional-equation helpers from Cost.FunctionalEquation; the Law of Existence supplies the aggregation step that lifts local identities to the global uniqueness statement.

why it matters in Recognition Science

CostUniqueness completes the T5 step of the forcing chain and supplies the cost axioms required by the downstream module CostAxioms, which formalizes the three primitive axioms from which logical coherence emerges. The result directly underwrites the RS-native constants ($\hbar = \phi^{-5}$, $G = \phi^5/\pi$) and the yardstick mass formula on the $\phi$-ladder.

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)