Cost Oscillatory Branch Audit Oscillatory Second Log Derivative

The rejected branch

The Recognition Composition Law is a rule that any cost function in the framework must obey. In log coordinates it takes the form of a d'Alembert addition law, the same identity that governs the hyperbolic cosine. The framework's unique cost function, J(x) = (x + 1/x)/2 - 1, is one solution: in log coordinates it is exactly cosh(t) - 1. The question is whether any other function could satisfy the same law.

The answer is yes, and the alternative is simple: the ordinary cosine. The function cos(t) - 1, pulled back to positive ratios as cos(log x) - 1, satisfies the same d'Alembert identity and therefore the same composition law. It is also reciprocal-symmetric and normalized at exact balance. This is not a flaw in the framework; it is a precise boundary on what the composition law alone can force. The law admits a whole family of branches, and the hyperbolic one is only selected after additional conditions are imposed.

The decisive test is the second log-derivative at the origin. For the hyperbolic branch it is +1. For the oscillatory branch it is -1, as the theorem oscillatory_second_log_derivative establishes. This single number is the unit calibration: it sets the scale of the cost function. A value of -1 instead of +1 means the function curves the wrong way, and it fails the requirement that cost be nonnegative. Indeed, the oscillatory branch takes the value -2 at the ratio exp(pi), a concrete point where cost would be negative.

In Recognition Science, this audit sharpens the earlier claim. It is not that cosine is incompatible with the composition law; it is that cosine is a valid branch of the law but is rejected by calibration and positivity. The main uniqueness theorem for the cost function remains unchanged. What the audit adds is a precise statement of why the oscillatory branch fails, and a certificate recording all six properties: it satisfies the law, is normalized, is reciprocal, has second log-derivative -1, fails calibration, and fails nonnegativity.

What the declaration does not claim is that the oscillatory branch is a viable cost function. It is not. It also does not claim that the composition law alone forces the hyperbolic branch; the audit explicitly shows the opposite. The declaration is a negative result, a boundary marker that makes the positive uniqueness theorem sharper by showing exactly which condition does the excluding work.

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

/-- 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 viable cost function. The composition law alone forces the hyperbolic branch. The audit changes the main cost uniqueness theorem.

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: