RGFixedPointCert
plain-language theorem explainer
A certificate structure packaging three analytic properties of the recognition domain cost and the canonical threshold used for the IR fixed-point coupling. Anyone citing the RS claim that the recognition RG flow fixes g* = J(φ) ≈ 0.118 at confinement will point here. It is a pure structure definition; inhabitants are assembled from sibling lemmas on domainCost and the threshold.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ vanishes; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical recognition threshold is strictly positive.
background
The module treats the infrared fixed point of the recognition renormalization-group flow. In Recognition Science the cost of a mismatch is the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and the Recognition Composition Law. The module claims the IR fixed coupling is $g^*=J(\varphi)\approx 0.118$, the canonical recognition coupling at the confinement scale.
Here "domain cost" is the two-argument cost on mass/energy (or scale) pairs built from that J-cost; equilibrium means equal arguments. The canonical threshold is the positive scale cut used to mark the fixed-point regime. Upstream, nonnegativity of recognition-event cost is already known: any recognition event has cost $\ge 0$ via $J$-cost nonnegativity on positive states.
proof idea
No proof body: this is a structure definition. It simply names three fields that any inhabitant must supply: diagonal vanishing of domain cost off zero, nonnegativity of domain cost on the positive quadrant, and positivity of the canonical threshold. Concrete filling is deferred to the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos, which the module's cert definition plugs in fieldwise.
why it matters
This certificate is the typed interface for the module's structural claim that the recognition RG fixed point is controlled by J-cost geometry rather than an independent coupling constant. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty RGFixedPointCert, closing the 0-sorry structural theorem advertised in the module doc.
In the broader framework it supports the QED-style fixed-point story $\alpha(\mu=\infty)\to$ strong coupling, specialized to RS units where the IR value is $g^*=J(\varphi)$ with $\varphi$ the golden ratio forced at T6. It does not itself compute $\alpha^{-1}$ in the $(137.030,137.039)$ band; it only packages the cost/threshold hypotheses that later physics modules use when tying confinement-scale coupling to the phi ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.