cost_phase_duality
plain-language theorem explainer
Cost-phase duality identifies the hyperbolic excess with recognition cost: cosh(t)-1 equals J(e^t) for every real t. Citers of the T5–T7 canonical-Hamiltonian bridge and of complex-structure forcing use this identity to link the real cost axis to the imaginary phase axis. The proof is a one-line rewrite of the existing J-cost/cosh lemma.
Claim. For every real number $t$, $\cosh t - 1 = J(e^{t})$, where the recognition cost is $J(x)=(x+x^{-1})/2-1$ on positive reals.
background
The module Complex Structure Forcing shows that the eight-tick cyclic shift on the ledger cannot be diagonalized over the reals: its spectrum includes the eighth roots of unity, and $\omega^2=i$ has no real square root. Complexification, the DFT-8, and phase-invariant J-cost then force a unitary Hilbert-space structure.
Recognition cost is the unique T5 functional $J(x)=(x+x^{-1})/2-1$ on $x>0$. The upstream lemma already records the exponential form $J(e^t)=\cosh t-1$ (via the log-cosh identity). The present statement simply orients that equality as cost-phase duality: the real parameter $t$ is the cost axis, while $it$ is the phase axis that the eight-tick discretizes.
proof idea
One-line wrapper. Rewrite the goal by the upstream lemma Jcost_exp_cosh, which states $J(e^t)=\cosh t-1$ and is itself obtained from the log-as-cosh identity. Equality is symmetric, so the oriented form follows immediately.
why it matters
The identity is a named field of the T5+T7 canonical-Hamiltonian bridge certificate in the unified forcing chain: that structure packages cost-phase duality, the quadratic small-deviation expansion $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$, and the DFT-8 eigenvalue data forced by the cyclic shift. The holding theorem of the bridge cites this result directly. Downstream, the sibling Hamiltonian-emergence theorem uses the same cost calculus in the small-deviation limit, reading the quadratic piece as kinetic energy. Within the module argument, the duality underwrites phase invariance of J (cost depends on modulus, not argument) and therefore the passage from the eight-tick operator to genuine unitarity. Framework landmarks: T5 J-uniqueness, T7 eight-tick octave, and the registry gap "complex Hilbert space from cost".
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.