cost_phase_duality
plain-language theorem explainer
Cost-phase duality equates the J-cost on the exponential ray to hyperbolic cosine: J(e^t) = cosh(t) - 1. Anyone tracing how the unique J-cost seeds a Hamiltonian or a phase axis cites this identity. The OperatorCore name is a pure re-export of the Foundation theorem, whose proof is a one-line rewrite by the known J-exp-cosh lemma.
Claim. For every real $t$, $\cosh t - 1 = J(e^{t})$, where $J$ is the Recognition cost. Equivalently, the cost along the positive real ray is the hyperbolic cosine shift of the log-coordinate.
background
Recognition Science fixes a unique nonnegative cost $J$ on the positive reals by the Recognition Composition Law and normalization; the closed form is $J(x) = (x + x^{-1})/2 - 1$, also written $\cosh(\log x) - 1$ (forcing step T5). Substituting $x = e^{t}$ therefore yields $J(e^{t}) = \cosh t - 1$ on the nose.
The surrounding module develops complex structure for the eight-tick cycle: the real log-coordinate is read as a cost axis, while the imaginary direction $it$ is read as phase, because $\cosh t = \cos(it)$ in the complex domain. The eight-tick (T7) discretizes that duality via the cyclic shift and its DFT-8 eigenmodes.
This OperatorCore declaration is only a namespace alias of the Foundation theorem of the same name; the mathematical content lives upstream.
proof idea
The underlying theorem is a one-line wrapper: rewrite the goal by the library identity Cost.Jcost_exp_cosh, which already records $J(e^{t}) = \cosh t - 1$. The OperatorCore abbrev adds no extra proof; it simply re-exports that theorem into the OperatorCore namespace for local use by Hamiltonian and bridge certificates.
why it matters
Cost-phase duality is the explicit link between the unique J-cost (T5) and the hyperbolic/trigonometric pair that separates cost from phase. Downstream, hamiltonian_emergence uses the small-deviation expansion of the same $J$ to obtain the quadratic kinetic term $J(1+\varepsilon)=\varepsilon^{2}/2+O(\varepsilon^{3})$. Both facts are fields of the bridge certificate T5_T7_To_CanonicalHamiltonian_Bridge, discharged by t5_t7_to_canonical_hamiltonian_bridge_holds, which packages cost-phase duality, the quadratic Hamiltonian remainder, and the DFT-8 eigenvalue structure forced by the eight-tick shift. In the forcing chain this is the T5+T7 route from unique cost and period-$8$ discreteness to a canonical Hamiltonian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.