JcostC
plain-language theorem explainer
Re-export of the complex J-cost: evaluate the real cost functional on the modulus of a complex amplitude, J_ℂ(z) := J(‖z‖). Anyone working phase invariance, Born-rule uniqueness, or the T5–T7 Hamiltonian bridge cites this. Pure abbreviation of the Foundation definition; no proof content.
Claim. Define $J_{\mathbb{C}} : \mathbb{C} \to \mathbb{R}$ by $J_{\mathbb{C}}(z) := J(\|z\|)$, where $J$ is the real Recognition cost (the unique solution of the Recognition Composition Law with $J(1)=0$).
background
In Recognition Science the real cost $J$ is forced by the Recognition Composition Law and T5 uniqueness: $J(x) = (x + x^{-1})/2 - 1 = \cosh(\log x) - 1$ on $\mathbb{R}_{>0}$. Amplitudes live in $\mathbb{C}$, so the cost must be lifted off the positive reals.
The natural lift is evaluation on the Euclidean norm: only the modulus carries cost. The parent module ComplexStructureForcing develops the eight-tick cyclic shift, DFT-8 modes, and unitary evolution on $\mathbb{C}^8$; this abbreviation simply surfaces that complex cost in OperatorCore for local use.
Upstream, the Foundation definition states: "J-cost evaluated on a complex amplitude via its norm. This is the natural extension: $J_{\mathbb{C}}(z) := J(|z|)$ for $z \neq 0$."
proof idea
No proof. One-line abbreviation that aliases Foundation.ComplexStructureForcing.JcostC, itself the noncomputable definition Cost.Jcost applied to the complex modulus.
why it matters
Phase invariance of cost is the root of the Born rule in this framework: probability must be a function of modulus alone because $J$ ignores phase. The theorem jcost_phase_invariant states exactly $J_{\mathbb{C}}(z) = J_{\mathbb{C}}(z e^{i\theta})$ and cites this definition.
Downstream, the structure T5_T7_To_CanonicalHamiltonian_Bridge packages cost-phase duality ($\cosh t - 1 = J(e^{t})$), the small-deviation expansion $J(1+\varepsilon)=\varepsilon^{2}/2+O(\varepsilon^{3})$ that yields the canonical quadratic Hamiltonian, and the DFT-8 eigenvalue structure forced by the eight-tick shift (T7). Without a complex-domain $J$, those bridges cannot even be stated on amplitudes.
Landmark link: T5 J-uniqueness plus the complex lift; T7 eight-tick octave supplies the cyclic mode basis on which totalModeCost is later summed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.