cert
plain-language theorem explainer
Packages three elementary facts into the uniqueness-master certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone invoking the RS uniqueness master theorem v3 cites this inhabited certificate rather than the three lemmas separately. Construction is a pure structure fill-in from sibling proofs.
Claim. There is an inhabited uniqueness certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module states a structural uniqueness master theorem: $J$ is the unique cost satisfying the four RS axioms, so constants, masses, and cosmological parameters are forced from $J$. The certificate structure collects three side conditions used by that master argument.
Domain cost is the RS cost evaluated on a pair of positive reals (measure and event scales). Vanishing on the diagonal means equal arguments incur zero cost, matching the $J$-minimum at identity. Nonnegativity is the global lower bound inherited from $J(x)\ge 0$. The canonical threshold is the positive cutoff against which cost comparisons are made in the uniqueness packing.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The three sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields of the certificate structure.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and strict positivity of the threshold by canonicalThreshold_pos. No extra algebra or tactics.
why it matters
Gives a single named certificate object for RS Uniqueness Master Theorem v3 (Plan v7), the structural theorem that $J$ is the unique function obeying the four RS axioms. That uniqueness is the T5 landmark in the forcing chain ($J(x)=(x+x^{-1})/2-1$), from which T6--T8 force $\varphi$, the eight-tick octave, and $D=3$. Downstream the sibling cert_inhabited and any master-theorem consumers can quote this package rather than three separate lemmas. No open sorry: status is structural with zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.