costUniqueness_clause_is_carried
plain-language theorem explainer
The cost-uniqueness slot of the quantum-gravity master theorem is definitionally identical to the universal J-cost uniqueness proposition, not a trivial True placeholder. Formal auditors of the master conjunction cite this disclosure to confirm the clause carries real content. The proof is pure reflexivity on the two definitions.
Claim. The cost-uniqueness clause of the master theorem is definitionally equal to the carried proposition that asserts universal uniqueness of the $J$-cost (the unique reciprocal cost satisfying the recognition composition law, normalization, calibration, and continuity).
background
This module answers a peer-review objection to the unconditional quantum-gravity master theorem: its witness slots have the shape $\Sigma(P:\mathrm{Prop}), P$, which is inhabited by $\langle\mathrm{True},\mathrm{trivial}\rangle$ and so carries no content unless the plugged-in propositions are genuine. For each atom of the master conjunction the audit supplies an rfl-level disclosure of what proposition the field actually is, plus a standalone proof that the field holds without assuming any master clause.
Cost uniqueness is the Recognition Science claim that the $J$-cost $J(x)=(x+x^{-1})/2-1$ is the unique reciprocal cost obeying the recognition composition law (RCL), normalization, calibration, and continuity. Upstream, law_of_logic_forces_jcost states exactly that uniqueness under a global Aczél smoothness package, with no caller-supplied regularity parameters. After the M1/M2/M3 upgrades the master clause no longer stores True; it stores the named carried proposition CostUniqueness_carried_prop.
proof idea
One-line term proof by reflexivity: the two sides are definitionally equal by construction of the master clause after the carried-prop upgrade. No lemmas are applied; the equality is pure definitional unfolding. The sibling that actually discharges the proposition (rather than disclosing its identity) invokes Cost.FunctionalEquation.law_of_logic_forces_jcost.
why it matters
This disclosure is one of the six conjuncts assembled by master_theorem_non_circularity_certificate, which records that the cost-uniqueness clause carries the universal $J$-cost uniqueness theorem and holds unconditionally. Without it, a referee could still suspect the master slot is a vacuous placeholder or secretly contains the master conclusion.
In the forcing chain this sits at T5 ($J$-uniqueness): the same $J$ fixed by the RCL is the cost that gravity and recognition calculus inherit. The audit converts that landmark from prose citation into a field the master theorem literally carries, so non-circularity of the QG master statement follows from independently proved, concretely named, non-self-referential atoms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.