Jsecond_agrees
plain-language theorem explainer
On every positive real, the second complex extension of the recognition cost agrees with the forced real J-cost. Anyone citing the U(1)-extension underdetermination record needs this agreement half of the counterexample pair. The proof unfolds the extension, reduces via the real-part agreement lemma, and cancels the real-norm prefactor to 1.
Claim. For every real $x > 0$, the second complex extension $J^{(2)}(z) = \frac{(\mathrm{Re}\, z)^2}{|z|^2} J_{\mathrm{ext}}(z)$ satisfies $J^{(2)}(x) = J(x)$, where $J(x) = \frac{x + x^{-1}}{2} - 1$ is the Recognition Science cost on $\mathbb{R}_+$.
background
The Recognition Composition Law forces a unique cost on positive reals: $J(x) = (x + x^{-1})/2 - 1$ (T5, Cost.Jcost). The TurnRatioCarrier module prices the per-cycle recognition cost of the continued 8-tick cycle as $C(T) = J(\kappa T / 2\pi)$ on the real turn ratio, deliberately refusing any extension of $J$ to the returned U(1) phase.
Two artificial complex extensions are built that agree with $J$ on $\mathbb{R}+$ yet differ off it. The second is $J^{(2)}(z) = (\mathrm{Re}, z)^2 / |z|^2 \cdot J{\mathrm{ext}}(z)$, chosen so its zero set differs from the first extension. Its doc-comment: "also agrees with $J$ on $\mathbb{R}_+$, also differs off it, and has a DIFFERENT zero set."
This lemma is the agreement half for $J^{(2)}$: the prefactor collapses to 1 on positive reals, and the remaining real-part extension matches the forced cost.
proof idea
From $x > 0$ get $x \neq 0$. Unfold $J^{(2)}$. Rewrite via the sibling JextRe_agrees so the real-part factor becomes Cost.Jcost x. On a positive real embedding, Complex.normSq_ofReal and Complex.ofReal_re give prefactor $x^2/(x \cdot x)$. Field simplification yields 1; left-multiply by 1 (one_mul) to finish. Short algebraic cancellation, no analysis.
why it matters
Feeds the two kernel records that close the extend-J-to-U(1) route to Bekenstein leg B (panel 2026-07-04). Downstream u1_extension_not_unique exhibits two extensions agreeing on all of $\mathbb{R}_+$ yet disagreeing at $i$: "Any argument that extends $J$ to the phase and reads off the period is choosing its conclusion." Downstream u1_extension_zero_set_not_forced shows $J^{(2)}$ vanishes at $i \neq 1$: imposing "zero iff closure" on an extension assumes B2 rather than deriving it.
Landmark: T5 J-uniqueness is a theorem only on $\mathbb{R}_+$. Complex extensions are choices, not forced objects. That is why the module prices $C(T)$ on the real turn ratio and treats the phase-branch formula as dead in-kernel (it is nonpositive and lattice-blind at covers).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.