RGFixed2Cert
plain-language theorem explainer
Certificate structure that packages three analytic facts needed for an RS two-scale RG fixed-point story: the domain cost vanishes on the diagonal, stays nonnegative for positive scales, and the canonical threshold is positive. Anyone wiring the phi-ladder RG module (Gaussian UV / Wilson–Fisher IR) cites this type. It is a pure structure definition; inhabitation is deferred to a later def.
Claim. A two-scale RG fixed-point certificate is a triple of properties: (i) the domain cost vanishes on equal nonzero scales, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative whenever both mass and energy scales are positive; (iii) the canonical threshold is strictly positive.
background
The module builds an RG fixed-point structure from the phi-ladder and the Recognition J-cost. In RS the Wilson–Fisher IR exponents at $D=3$ are read off as $\eta=J(\varphi)\approx 0.118$ and $\nu=1/\varphi\approx 0.618$, with $\nu$ already within a few percent of the empirical value. The local objects are a two-argument domain cost (mass vs energy scale) and a canonical threshold that marks the fixed-point window.
Upstream, nonnegativity of recognition cost is already forced: any recognition event has $0\le e.\mathrm{cost}$ because $J$ is nonnegative on positive reals. The present certificate simply lifts that style of positivity and diagonal-vanishing statements into the RG scale pair $(m,e)$.
Status of the module is structural: zero sorry, zero axioms. The certificate is the interface that later defs must inhabit.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of the domain cost, nonnegativity for positive scales, positivity of the canonical threshold). Inhabitation is supplied separately by the def cert, which plugs in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
This type is the contract for the RG-from-J-cost story in Plan v7 session 3. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty RGFixed2Cert, so later physics lemmas can assume a fixed-point certificate without re-proving the three analytic facts.
In the broader framework it sits under the $D=3$ forcing (T8) and the unique J-cost (T5): the same $J$ that yields the RCL and the phi self-similarity also supplies the cost whose fixed-point geometry is being certified. The module’s target exponents ($\eta=J(\varphi)$, $\nu=1/\varphi$) are the quantitative payoff once the certificate is in hand; the structure itself only locks the qualitative fixed-point axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.