phiCost
plain-language theorem explainer
The phi cost function maps real u to cosh of (log phi times u) minus one. Analysts of annular rings and Jensen coercivity bounds in Recognition Science invoke this as the explicit cost for phase increments under logarithmic scaling. It is introduced as a direct abbreviation realizing the hyperbolic cosine form of the J function at powers of phi.
Claim. $phiCost(u) := cosh((log phi) u) - 1$ for $u in R$.
background
The Annular J-Cost Framework defines phiCost as the fundamental cost on phase increments for concentric rings. By construction phiCost(u) equals cosh((log phi) u) - 1, which coincides with the J-cost of phi^u via the identity J(x) = cosh(log x) - 1. This supplies the building block for ring cost summation and winding-constrained samples in annular meshes.
proof idea
This declaration is a one-line definition that transcribes the cosh representation of J directly into log-coordinates using the constant phi.
why it matters
This definition anchors all annular cost calculations, feeding annularCost, jensen_ring_bound, phiCost_convexOn, and the linear-quadratic perturbation bounds. It realizes the J-uniqueness and phi fixed-point steps of the forcing chain by giving the explicit cost for self-similar scaling on rings. The module leaves open the concrete trace family construction for the analytic carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.