oscillatoryCost
plain-language theorem explainer
Defines the oscillatory recognition cost on positive reals by pulling back the cosine branch: cos(log x) − 1. Auditors of the Recognition Composition Law cite it as the explicit rival to the hyperbolic J-cost. The body is a one-line closed form; all subsequent lemmas only rewrite this expression in log coordinates or test side conditions.
Claim. For $x \in \mathbb{R}$ (intended on positive ratios), the oscillatory cost is $\cos(\log x) - 1$. In log coordinates $t = \log x$ this is exactly $\cos t - 1$.
background
The Recognition Composition Law (RCL) is the functional equation that forces the cost of a positive ratio. In log coordinates both $\cosh t - 1$ and $\cos t - 1$ obey the same shifted d'Alembert addition identity, so RCL alone does not pick the hyperbolic branch.
The main RS cost is $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$ (T5 J-uniqueness). Side conditions then select it: unit calibration (second log-derivative $+1$ at balance) and nonnegativity on positive ratios.
This module records the peer-audit correction that cosine is an RCL solution but fails those side conditions. The present definition is the cosine branch written on ratio space rather than on the log line.
proof idea
Pure definition: assign to each real $x$ the value $\operatorname{Real.cos}(\operatorname{Real.log} x) - 1$. No proof obligations. Downstream simp lemmas (e.g. the log-coordinate form $G$) unfold this abbreviation and apply standard cosine identities.
why it matters
Supplies the explicit counter-branch used throughout the oscillatory audit. Downstream results show it satisfies RCL and reciprocity, is normalized at exact balance, yet has second log-derivative $-1$ at the origin, is negative at $e^{\pi}$, and therefore fails calibration and nonnegativity. The certificate structure packages those facts.
Framework role: sharpens the paper claim from "cosine is incompatible with RCL" to "cosine is an RCL branch rejected by calibration and positivity," leaving T5 J-uniqueness unchanged. It is the concrete object that makes the exclusion argument checkable rather than rhetorical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.