CostUniqueness_proven
plain-language theorem explainer
Any real cost functional that is reciprocal, normalized, composition-law compliant, calibrated, and continuous must equal the J-cost J(x)=(x+x^{-1})/2-1. Gravity and master-theorem authors cite this as the closed cost-uniqueness clause of the RS quantum-gravity master statement. The proof is a one-line discharge into the Law-of-Logic uniqueness theorem from Cost.FunctionalEquation.
Claim. The cost-uniqueness clause holds: if $F:\mathbb{R}\to\mathbb{R}$ is a reciprocal cost, normalized, satisfies the Recognition Composition Law, is calibrated, and is continuous (under the standing Aczél smoothness package), then $F(x)=J(x)$ for all admissible $x$, where $J(x)=(x+x^{-1})/2-1$.
background
Track 7.A authors the RS quantum-gravity master theorem as a twelve-clause conjunction. Eight clauses are already closed from prior sessions; five remain as hypothesis inputs. Cost uniqueness is one of the closed structural clauses: it asserts that the recognition cost is forced, not chosen.
The J-cost is the unique reciprocal cost fixed by the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, together with normalization, calibration, and continuity. Equivalently $J(x)=\cosh(\log x)-1$. This is the T5 landmark in the T0–T8 forcing chain: once reciprocity and the composition law are imposed, no other continuous cost survives.
Upstream, law_of_logic_forces_jcost already proves that uniqueness under the global Aczél smoothness package, with no extra regularity parameters required from the caller. The master-theorem module only needs to package that fact as the named clause CostUniqueness.
proof idea
One-line wrapper. Introduce the cost $F$ and the reciprocity, normalization, composition-law, calibration, and continuity hypotheses, then apply Cost.FunctionalEquation.law_of_logic_forces_jcost directly to those hypotheses at the evaluation point $x$. No local algebra is redone; the clause is inhabited by the existing Law-of-Logic uniqueness theorem.
why it matters
Feeds the conditional master theorem rs_quantum_gravity_master_conditional, which discharges the eight closed clauses (including this one) and leaves only the five open-track hypotheses. Also anchors the non-circularity audit: costUniqueness_clause_holds and carried_clauses_hold cite this theorem to record that the cost-uniqueness conjunct is proved, not assumed.
In the framework this is T5 (J-uniqueness) packaged for gravity: the same cost that forces $\phi$, the eight-tick octave, and $D=3$ is the unique continuous reciprocal cost compatible with the Recognition Composition Law. Without this clause the master statement would still carry a free functional degree of freedom in the gravitational sector. It does not close the five open tracks (Regge continuum/Bianchi, unconditional amplitude linearity, Page curve, PTA vs inflation, strong-field discriminators); those remain hypothesis inputs to the conditional master theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.