RSGRVStructural006Cert
plain-language theorem explainer
A certificate packing three structural facts used in the gravity module on phi uniqueness: the domain cost vanishes on the diagonal, stays non-negative off it for positive arguments, and the canonical threshold is strictly positive. Gravity and forcing-chain authors cite it when they need a single inhabited bundle rather than three separate lemmas. It is a pure structure definition; inhabitance is discharged downstream by wiring the sibling lemmas.
Claim. A certificate consists of three properties of the domain cost $C$ and the canonical threshold $\tau$: (i) $C(r,r)=0$ for every nonzero real $r$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
Module 6 of the RS gravity structural series records the uniqueness of $\varphi$ as the self-similar fixed point of the continued fraction $1+1/(1+1/\cdots)$. The local objects are a domain cost $C:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ (the cost of matching a mass-like argument against an energy-like argument) and a canonical threshold $\tau>0$ that marks the scale at which the fixed-point comparison is meaningful.
Upstream, recognition cost is already known to be non-negative: any recognition event $e$ satisfies $0\le e.\mathrm{cost}$, via non-negativity of the $J$-cost on positive states. The present certificate lifts that non-negativity (and the diagonal vanishing) into the gravity-domain cost used for the $\varphi$-uniqueness argument, together with positivity of the comparison threshold.
proof idea
No proof body: this is a structure declaration. The three fields are pure Prop-valued requirements. Inhabitation is supplied by the sibling definition cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields, and by the one-line theorem cert_inhabited that packages that assignment as Nonempty.
why it matters
The certificate is the single object that module 6 exports as evidence that its structural obligations are met. Downstream, cert builds a concrete inhabitant and cert_inhabited records non-emptiness, so later gravity lemmas can assume the bundle rather than re-prove diagonal vanishing, non-negativity, and threshold positivity. In the broader RS chain this sits under T6 ($\varphi$ forced as the self-similar fixed point) and under the non-negativity of $J$-cost that begins the forcing ladder. It does not itself prove uniqueness of $\varphi$; it only packages the cost-and-threshold side conditions that the uniqueness argument consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.