phiCostLinearCoeff
plain-language theorem explainer
The linear perturbation coefficient for the φ-cost function f(u) = cosh((log φ) u) − 1 on the interval [−A, A] is log φ ⋅ sinh(log φ ⋅ A). Researchers decomposing annular ring costs into topological floor plus error terms cite this coefficient when controlling linear contributions from small phase perturbations. It is supplied by a direct one-line definition that evaluates the boundary derivative of the cosh expression.
Claim. Let $a = log φ$. For the cost function $f(u) = cosh(a u) − 1$ on the interval $[−A, A]$, the linear coefficient is $a sinh(a A)$.
background
In the annular J-cost framework the φ-cost is defined by $f(u) := cosh((log φ) ⋅ u) − 1$, equivalently $J(φ^u)$ via the hyperbolic representation of the J function. This supports perturbative bounds on sampled rings whose phase increments decompose into a uniform winding term plus small regular perturbations. The real parameter A bounds the absolute value of the phase coordinate u on each ring.
proof idea
One-line definition that directly evaluates the scaled hyperbolic sine at the boundary: log φ ⋅ sinh(log φ ⋅ A). This is the maximum absolute slope of f on [−A, A] because the derivative of cosh(a u) is a sinh(a u) and sinh is odd and increasing.
why it matters
The coefficient is invoked by the perturbative bound phiCost_add_le_phiCost_add_linear_quadratic and by the ring-level estimate ringCost_le_topologicalFloor_add_linear_quadratic_error that separates the topological floor from regular-part error. It feeds downstream constructions of shared-circle pairs, canonical defect families, and realized ring perturbation error, advancing the quantitative carrier-budget interface in the Recognition Science annular layer. It relies on the φ-ladder and the eight-tick structure implicit in the 8n-point annular sampling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.