CostUniqueness
plain-language theorem explainer
Aliases the T5 uniqueness proposition: any reciprocal, normalized, composition-law, calibrated cost F that is continuous on (0,∞) and carries Aczél smoothness equals the canonical J-cost. Gravity master-statement authors and foundation uniqueness proofs cite this named clause. The body is a one-line Prop synonym for the carried statement.
Claim. The cost-uniqueness clause is the proposition that every $F:\mathbb{R}\to\mathbb{R}$ satisfying Aczél smoothness, reciprocity, normalization $F(1)=0$, the Recognition Composition Law, calibration, and continuity on $(0,\infty)$ obeys $F(x)=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$.
background
Gravity.MasterTheorem authors the twelve-clause quantum-gravity master statement as named Props. Closed clauses are inhabited from existing theorems; structural and open clauses remain hypothesis inputs. Cost uniqueness is one of those named clauses.
The carried content is T5 J-uniqueness from the forcing chain: under the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ together with reciprocity, normalization, calibration, continuity on $(0,\infty)$, and Aczél smoothness, the unique cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The module doc ties this algebraic core to law-of-logic forcing via d'Alembert, witnessed upstream by the functional-equation result that forces $J$.
Sibling clauses in the same file package T0–T8, Lorentzian $1+3$, and related structural claims so the conditional master theorem can conjoin them uniformly.
proof idea
One-line definitional wrapper: CostUniqueness is definitionally equal to CostUniqueness_carried_prop. No tactics or lemmas run at this site. Mathematical content lives entirely in the carried Prop (universal quantification over costs with the five structural hypotheses plus continuity, concluding pointwise equality with canonical $J$). Discharge of that Prop is deferred to the separate proven witness and to foundation uniqueness theorems that cite this name.
why it matters
Pins the T5 slot inside the gravity master theorem template so Track 7.A can name cost uniqueness without inlining the full functional-equation statement. Downstream, foundation cost-axiom uniqueness and the unconditional d'Alembert complete forcing chain treat this clause as the canonical T5 specification; Delta-spine bridges equate discrete doubled costs to $2J(\varphi^n)$ and connect T6 $\varphi$ forcing to the same $J$. Regularity certificates for $J$ (continuity, strict convexity, log-second-derivative calibration) and maximal-forcing independence results also hang off this named Prop. In the primer chain it is exactly T5, the algebraic gate before $\varphi$, the eight-tick octave, and $D=3$. It does not itself close the five still-open master-theorem hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.