phiCost_zero
plain-language theorem explainer
phiCost vanishes at the origin. Workers on annular J-cost bounds cite this base case when establishing zero topological floor for zero-winding traces. The argument reduces directly via the definition of phiCost and the identity cosh 0 = 1.
Claim. Let $f(u) := cosh((log phi) u) - 1$. Then $f(0) = 0$.
background
The module develops the annular J-cost framework for the RS topological cost-covering bridge. Core object is the function defined by $f(u) = cosh((log phi) u) - 1$, which equals J(phi^u) by the cosh representation of J. This sits inside the phi-weighted cost function and annular sampling machinery, with Jensen-based coercivity and carrier budget results already formalized.
proof idea
The proof is a one-line wrapper that applies simplification using the definition of phiCost together with the identity Real.cosh 0 = 1.
why it matters
This result feeds the proof that the annular topological floor vanishes for zero winding on every ring and the excess decomposition for sampled traces. It closes the base case in the annular layer, consistent with J-uniqueness T5 and the self-similar fixed point phi in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.