cert
plain-language theorem explainer
Packages three already-proved facts about the two-scale domain cost and the canonical threshold into a single RG fixed-point certificate. Anyone citing the structural RG-from-J-cost development uses this bundle rather than the three lemmas separately. The definition is a pure structure instance: each field is filled by a named sibling lemma.
Claim. There is a certificate recording that (i) the two-scale domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy scales; and (iii) the canonical threshold is strictly positive.
background
The module develops the renormalization-group fixed-point structure implied by the Recognition Science cost $J$, on the $\varphi$-ladder at spatial dimension $D=3$. The status line is structural: zero sorry, zero axioms. The intended fixed points are the Gaussian UV fixed point and the Wilson–Fisher IR fixed point, with RS critical exponents $\eta=J(\varphi)\approx 0.118$ and $\nu=1/\varphi\approx 0.618$.
The certificate type bundles three elementary properties of the two-argument domain cost (the cost comparing a mass scale to an energy scale) and of the canonical threshold used to separate UV/IR regimes. Nonnegativity of recognition cost is the global prior: every recognition event has cost $\ge 0$, which is the $J$-cost nonnegativity theorem from ObserverForcing.
Sibling lemmas already establish diagonal vanishing, domain-cost nonnegativity on the positive quadrant, and positivity of the canonical threshold; this definition only names the triple as one object.
proof idea
One-line structure instance. The three fields of RGFixed2Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new algebra is performed; the definition is pure packaging.
why it matters
Gives a single named inhabitant of the RG fixed-point certificate so downstream material can assume the three cost/threshold axioms by one hypothesis rather than three. The module frames this as the structural backbone for reading Wilson–Fisher exponents off $J$ at $D=3$ (primer landmark T8), with $\eta=J(\varphi)$ and $\nu=1/\varphi$ (T5–T6). No used_by edges are recorded yet; the immediate sibling cert_inhabited is the natural consumer. Empirical tension on $\eta$ (RS $\sim 0.118$ vs measured $\sim 0.036$) is acknowledged in the module doc and is not discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.