phiCost_eq_Jcost
plain-language theorem explainer
The equality identifies phiCost(u) with Jcost evaluated at phi to the power u, linking the annular sampling cost directly to the core J function of Recognition Science. Researchers building the topological cost-covering bridge cite it to justify phi-weighted ring increments in J-cost calculations. The term-mode proof is a two-step rewrite that applies the Jlog_as_cosh identity followed by the exponential definition of Jlog.
Claim. For all real $u$, phiCost$(u) = $Jcost$($phi$^u)$, where phiCost$(u) := $cosh$((log phi) · u) - 1$ and Jcost$(x) = (x + x^{-1})/2 - 1$.
background
The Annular J-Cost Framework module introduces phiCost u := cosh((log φ)·u) − 1, presented as equal to J(φ^u). This object supports annular sampling on concentric rings and Jensen-based coercivity bounds of the form Θ(m² log N) for nonzero winding. The upstream Jlog definition from the Cost module states Jlog(t) := Jcost(Real.exp t), while the lemma Jlog_as_cosh proves Jlog t = Real.cosh t - 1 by direct expansion of the hyperbolic identity.
proof idea
The term-mode proof first rewrites phiCost u to Jlog (Real.log phi * u) by unfolding the phiCost definition and invoking Jlog_as_cosh. It then applies the Jlog definition together with Real.rpow_def_of_pos under the hypothesis phi_pos to reach Jcost(phi^u).
why it matters
This equality supplies the basic interface between the annular cost function and the J-cost in the Recognition Science framework, directly supporting the phi-ladder mass formula and the eight-tick octave (T7). It fills the connection step required by the module's annular topological floor and excess decomposition, though no downstream theorems yet depend on it. The result closes a foundational link in the cost-covering bridge without addressing carrier-budget construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.