Cost Oscillatory Branch Audit Oscillatory Cosh Add Identity

The oscillatory branch

The Recognition Composition Law is a functional equation that a cost function must satisfy. In log coordinates, the standard cost function J takes the form cosh t minus 1. The declaration oscillatory_cosh_add_identity proves that another function, cos t minus 1, satisfies the exact same shifted d'Alembert addition law. This means the composition law alone does not single out the hyperbolic branch; a cosine-based branch is also a valid solution.

This oscillatory branch, pulled back to positive ratios, is cos(log x) minus 1. It is reciprocal-symmetric and normalized at exact balance, matching two of the side conditions. But it fails the remaining ones. Its second log-derivative at the origin is -1, not +1, so it fails the unit positive calibration. It also takes negative values, for instance -2 at x = e^π, so it fails the nonnegative-cost requirement. The audit certificate bundles these facts: the branch satisfies the composition law, but calibration and positivity reject it.

In Recognition Science, this correction sharpens an earlier paper claim. The accurate statement is not that cosine is incompatible with the composition law, but that cosine is a branch of it, and the side conditions do the rejecting. The main cost uniqueness theorem stands unchanged, because its proof relies on those side conditions. The oscillatory branch remains a mathematical curiosity, a solution family that the framework's physical requirements exclude.

/-- The oscillatory branch satisfies the same shifted d'Alembert identity as `J`. -/
theorem oscillatory_cosh_add_identity :
    CoshAddIdentity oscillatoryCost := by
  intro t u
  simp only [G_oscillatoryCost]
  rw [Real.cos_add, Real.cos_sub]
  ring

/-- The oscillatory branch is reciprocal-symmetric. -/
theorem oscillatory_reciprocal : IsReciprocalCost oscillatoryCost := by
  intro x hx
  have hlog : Real.log x⁻¹ = - Real.log x := by
    simp [Real.log_inv]
  simp [oscillatoryCost, hlog, Real.cos_neg]

/-- The oscillatory branch is normalized at exact balance. -/
theorem oscillatory_normalized : IsNormalized oscillatoryCost := by
  simp [IsNormalized, oscillatoryCost]

/-- Hence it fails the RS unit calibration. -/
theorem oscillatory_not_calibrated :
    ¬ IsCalibrated oscillatoryCost := by
  intro h
  have hneg := oscillatory_second_log_derivative
  rw [IsCalibrated] at h
  linarith

/-- Consequently it is not a nonnegative recognition cost on positive ratios. -/
theorem oscillatory_not_nonnegative_on_positive :
    ¬ (∀ x : ℝ, 0 < x → 0 ≤ oscillatoryCost x) := by
  intro h
  have hpos : 0 < Real.exp Real.pi := Real.exp_pos Real.pi
  have hnonneg := h (Real.exp Real.pi) hpos
  rw [oscillatory_negative_at_exp_pi] at hnonneg
  norm_num at hnonneg

What this page does not claim

The oscillatory branch is a valid recognition cost in the framework. The composition law alone forces the hyperbolic branch. The main cost uniqueness theorem is invalidated by the existence of the oscillatory branch.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/OscillatoryBranchAudit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: