Cost Oscillatory Branch Audit Oscillatory Normalized

The oscillatory branch

The Recognition Composition Law (RCL) is the functional equation that any recognition cost must satisfy. In log coordinates, the standard cost function J(x) = (x + 1/x)/2 - 1 becomes cosh(t) - 1, where t = log x. The declaration oscillatory_normalized establishes that the alternative branch cos(t) - 1, pulled back to positive ratios as cos(log x) - 1, also satisfies the same composition law. This means the RCL alone does not single out the hyperbolic branch; it admits both the familiar cosh solution and an oscillatory cosine solution.

The oscillatory branch is normalized at exact balance: at x = 1, its value is 0, and it is reciprocal-symmetric, meaning the cost of a ratio equals the cost of its inverse. These properties mirror those of the standard cost. However, the oscillatory branch fails two side conditions that the framework imposes. Its second log-derivative at the origin is -1, not +1, so it fails the unit positive calibration requirement. It also becomes negative at nonzero log-ratios, for instance at x = exp(pi), where it equals -2, violating the nonnegative-cost requirement.

In Recognition Science, the declaration thus sharpens the earlier claim from "cos is incompatible with the RCL" to the correct statement: "cos is an RCL branch, but calibration and positivity reject it." The main cost uniqueness theorem remains unchanged. The oscillatory branch is not a valid recognition cost because it fails the physical side conditions, not because it fails the composition law.

What oscillatory_normalized does not claim is equally important. It does not assert that the oscillatory branch is a valid recognition cost; it only establishes the normalization property. It does not prove that the RCL uniquely forces the hyperbolic branch; the uniqueness theorem requires the additional calibration and nonnegativity conditions. And it does not claim that the oscillatory branch is incompatible with the RCL; the audit shows the opposite, that it satisfies the composition law.

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

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

/-- 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. The RCL alone uniquely forces the hyperbolic branch. The oscillatory branch is incompatible with the RCL.

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: