phiCostQuadraticCoeff
plain-language theorem explainer
phiCostQuadraticCoeff supplies the quadratic error coefficient in the second-order bound for the J-cost function phiCost on a compact interval [-A, A]. Researchers formalizing annular ring costs and carrier budget comparisons cite it to control perturbation excesses above the topological floor. The definition is the direct product of the base scaling kappa with the exponential of log phi times A, extracted from the Taylor remainder of the hyperbolic cosine expression.
Claim. The quadratic coefficient in the perturbative expansion of the cost function on the interval $[-A, A]$ is given by $kappacdot exp((log phi) A)$, where $kappa$ is the phi-ladder conductivity factor.
background
The annular J-cost framework defines the cost function as phiCost u := cosh((log phi) u) - 1, equivalent to the J-function applied to phi^u. This function obeys the Recognition Composition Law and yields coercive costs for nonzero winding on concentric rings. Annular sampling decomposes the total cost into a topological floor from the winding number plus linear and quadratic errors from regular perturbations.
proof idea
The definition is a direct algebraic expression multiplying kappa by the exponential of (log phi) times A. It follows immediately from evaluating the second derivative of cosh at the boundary of the perturbation interval, scaled by the base factor kappa.
why it matters
This coefficient enters the upper bound theorems for phiCost under small perturbations and the ring cost estimates that isolate the topological floor. It supports the excess bounds for shared circle pairs and the perturbation control for defect sampled families. In the Recognition Science chain it advances the quantitative trace construction for Axiom 2 by providing the explicit quadratic term in the annular decomposition, consistent with the J-uniqueness and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.