cert
plain-language theorem explainer
Packages three proved facts about the domain cost into the structural certificate for the phi-uniqueness module: diagonal vanishing, nonnegativity on the positive quadrant, and a strictly positive canonical threshold. Anyone citing the module-6 structural theorem uses this bundle. The definition is a pure field assembly of three sibling lemmas.
Claim. The module-6 structural certificate asserts three properties of the domain cost $C$: (i) $C(r,r)=0$ for every nonzero real $r$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ satisfies $T>0$.
background
Module RS_PHY_Structural_006 records the structural side of RS phi uniqueness: $\varphi$ as the self-similar fixed point of the continued fraction $1+1/(1+1/(\cdots))$, forced already at T6 in the unified forcing chain. Status is a structural theorem with no sorry and no axioms.
The certificate structure collects three elementary properties of a real bivariate domain cost $C$ used in this module: vanishing on the diagonal away from zero, nonnegativity for positive mass/energy-style arguments, and positivity of a fixed canonical threshold. Upstream, the foundation lemma cost_nonneg states that every recognition event has nonnegative J-cost, via nonnegativity of $J$ on positive reals; the local nonnegativity field is the domain-cost analogue of that fact.
Sibling lemmas supply each field: diagonal identity of $C$, nonnegativity of $C$ on the open positive quadrant, and positivity of the canonical threshold constant.
proof idea
One-line structure instance. Each of the three certificate fields is filled by the corresponding sibling lemma already proved in the same module: diagonal vanishing, domain-cost nonnegativity, and canonical-threshold positivity. No additional rewriting or case analysis occurs at this site.
why it matters
Gives a single named inhabitant of the module-6 certificate type so downstream physics code can depend on one object rather than three separate lemmas. The module itself is the structural packaging of T6 (phi forced as the self-similar fixed point $\varphi=1+1/(1+1/(\cdots))$). With zero sorry and zero axioms, this certificate is the closed witness that the cost-side hypotheses of that structural theorem are discharged. No further used-by edges are recorded yet; the immediate consumer is the companion inhabitedness fact for the same certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.