Cost Oscillatory Branch Audit Oscillatory Negative At Exp Pi

The oscillatory branch

In the Recognition Science framework, a cost is a function that assigns a nonnegative number to a ratio, measuring how far a recognition event is from exact balance. The framework's central theorem states that any cost satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. A peer audit found a subtle point: the composition law alone does not rule out a second, oscillatory branch. In log coordinates, this branch is exactly cos t - 1, the same shape as the hyperbolic branch but with cosine instead of hyperbolic cosine.

The declaration oscillatory_negative_at_exp_pi establishes a concrete fact about this branch: at the ratio x = e^π, the oscillatory cost equals -2. Since a cost must be nonnegative, this single value is enough to show the branch fails the nonnegativity requirement. The branch also has second log-derivative -1 at the origin, failing the unit calibration condition that the true cost satisfies with +1. These two failures, not the composition law itself, are what exclude the oscillatory branch from the uniqueness theorem.

In Recognition Science, the framework models recognition events as entries in a discrete record, or ledger, and the cost measures how expensive a recognition is. The oscillatory branch satisfies the composition law, is normalized at exact balance, and is reciprocal-symmetric, but it is not a valid cost because it goes negative. The audit sharpens the earlier claim: it is not that cosine is incompatible with the composition law, but that calibration and positivity reject it.

What the declaration does not claim is that the oscillatory branch is a viable alternative cost. It only shows one specific value where the branch is negative, which is enough to rule it out. The uniqueness theorem for the true cost J remains unchanged. The audit is a correction to the framing, not to the conclusion: the five conditions still force J, and the oscillatory branch is a counterexample to a weaker version of the claim that omits calibration and nonnegativity.

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

/-- 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 normalized at exact balance. -/
theorem oscillatory_normalized : IsNormalized oscillatoryCost := by
  simp [IsNormalized, oscillatoryCost]

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

/-- 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 alternative cost in Recognition Science; it is excluded by calibration and nonnegativity. The composition law alone forces the hyperbolic branch; the oscillatory branch satisfies the same law. The uniqueness theorem for the true cost J is weakened by this audit; it remains unchanged.

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: