phiCost_symm
plain-language theorem explainer
phiCost(u) equals phiCost(-u) for every real u, where phiCost is defined as cosh((log φ) u) minus one. Workers on the annular J-cost framework cite this symmetry when deriving even cost functions or applying Jensen bounds on rings. The proof is a one-line term simplification that unfolds the definition and invokes the evenness of cosh together with the sign change on the linear term.
Claim. Let $J$ be the Recognition Science cost function and let $φ$ be the golden ratio. Define $φCost(u) := J(φ^u) = cosh((log φ)·u) - 1$. Then $φCost(u) = φCost(-u)$ for all real $u$.
background
The module AnnularCost develops the φ-weighted cost function and annular sampling machinery for the RS topological cost-covering bridge. Its core object is phiCost(u) := cosh((log φ)·u) - 1, which is identical to J(φ^u). This definition sits inside a larger collection of phiCost properties that includes nonnegativity, convexity, and quadratic lower bounds, all feeding Jensen-based coercivity statements for nonzero winding on concentric rings.
proof idea
The proof is a one-line term-mode simplification. It unfolds the definition of phiCost and applies the library facts Real.cosh_neg (cosh is even) and mul_neg (the linear argument flips sign under u to -u).
why it matters
This symmetry is listed among the core phiCost properties in the module documentation for the annular J-cost framework. It supplies the even structure needed for subsequent coercivity and excess-decomposition results that close the topological cost-covering bridge. In the Recognition Science chain it is consistent with J-uniqueness (T5) and the self-similar fixed point phi (T6), ensuring the cost respects the even character induced by the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.