Cost Oscillatory Branch Audit Oscillatory Not Nonnegative On Positive

The oscillatory branch

The cost function in Recognition Science measures the price of a recognition event, a discrete record of comparison between two quantities. The framework's central theorem proves that any cost satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. That proof relies on a composition law, a forced rule for how costs combine when two comparisons happen in sequence.

A machine-checked library of formal theorems records a peer-audit correction about that composition law. The law alone does not pick out the unique cost. In logarithmic coordinates, where a ratio x becomes t = log x, the main cost J becomes cosh t - 1. But the cosine function cos t - 1 satisfies the same shifted d'Alembert addition law, the same composition rule, on positive ratios. The oscillatory branch is a genuine alternative solution to the composition law.

The framework rejects that alternative through its side conditions. At exact balance, where t = 0, the oscillatory branch has second log-derivative -1, not +1, so it fails the unit positive calibration, the requirement that the cost curve bend upward at the origin. More plainly, the branch goes negative: at the ratio x = e^π, the cost equals -2. A recognition cost that can be negative violates the nonnegative-cost requirement, the condition that recognition never pays you. The declaration oscillatory_not_nonnegative_on_positive establishes exactly this failure: it proves, by exhibiting the ratio e^π, that the oscillatory branch is not nonnegative on positive ratios.

What the declaration does not claim is that the oscillatory branch is incompatible with the composition law. The audit sharpens an older paper claim: cosine is not excluded by the composition law at all; it is excluded by calibration and positivity. The main cost uniqueness theorem, the one that forces J from the five conditions, remains unchanged, because those conditions include the calibration and nonnegativity that the oscillatory branch fails.

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

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

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

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

What this page does not claim

The oscillatory branch is incompatible with the composition law; it satisfies it. The main cost uniqueness theorem is weakened by the existence of the oscillatory branch. The oscillatory branch is nonnegative on any subset of positive ratios.

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: