G_oscillatoryCost
plain-language theorem explainer
In log coordinates the oscillatory cost branch is exactly cos t - 1. Auditors of the Recognition Composition Law cite this when comparing the hyperbolic and trigonometric solutions of the shifted d'Alembert identity. The proof is a one-line simplification unfolding the log reparametrization against the definition of the oscillatory cost on positive ratios.
Claim. For every real $t$, the log-coordinate reparametrization of the oscillatory cost equals $\cos t - 1$. Writing $G_F(t) := F(e^t)$ and taking $F(x) = \cos(\log x) - 1$ on positive $x$, one has $G_F(t) = \cos t - 1$.
background
The Recognition Composition Law (RCL) is the functional equation underlying J-cost uniqueness in Recognition Science. In log coordinates both $\cosh t - 1$ and $\cos t - 1$ obey the same shifted d'Alembert addition law, so the bare RCL does not select the hyperbolic branch.
The log reparametrization is $G_F(t) := F(e^t)$. The oscillatory cost pulls the cosine branch back to positive ratios: $F(x) = \cos(\log x) - 1$. This module records the peer-audit correction that cosine solves the RCL yet fails the RS side conditions (second log-derivative $-1$ at the origin, and negativity for nonzero small log-ratios).
The main cost uniqueness theorem is left unchanged. The paper claim is sharpened from "cos is incompatible with the RCL" to "cos is an RCL branch rejected by calibration and nonnegativity."
proof idea
One-line wrapper. The tactic simp [G, oscillatoryCost] unfolds the log reparametrization $G_F(t) = F(e^t)$ and the definition $F(x) = \cos(\log x) - 1$. Substituting $x = e^t$ yields $\cos t - 1$ immediately.
why it matters
Supplies the coordinate identity used by the two core audit lemmas in this module. Downstream, the shifted d'Alembert check for the oscillatory branch rewrites through this identity and finishes with the cosine addition formulas; the second-log-derivative lemma rewrites $G$ of the oscillatory cost as $t \mapsto \cos t - 1$ and evaluates the second derivative at the origin to $-1$ (not $+1$).
In the forcing chain this sits under T5 J-uniqueness: RCL plus unit-positive calibration and nonnegative cost force $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$. The oscillatory audit closes the gap that cosine also solves the bare composition law, so exclusion must come from the side conditions rather than from the RCL alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.