IndisputableMonolith.Cost.JcostLogic
Defines the canonical reciprocal cost J on the recovered real line (LogicReal), with the closed form (x+x^{-1})/2-1 and its elementary algebraic properties. Supplies the LogicReal-side composition law and the transport map that recovers the ordinary real-valued cost. Cited by anyone working the T5 uniqueness argument or the law-of-logic comparison operators on recovered reals. The module is mostly definitional plus short algebraic lemmas.
claimOn the recovered reals, the canonical reciprocal cost is $J_L(x)=\frac{x+x^{-1}}{2}-1$. It satisfies $J_L(1)=0$, $J_L(x)=J_L(x^{-1})$, $J_L\ge 0$, $J_L(x)=\frac{(x-1)^2}{2x}$ (when defined), $J_L(x)=0\Leftrightarrow x=1$, and the Recognition Composition Law. Transport through $\mathrm{toReal}$ recovers the ordinary real cost $J$.
background
Recognition Science forces a unique reciprocal cost functional $J$ (forcing step T5) with closed form $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. The Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ is the functional equation that pins $J$ down among admissible costs.
This module works on the recovered real line LogicReal rather than ordinary \mathbb{R}. Upstream, LogicRealConstants mirrors RS constants on that line and proves that LogicReal.toReal recovers the usual real constants; FunctionalEquation supplies the T5 helper lemmas on the ordinary real side. The local objects are the LogicReal cost JcostL, its elementary identities, a predicate SatisfiesCompositionLawL, and a transport map that pushes the LogicReal cost and the composition law back to ordinary reals.
proof idea
Definition module with short algebraic lemmas, not a single deep proof. JcostL is introduced by the closed-form expression on LogicReal. Unit value, reciprocity symmetry, non-negativity, the squared-defect identity, and the zero set are proved by direct rewriting and field arithmetic on LogicReal. The composition-law predicate is discharged by the same algebraic expansion used on the real side. Transport lemmas apply LogicReal.toReal (and the corresponding constant-transport facts from LogicRealConstants) to recover the ordinary real cost and the real composition law; the FunctionalEquation helpers are the real-side counterparts being mirrored.
why it matters in Recognition Science
Gives the recovered-real mirror of the T5 cost that the rest of the foundation needs when it reasons inside LogicReal rather than ordinary reals. Downstream, Foundation.LogicAsFunctionalEquationLogic imports this module to build law-of-logic comparison operators on recovered reals: it transports analytic regularity (continuity, polynomial-combiner surface) through toReal while keeping local structural fields (identity, composition) native on LogicReal. Without JcostL and compositionLawL_to_real, that mirror layer cannot state or discharge the cost side of the functional equation. In the broader forcing chain this is the LogicReal carrier for T5 J-uniqueness and the RCL, sitting under the later steps that force $\varphi$, the eight-tick octave, and $D=3$.
scope and limits
- Does not prove T5 uniqueness from scratch; it mirrors the already-known real cost on LogicReal.
- Does not address continuity or analytic regularity; those live in the downstream LogicAsFunctionalEquationLogic layer.
- Does not derive mass ladders, alpha, or dimensional forcing (T6–T8).
- Does not introduce a new cost functional beyond the canonical reciprocal J.