Cost Oscillatory Branch Audit Oscillatory Not Calibrated

The oscillatory branch

The Recognition Composition Law is a functional equation that any recognition cost must obey. In log coordinates, the true cost takes the form cosh(t) - 1. A natural question is whether another function, cos(t) - 1, could also work. This oscillatory branch does satisfy the same shifted d'Alembert addition law, meaning it passes the composition requirement on positive ratios.

The framework's machine-checked library of formal theorems proves this in detail. It shows the oscillatory branch is normalized at exact balance and reciprocal-symmetric, so it meets several of the same conditions as the true cost. The key difference appears at the origin. The second log-derivative of the oscillatory branch is -1, while the true cost has second log-derivative +1. This single number, the unit calibration, is what separates the two.

Because the second log-derivative is -1, the oscillatory branch fails the unit positive calibration requirement. It also becomes negative for some positive ratios: at x = e^π, the cost equals -2. A recognition cost must be nonnegative, so this is a second, independent rejection. The theorem oscillatory_not_calibrated records the first failure, and oscillatory_not_nonnegative_on_positive records the second.

In Recognition Science, this audit sharpens an earlier claim. The composition law alone does not force the hyperbolic branch; it admits the oscillatory one. The side conditions of calibration and nonnegativity do the excluding. The main cost uniqueness theorem remains unchanged, because it includes those side conditions. What this audit adds is a precise statement of where the exclusion happens.

The practical consequence is a cleaner boundary for the framework's central result. A reader can now see that the uniqueness proof does not rest on a hidden assumption about the composition law. It rests on the explicit, checkable requirements that a cost be calibrated and nonnegative. The oscillatory branch is a concrete counterexample that passes the first test and fails the others.

/-- 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

/-- Therefore the oscillatory branch satisfies the RCL on positive ratios. -/
theorem oscillatory_satisfies_composition_law :
    SatisfiesCompositionLaw oscillatoryCost :=
  (composition_law_equiv_coshAdd oscillatoryCost).mpr
    oscillatory_cosh_add_identity

/-- Its second log-derivative at balance is `-1`, not `+1`. -/
theorem oscillatory_second_log_derivative :
    deriv (deriv (G oscillatoryCost)) 0 = -1 := by
  have hG : G oscillatoryCost = fun t => Real.cos t - 1 := by
    funext t
    exact G_oscillatoryCost t
  rw [hG]
  have hderiv : deriv (fun t : ℝ => Real.cos t - 1) =
      fun t => -Real.sin t := by
    funext t
    have hcos := Real.hasDerivAt_cos t
    have hconst : HasDerivAt (fun _ : ℝ => (1 : ℝ)) 0 t := hasDerivAt_const t 1
    simpa using (hcos.sub hconst).deriv
  have hderiv2 : deriv (fun t : ℝ => -Real.sin t) =
      fun t => -Real.cos t := by
    funext t
    have hsin := Real.hasDerivAt_sin t
    simpa using hsin.neg.deriv
  calc
    deriv (deriv (fun t : ℝ => Real.cos t - 1)) 0
        = deriv (fun t : ℝ => -Real.sin t) 0 := by rw [hderiv]
    _ = (fun t : ℝ => -Real.cos t) 0 := by rw [hderiv2]
    _ = -1 := by simp

/-- 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

/-- The oscillatory branch is negative at one nonzero log-ratio. -/
theorem oscillatory_negative_at_exp_pi :
    oscillatoryCost (Real.exp Real.pi) = -2 := by
  simp [oscillatoryCost]
  norm_num

/-- Certificate inhabitant for the oscillatory-branch audit. -/
theorem oscillatory_branch_audit : OscillatoryBranchCert where
  satisfies_rcl := oscillatory_satisfies_composition_law
  normalized := oscillatory_normalized
  reciprocal := oscillatory_reciprocal
  second_log_derivative_eq_neg_one := oscillatory_second_log_derivative
  fails_calibration := oscillatory_not_calibrated
  fails_nonnegativity := oscillatory_not_nonnegative_on_positive

What this page does not claim

The oscillatory branch is a valid recognition cost in the framework. The composition law alone is sufficient to prove the main cost uniqueness theorem. The oscillatory branch is the only alternative solution to the composition law.

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: