JcostL
plain-language theorem explainer
Defines the canonical reciprocal cost on the recovered real line: J(x) = (x + x^{-1})/2 - 1. Anyone working the Recognition cost layer or the T5 uniqueness chain cites this as the LogicReal-native form of J. The body is a direct algebraic definition, transporting the classical formula via fromReal on the constants 2 and 1.
Claim. For $x$ on the recovered real line, the canonical reciprocal cost is $J_L(x) := \frac{x + x^{-1}}{2} - 1$, where the constants $2$ and $1$ are the images of the ordinary reals under the transport map into the recovered line.
background
Recognition Science fixes a unique nonnegative cost on positive reals by the Recognition Composition Law and mild regularity; the closed form is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced at T5 of the unified forcing chain.
This module is the transport mirror of the already-verified Mathlib-real cost core. Definitions live on LogicReal, the Cauchy completion of the recovered rationals (a thin wrapper around Bourbaki reals via the LogicRat equivalence), so that later theorems can reduce to the real surface by toReal.
fromReal embeds ordinary Mathlib reals into that recovered line. The present definition simply writes the classical J formula with those embedded constants, giving a native cost on recovered reals rather than on $\mathbb{R}$.
proof idea
Pure definitional body: no tactics. Expand as $(x + x^{-1}) / \mathrm{fromReal}(2) - \mathrm{fromReal}(1)$. Downstream simp lemmas (especially the bridge toReal_JcostL) identify this with the ordinary real cost after transport.
why it matters
This is the LogicReal-native J that the rest of Cost.JcostLogic hangs on. Immediate consumers prove unit normalization ($J_L(1)=0$), reciprocity symmetry, nonnegativity on positives, the squared form, the zero locus $J_L(x)=0 \Leftrightarrow x=1$, and the transport identity toReal(J_L x) = J(toReal x).
Those facts feed the composition-law transport (SatisfiesCompositionLawL, compositionLawL_to_real) and keep the cost layer aligned with T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Without a native definition on recovered reals, the forcing chain could not stay inside the logic-first real line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.