phiCostLinearCoeff
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove any inequality bound on phiCost.
- Does not depend on winding number or charge.
- Does not apply when |log φ ⋅ ε| > 1.
- Does not supply the quadratic coefficient.
formal statement (Lean)
126noncomputable def phiCostLinearCoeff (A : ℝ) : ℝ :=
proof body
Definition body.
127 Real.log phi * Real.sinh (Real.log phi * A)
128
129/-- Quadratic perturbation coefficient for `phiCost` on `[-A, A]`. -/
used by (10)
-
phiCost_add_le_phiCost_add_linear_quadratic -
ringCost_le_topologicalFloor_add_linear_quadratic_error -
mkSharedCirclePair -
mkSharedCirclePair_carrier_excess_bounded -
canonicalDefectSampledFamily_ringPerturbationControl -
realizedRingPerturbationError -
phaseFamily_ringPerturbationControl -
DefectPhasePerturbationWitness -
genuineZetaDerivedPhasePerturbationWitness -
regular_perturbation_linear_term_bounded