oscillatory_normalized
plain-language theorem explainer
The oscillatory cost $\cos(\log x)-1$ vanishes at exact balance $x=1$, so it meets the normalization side condition of the Recognition Composition Law. Branch auditors cite this when packing the oscillatory-branch certificate. The proof is a one-line simplification of the two definitions.
Claim. The oscillatory cost $F(x)=\cos(\log x)-1$ is normalized: $F(1)=0$.
background
The module audits a peer correction to the Recognition Composition Law (RCL). In log coordinates both $\cosh t-1$ and $\cos t-1$ obey the same d'Alembert addition identity, so the RCL alone does not pick the hyperbolic branch.
Normalization is the elementary side condition $F(1)=0$: cost vanishes at exact balance (ratio one). The oscillatory cost is the pullback $F(x)=\cos(\log x)-1$ of the cosine branch to positive ratios. Related side conditions (reciprocal symmetry, second log-derivative, calibration, nonnegativity) are handled by sibling lemmas in the same audit.
Upstream, IsNormalized is exactly the predicate $F(1)=0$ from the functional-equation layer (also mirrored in the d'Alembert inevitability development).
proof idea
Term-mode one-liner: simp unfolds normalization to $F(1)=0$ and the oscillatory cost to $\cos(\log 1)-1$. Since $\log 1=0$ and $\cos 0=1$, the expression collapses to zero.
why it matters
Feeds the normalized field of the oscillatory-branch certificate (oscillatory_branch_audit), which packages RCL satisfaction, normalization, reciprocity, second-log-derivative $-1$, and calibration failure. That certificate sharpens the paper claim: cosine is an RCL branch, but unit-positive calibration and nonnegative cost reject it. The main cost uniqueness theorem (hyperbolic $J$, T5) is unchanged; only the exclusion route is corrected. Landmark link: RCL and J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.