sinh_mul_le_mul_sinh
plain-language theorem explainer
For 0 ≤ t ≤ 1 and x ≥ 0 the inequality sinh(t x) ≤ t sinh(x) holds. It supplies the linear scaling bound needed to control regular-factor perturbations inside meromorphic phase-charge estimates. The proof is a one-line wrapper that feeds the convexity of sinh on [0, ∞) into the definition of ConvexOn at the endpoints 0 and x.
Claim. For all real $t, x$ with $0 ≤ t ≤ 1$ and $x ≥ 0$, $sinh(t x) ≤ t sinh(x)$.
background
The Meromorphic Circle Order module factors meromorphic functions locally as (z − ρ)^n g(z) to isolate winding phase charge from the regular holomorphic factor g. Phase increments on annular rings are decomposed into a pure winding term plus a small regular perturbation ε_j; the sinh inequality bounds the linear growth of these ε_j when the refinement parameter t lies in [0,1]. Upstream convexity of sinh on the nonnegative reals is recorded as convexOn_sinh_Ici. The same module imports J-cost structures from PhiForcingDerived and ledger factorization from DAlembert to keep all estimates inside the Recognition Science annular-cost framework.
proof idea
Apply the ConvexOn property of sinh at the points x and 0 with weights t and 1-t. The resulting convex-combination inequality is sinh(t x) ≤ t sinh(x) + (1-t) sinh(0). The zero term vanishes and algebraic simplification yields the stated bound.
why it matters
The bound is invoked inside genuineZetaDerivedPhasePerturbationWitness to guarantee that linear and quadratic error terms remain summable uniformly in refinement depth. It thereby closes the perturbation-control step required for the zeta-derived phase family in the Recognition Science treatment of meromorphic order. The lemma sits between the convexity infrastructure and the downstream phase-perturbation witness, ensuring compatibility with the phi-ladder cost estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.