CouplingRun3Cert
plain-language theorem explainer
A certificate packing three structural properties of the domain cost used for three-flavor coupling running: the cost vanishes on the diagonal, stays nonnegative for positive mass and energy scales, and the canonical threshold is strictly positive. Anyone assembling or discharging the CouplingRun3 certificate cites this bundle. It is a pure structure definition; inhabitants are built by plugging in the sibling lemmas.
Claim. A certificate consists of three facts about the domain cost $C$ and the canonical threshold $\tau$: (i) $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module treats running couplings on the Recognition Science phi-ladder. The headline claim is that the strong coupling at the Z mass matches the J-cost of phi: $\alpha_s(M_Z)=J(\phi)\approx 0.118$, against the experimental $0.1179$.
Domain cost is the two-argument cost that compares a mass scale to an energy scale in the running. The canonical threshold is the positive cutoff that marks when the cost-based running is active. Both sit beside the classical J-cost $J(x)=(x+x^{-1})/2-1$, whose nonnegativity is already forced upstream.
Upstream, cost_nonneg records that every recognition event has nonnegative cost, via $J$-cost nonnegativity on positive states. The present structure lifts that positivity language to the two-scale domain cost used for coupling running.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Downstream, the concrete inhabitant cert fills them by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Inhabitation is then one constructor application.
why it matters
This certificate is the typed interface for the structural theorem that three-flavor coupling running is controlled by J-cost on the phi-ladder. Downstream, cert assembles a concrete value and cert_inhabited proves the type is nonempty, closing the module's zero-sorry claim.
In the broader framework it supports the RS QCD prediction $\alpha_s=J(\phi)$ at the Z scale, tying the running story to T5 J-uniqueness and the phi fixed point (T6). It does not itself compute a numerical beta function; it only packages the cost axioms the numerical match relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.