IndisputableMonolith.Cost.OscillatoryBranchAudit
Audit of the oscillatory log-cost branch on positive ratios: it obeys the Recognition Composition Law and basic algebraic identities, yet fails nonnegativity and calibration. Anyone proving T5 J-uniqueness cites it to rule out the cos-type competitor to J(x)=cosh(log x)-1. The module packages explicit counterexamples and a certificate object rather than a single deep proof.
claimOn $x>0$, the oscillatory cost $J_{\mathrm{osc}}(x)=\cos(\log x)-1$ (and its $G$-form) satisfies the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, normalization $J(1)=0$, and reciprocity $J(x)=J(x^{-1})$, but is not calibrated: it takes negative values (e.g. at $x=e^{\pi}$) and is not nonnegative on $\mathbb{R}_{>0}$.
background
T5 uniqueness for the Recognition cost asks which functions on positive ratios obey the Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ together with normalization, reciprocity, and a calibration/nonnegativity demand that selects the physical yardstick. The canonical solution is $J(x)=\cosh(\log x)-1=(x+x^{-1})/2-1$.
The FunctionalEquation helpers supply the algebraic skeleton for that uniqueness argument. Beside the hyperbolic solution sits an oscillatory log branch obtained by replacing cosh with cos. Pulled back to $x>0$, it still solves the same functional equation and shares several formal identities (addition formula for cos, second logarithmic derivative, reciprocal symmetry), so it is a genuine competitor that must be excluded by the remaining axioms rather than by RCL alone.
This module isolates that competitor: definitions of the oscillatory cost and its $G$-form, the identities it does satisfy, and the concrete failures of calibration and nonnegativity.
proof idea
Definition-plus-audit structure, not a single theorem. The cost and $G$-form are introduced by direct formula. Composition-law satisfaction is reduced to the elementary cos addition identity after the log change of variables. Normalization at $1$ and reciprocity are immediate from $\cos 0=1$ and evenness of cos. Failure modes are witnessed by evaluation: at $x=e^{\pi}$ one obtains $\cos\pi-1=-2<0$, hence the map is neither nonnegative on positives nor calibrated in the T5 sense. A bundled certificate aggregates these positive and negative facts for downstream discharge.
why it matters in Recognition Science
T5 J-uniqueness is the forcing-chain step that pins the cost to $J(x)=\cosh(\log x)-1$. Uniqueness proofs must show that every RCL solution outside that family violates calibration or positivity. This module supplies the explicit oscillatory counter-model and the lemmas that separate "satisfies RCL" from "is the Recognition cost," so the main uniqueness argument can cite a named audit rather than re-derive the cos branch in-line. It does not itself close T5; it clears the competing branch so the hyperbolic solution remains the only calibrated one. No downstream modules are wired yet in the graph; the natural consumers are the T5 uniqueness assembly and any cost-axioms certificate that lists ruled-out branches.
scope and limits
- Does not prove full T5 uniqueness; only audits the oscillatory competitor.
- Does not claim every non-hyperbolic RCL solution is classified here.
- Does not establish positivity or calibration for the cosh cost; that lives elsewhere.
- Does not treat complex or non-positive ratios beyond the stated pullback.
- Does not connect numerically to alpha, masses, or eight-tick structure.
depends on (1)
declarations in this module (12)
-
def
oscillatoryCost -
theorem
G_oscillatoryCost -
theorem
oscillatory_cosh_add_identity -
theorem
oscillatory_satisfies_composition_law -
theorem
oscillatory_normalized -
theorem
oscillatory_reciprocal -
theorem
oscillatory_second_log_derivative -
theorem
oscillatory_not_calibrated -
theorem
oscillatory_negative_at_exp_pi -
theorem
oscillatory_not_nonnegative_on_positive -
structure
OscillatoryBranchCert -
theorem
oscillatory_branch_audit