jcost_kernelCostContent
plain-language theorem explainer
The recognition cost $J(x)=(x+x^{-1})/2-1$ satisfies the five kernel cost premises: reciprocity, normalization, the recognition composition law, unit log-curvature calibration, and continuity on positive ratios. Anyone citing the reach wall or the forcing of $J$ from kernel content needs this instance. The proof discharges each structure field by direct algebra, a known symplectic composition lemma, and elementary derivative identities for $\cosh$ and $\sinh$.
Claim. The function $J(x)=\frac{x+x^{-1}}{2}-1$ on the positive reals satisfies the kernel's cost content: it is reciprocal ($J(x)=J(x^{-1})$ for $x>0$), normalized ($J(1)=0$), obeys the recognition composition law, is calibrated so its log-coordinate second derivative at the origin equals $1$, and is continuous on $(0,\infty)$.
background
This module asks how far the recognition kernel reaches. Its answer is structural: the kernel fixes what a configuration costs, not how a configuration moves. The kernel's cost content is the five-premise package consumed by the uniqueness theorem that forces the cost to be $J$: reciprocity, normalization, the recognition composition law, unit log-curvature calibration, and continuity on positive ratios. Every field is a property of the cost of a single ratio; none quantifies over maps, sequences, or dynamics.
The recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. In the forcing chain this is the T5 unique cost. The composition law is the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Calibration means the second derivative of the log-coordinate form $G(J)(t)=J(e^t)$ at $t=0$ equals $1$, which for $J$ is the identity $\frac{d^2}{dt^2}(\cosh t-1)|_{0}=1$.
proof idea
The proof is a structure instance for the five fields of kernel cost content on $J$.
Reciprocity: unfold $J$, clear denominators, and ring-close $J(x)=J(x^{-1})$ on $x>0$. Normalization: unfold and evaluate $J(1)=0$ by norm_num. Composition: one-line citation of the existing symplectic-action lemma that $J$ satisfies the composition law.
Calibration: rewrite $G(J)=t\mapsto\cosh t-1$ via the known identity, then chain hasDerivAt facts $\frac{d}{dt}(\cosh t-1)=\sinh$ and $\frac{d}{dt}\sinh=\cosh$, and finish with $\cosh 0=1$. Continuity on $(0,\infty)$: assemble ContinuousOn for $x\mapsto\frac{x+x^{-1}}{2}-1$ from continuity of id, inversion away from zero, addition, division, and subtraction.
why it matters
This is the positive half of the reach wall. Downstream, kernel_cost_content_does_not_entail_cost_spending pairs the instance with the ledger's reciprocal involution $x\mapsto 1/x$ (strain $t\mapsto -t$), which preserves $J$ everywhere, is continuous, and never reaches the carrier from nonzero strain. The logical form no_kernel_derivation_of_residue then states that kernel cost content does not entail the C2 residue (every continuous strain map strictly spends cost off the least-cost state).
In the framework this sits under T5 $J$-uniqueness and the Recognition Composition Law: the same five premises that force $J$ are shown to be silent about motion. The module's named postulate (cost-spending substrate) is therefore an explicit extra assumption for the C2 bridge, not a kernel consequence. Without this instance the reach-wall counterexample cannot even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.