cert
plain-language theorem explainer
Packages three domain-cost lemmas into a single RG fixed-point certificate: equilibrium cost vanishes, cost is nonnegative off equilibrium, and the canonical threshold is positive. Physicists citing the IR recognition coupling g* = J(φ) use this bundle as the structural witness. Construction is a three-field structure instance, no extra proof work.
Claim. There is a certificate recording that the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive mass and energy arguments, and that the canonical threshold is strictly positive.
background
The module treats the infrared fixed point of the recognition renormalization-group flow. In Recognition Science the canonical coupling at that fixed point is $g^*=J(\varphi)\approx 0.118$, identified with the confinement-scale recognition coupling; the module status line calls this a structural theorem with no sorry and no axioms.
domainCost is the two-argument cost used for the RG domain comparison. The certificate structure RGFixedPointCert asks for three facts: cost vanishes when the two arguments coincide (equilibrium), cost is nonnegative for positive inputs, and the canonical threshold is positive. Upstream, nonnegativity of recognition cost is the standard $J$-cost fact: every recognition event has cost $\ge 0$, with the identity event at the $J$-minimum $x=1$.
proof idea
Pure structure assembly. The definition fills the three fields of RGFixedPointCert by pointing at the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos. No tactics and no new algebra; it is a named witness that those three results hold simultaneously.
why it matters
Gives a single inhabitance proof that the RG fixed-point side conditions are met, so downstream arguments can assume the certificate rather than re-cite the three lemmas. The module frames the physics claim as the QED-style IR fixed point (strong coupling as $\mu\to\infty$) realized in RS by $g^*=J(\varphi)$ at the confinement scale. That sits on the $J$-cost uniqueness chain (T5) and the forced self-similar scale $\varphi$ (T6). No used_by edges are recorded yet; the certificate is the local packaging step for that fixed-point story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.