perturbativeCost
plain-language theorem explainer
The perturbative cost approximates the J-cost for small log deviations t as the quadratic term t squared over 2. Physicists matching Standard Model renormalization flows to the geometric Recognition Science mass ladder would cite this definition when isolating the leading weak-coupling behavior. It is supplied directly as the explicit quadratic formula without further reduction.
Claim. The perturbative cost function is defined by $C_0(t) = t^2/2$ for real $t$.
background
In the Unification.CouplingLaw module the gap between geometric residues F(Z) on the phi-ladder and small perturbative running f_RG is closed by the J-cost. Upstream, cost from MultiplicativeRecognizerL4 is the derived cost of a comparator on positive ratios, while cost from ObserverForcing is the J-cost of any recognition event. The module states that J(e^t) equals cosh(t) minus 1, so the quadratic Taylor term t^2/2 supplies the perturbative limit of that exact cost.
proof idea
The declaration is a direct definition that writes the quadratic term t^2/2 explicitly.
why it matters
It supplies the perturbative side of the coupling identity used by coupling_identity and CouplingLawCert. Those results establish that exactCost equals coshEnhancement times perturbativeCost for t not zero, with the enhancement factor forced solely by the Recognition Composition Law and the identification J = cosh minus 1. The definition therefore anchors the bridge between the eight-tick octave geometry and Standard Model running without introducing free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.