costUniqueness_clause_holds
plain-language theorem explainer
The cost-uniqueness clause carried by the quantum-gravity master theorem holds unconditionally: any admissible cost functional is forced to the unique J-cost. Non-circularity auditors of the master conjunction cite this field. The proof is a one-line alias of the already-proved uniqueness theorem, which applies the law-of-logic forcing of J-cost.
Claim. The carried cost-uniqueness proposition holds: every real functional $F$ on positive reals that satisfies reciprocity, normalization, the Recognition Composition Law, calibration, and continuity coincides with the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$).
background
This module is a field-by-field non-circularity audit of the unconditional quantum-gravity master theorem. A referee objection was that witness slots of shape $\Sigma(P:\mathrm{Prop}),P$ can be inhabited by trivial placeholders. For each atom of the master conjunction the audit discloses the concrete proposition and proves it holds without assuming the master conclusion.
Cost uniqueness is the T5 landmark of the forcing chain: the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, together with reciprocity, normalization, calibration, and continuity, forces $J(x)=(x+x^{-1})/2-1$. In the master theorem the clause is the named proposition CostUniqueness_carried_prop, not definitional True.
Upstream, CostUniqueness_proven already discharges that proposition by invoking law_of_logic_forces_jcost on an arbitrary admissible $F$. The present declaration simply re-exports that fact under the audit's clause-naming convention.
proof idea
One-line term proof: the goal is definitionally MasterTheorem.CostUniqueness, which equals the carried uniqueness proposition, and that is exactly the conclusion of CostUniqueness_proven. No new tactics or hypotheses are introduced. The real work lives upstream: CostUniqueness_proven introduces an arbitrary $F$ with reciprocity, normalization, composition, calibration, and continuity, then applies Cost.FunctionalEquation.law_of_logic_forces_jcost pointwise.
why it matters
After the M1–M3 upgrades, cost uniqueness is no longer a True placeholder inside the master conjunction. This audit theorem records that the carried clause holds on its own, so assembling the master statement does not smuggle in the conclusion. That is the peer-review non-circularity requirement (F1 / Rec 2) for this field.
Framework-wise it is the gravity-side packaging of T5 J-uniqueness from the Unified Forcing Chain and of the Recognition Composition Law. Downstream the module uses the same pattern for T0–T8, BMV positivity, and the closed certificates; together those clauses justify that the unconditional master theorem is a genuine conjunction of independently proved physics propositions rather than a circular witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.