oscillatory_second_log_derivative
plain-language theorem explainer
The oscillatory cost branch has second log-derivative equal to -1 at balance, opposite the RS unit-calibration value +1. Cost-uniqueness auditors cite this to exclude the cosine solution of the Recognition Composition Law. The proof identifies the log-reparametrized cost with cos t - 1 and differentiates twice by the standard cosine/sine derivative rules.
Claim. Let $F(x)=\cos(\log x)-1$ on positive reals, and let $G_F(t)=F(e^{t})$. Then the second derivative satisfies $(G_F)''(0)=-1$.
background
The Recognition Composition Law (RCL) is a functional equation on positive-ratio costs. In log coordinates both $\cosh t-1$ and $\cos t-1$ obey the same shifted d'Alembert addition identity, so the RCL alone does not pick the hyperbolic branch.
The log-coordinate reparametrization is $G_F(t)=F(e^{t})$. The oscillatory cost is the pullback $F(x)=\cos(\log x)-1$, and the sibling identity records $G_F(t)=\cos t-1$ exactly. RS unit calibration demands that the second log-derivative at the origin equal $+1$ (matching the unique $J$-cost from the forcing chain).
This module is a peer-audit correction: cosine is an RCL solution, but side conditions (calibration and nonnegativity) reject it. The main cost-uniqueness theorem is unchanged.
proof idea
First rewrite $G$ of the oscillatory cost as the function $t\mapsto\cos t-1$ via the sibling pointwise identity, then substitute.
Compute the first derivative: $\mathrm{HasDerivAt}$ for cosine minus the constant $1$ yields $t\mapsto -\sin t$. Compute the second derivative: negate the sine derivative to get $t\mapsto -\cos t$.
A short calc chain evaluates at $0$: second derivative equals $-\cos 0=-1$. All steps are elementary real-analysis facts from Mathlib.
why it matters
This is the quantitative obstruction that kills the oscillatory branch under RS side conditions. Downstream, it is the sole arithmetic input to the non-calibration theorem: assuming unit calibration forces the second log-derivative to be $+1$, which contradicts the value $-1$ proved here (via a one-line linarith).
It is also a field of the oscillatory-branch audit certificate, which packages RCL satisfaction, normalization, reciprocity, this derivative identity, and calibration failure into a single inhabitant. That certificate sharpens the paper claim from "cosine is incompatible with the RCL" to "cosine is an RCL branch, but calibration and positivity reject it."
In the broader framework this protects T5 $J$-uniqueness: after RCL selects the d'Alembert family, the unit-calibration condition $G''(0)=+1$ isolates $J(x)=(x+x^{-1})/2-1$ and discards the oscillatory twin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.