phiCost_add_le_phiCost_add_linear_quadratic
plain-language theorem explainer
The declaration establishes a perturbative upper bound on the φ-cost function, showing that for |u| bounded by A and perturbations ε satisfying |log φ ⋅ ε| ≤ 1 the cost at u + ε is at most the cost at u plus an explicit linear term in |ε| and quadratic term in ε. Analysts working on annular sampling and ring-cost decompositions in Recognition Science cite this to control regular-part errors when separating topological floors. The proof expands the cosh addition formula, applies sinh and cosh bounds for bounded x and |y| ≤ 1, substitutes the pre
Claim. Let φ > 1 be the golden ratio and set a = log φ. For real numbers A, u, ε with |u| ≤ A and |a ε| ≤ 1, cosh(a(u + ε)) − 1 ≤ cosh(a u) − 1 + a sinh(a A) |ε| + a² exp(a A) ε².
background
The annular J-cost framework defines phiCost(u) := cosh((log φ) u) − 1, equivalently J(φ^u) where J is the recognition cost function from the DAlembert ledger factorization. The module develops φ-weighted costs for annular sampling in the RS topological cost-covering bridge, including Jensen coercivity for nonzero winding and carrier-budget estimates for holomorphic nonvanishing carriers. Local conventions include the eight-tick phase increments and the φ-ladder mass formula. This result relies on the upstream fact one_lt_phi that 1 < φ together with standard hyperbolic inequalities for |y| ≤ 1.
proof idea
The proof is a tactic-mode calculation. It sets a = log φ, x = a u, y = a ε and proves |x| ≤ a A from |u| ≤ A and a > 0. It obtains |sinh x| ≤ sinh(a A) and cosh x + |sinh x| ≤ exp(a A). The hypothesis |y| ≤ 1 supplies the bounds cosh y − 1 ≤ y² and |sinh y| ≤ |y| + y². Expansion of phiCost(u + ε) via cosh_add produces the difference cosh x (cosh y − 1) + sinh x sinh y, which is majorized by |sinh x| |y| + (cosh x + |sinh x|) y². Substituting |y| = a |ε| and y² = a² ε² and applying the coefficient definitions, nlinarith closes the comparison.
why it matters
This supplies the basic ring-level perturbative control that feeds directly into the downstream theorem ringCost_le_topologicalFloor_add_linear_quadratic_error bounding total ring cost by the topological floor plus linear-quadratic error. It completes the annular cost decomposition that separates the topological floor from regular-part error in sampled annular meshes. Within the Recognition Science framework it supports J-cost analysis on the phi-ladder and the eight-tick octave underlying annular phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.