JextRe
plain-language theorem explainer
Naive real-part extension of the T5 J-cost formula to the complex plane: Re((z + 1/z)/2 − 1). Anyone building counterexample U(1) extensions that match J on the positive reals but diverge off them cites this carrier. Pure definitional abbreviation; no proof content beyond the algebraic expression and real-part projection.
Claim. For $z \in \mathbb{C}$, define $J_{\mathrm{ext}}(z) := \operatorname{Re}\bigl(\frac{z + z^{-1}}{2} - 1\bigr)$. This is the pointwise real-part projection of the algebraic T5 J-expression, evaluated on complex arguments (including where $z^{-1}$ is defined).
background
In Recognition Science the T5 cost is the unique J satisfying the Recognition Composition Law, written $J(x) = (x + x^{-1})/2 - 1$ on positive reals (equivalently $\cosh(\log x) - 1$). It vanishes only at $x = 1$ and is strictly positive elsewhere on $\mathbb{R}_{+}$.
The TurnRatioCarrier module (LEG-B panel decision) 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. The module shows that the phase branch is dead in-kernel (never strictly positive, lattice-blind on covers) and that extending $J$ off $\mathbb{R}_{+}$ is underdetermined.
This definition supplies the naive complex formula whose real part is later shown to recover $J$ on the reals, and which seeds two inequivalent extensions used in the underdetermination argument.
proof idea
Definitional. The body is the real part of the algebraic T5 expression $(z + z^{-1})/2 - 1$ evaluated at $z \in \mathbb{C}$. No lemmas, no tactics; noncomputable only because complex inversion and real-part extraction are noncomputable in the ambient library.
why it matters
Anchors the U(1)-extension underdetermination block of TurnRatioCarrier (module point 4). Downstream, JextRe_agrees proves it recovers Cost.Jcost on reals; JextRe_I evaluates it at $i$ to $-1$. The two counterexample extensions Jprime and Jsecond are built by multiplying this carrier by real prefactors that equal 1 on $\mathbb{R}{+}$ (or $\mathbb{R}$) yet differ off it, yielding distinct zero sets. Together they record that "extend $J$ off the reals" is a choice, not a forced object, killing the extend-J-to-U(1) route to B2. Ties to T5 J-uniqueness in the forcing chain: uniqueness holds on $\mathbb{R}{+}$, not automatically on $\mathbb{C}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.