phiCost_convexOn
plain-language theorem explainer
The theorem establishes convexity of the phi-cost function over the reals. Researchers deriving Jensen bounds for annular samples in Recognition Science cite it to justify coercivity estimates on rings. The argument reduces phiCost to Jlog composed with multiplication by log phi, then invokes preservation of convexity under linear maps.
Claim. The map $umapsto cosh((log phi)cdot u)-1$ is convex on $mathbb{R}$.
background
In the annular J-cost framework, phiCost is introduced as phiCost u := cosh((log phi)cdot u)-1, equivalently J(phi^u) where J denotes the recognition cost. This construction sits inside the Jlog layer, with Jlog t := J(exp t) reducing to cosh t -1. The module uses these objects to obtain Jensen-based coercivity for nonzero winding on concentric rings and to bound annular topological cost.
proof idea
The proof defines the linear map g(x) := (log phi)cdot x. It obtains ConvexOn of Jlog from Jlog_strictConvexOn via its convexOn projection, then applies the linear-map composition theorem to Jlog circ g. A final conversion using Jlog_as_cosh and the definition of phiCost identifies the result with phiCost.
why it matters
The result supplies the convexity fact required by jensen_ring_bound, which produces the Jensen lower bound (8n)cdot phiCost of average winding for ringCost. It completes the phiCost properties block inside the annular J-cost framework, supporting the topological floor and excess decomposition. The convexity inherits directly from the cosh representation tied to J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.