OscillatoryBranchCert
plain-language theorem explainer
Packages the peer-audit facts that the oscillatory cost F(x)=cos(log x)-1 obeys the Recognition Composition Law, is normalized and reciprocal, yet has second log-derivative -1 at the origin and takes negative values. Anyone citing the sharpened uniqueness claim (RCL alone does not kill cos; calibration and nonnegativity do) points here. The structure is a pure certificate type; the inhabitant is built elsewhere from the sibling lemmas.
Claim. A certificate bundling six facts about the oscillatory cost $F(x)=\cos(\log x)-1$: it satisfies the Recognition Composition Law; $F(1)=0$; it is reciprocal under $x\mapsto 1/x$; the second derivative of $G_F(t)=F(e^t)$ at $0$ equals $-1$; it fails calibration $G_F''(0)=1$; and it is not nonnegative on $(0,\infty)$.
background
The Recognition Composition Law (RCL) is the functional equation that forces the J-cost in the RS forcing chain (T5). In log coordinates $G_F(t)=F(e^t)$, both $\cosh t-1$ and $\cos t-1$ obey the same d'Alembert addition identity, so RCL alone does not select the hyperbolic branch.
Side conditions used in the cost module are: normalization $F(1)=0$; reciprocity $F(1/x)=F(x)$; calibration $G_F''(0)=1$ (equivalently $\lim_{t\to 0} 2F(e^t)/t^2=1$); and nonnegativity of $F$ on positive reals. The oscillatory candidate meets RCL, normalization, and reciprocity, but has $G''(0)=-1$ and dips below zero, so calibration and positivity reject it.
This module records that peer-audit correction: the paper claim shifts from "cos is incompatible with RCL" to "cos is an RCL branch that calibration and positivity exclude." Main cost uniqueness is unchanged.
proof idea
No proof body: this is a structure type, not a theorem. Each field is a named Prop about oscillatoryCost. The inhabitant oscillatory_branch_audit fills the fields by direct appeal to the sibling lemmas oscillatory_satisfies_composition_law, oscillatory_normalized, oscillatory_reciprocal, oscillatory_second_log_derivative, oscillatory_not_calibrated, and the nonnegativity failure lemma. The certificate is just the packaging of those six results into one audit object.
why it matters
Feeds the single downstream theorem oscillatory_branch_audit, which constructs the certificate inhabitant. That audit sharpens the uniqueness story around T5 (J-uniqueness via RCL): the hyperbolic branch $J(x)=(\cosh\circ\log)(x)-1$ remains the unique cost once calibration and nonnegativity are imposed, but the oscillatory branch is a genuine RCL solution that must be excluded by those side conditions rather than by the composition law itself.
Without this certificate, a referee could claim the paper overstated RCL's selectivity. The structure makes the corrected claim machine-checkable and keeps the main uniqueness theorem's hypotheses honest. It does not reopen the forcing chain; it documents a boundary case the chain already rules out via calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.