Cost Oscillatory Branch Audit Oscillatory Branch Audit

The oscillatory branch

The Recognition Composition Law is a rule that any recognition cost must obey when two ratios are combined. In logarithmic coordinates, the standard cost function takes the form cosh(t) - 1, where t is the log of the ratio. A natural question is whether other functions might also satisfy the same rule. The oscillatory branch audit answers this with a concrete example: the function cos(t) - 1, a cosine curve shifted down by one, also satisfies the composition law exactly.

This fact is not a flaw in the framework. The audit proves that the cosine branch is reciprocal-symmetric and normalized at exact balance, meaning it treats a ratio and its reciprocal the same way and assigns zero cost when the ratio is one. But it fails two side conditions that a recognition cost must meet. Its second log-derivative at balance is -1 instead of +1, which fails the unit calibration requirement. And it takes negative values for some positive ratios, for instance at the ratio exp(π) the cost is -2, which violates the requirement that a cost be nonnegative.

In Recognition Science, the audit is a correction to an earlier claim. That claim had said the cosine branch is incompatible with the composition law. The audit shows the correct statement: the cosine branch is a valid solution of the composition law, but the calibration and positivity requirements reject it. The main cost uniqueness theorem, which says the standard cost J(x) = (x + 1/x)/2 - 1 is the only one satisfying all five conditions, remains unchanged.

For a reader, the lesson is that the composition law alone does not pin down the cost function. It takes the full set of conditions, including calibration and nonnegativity, to force the unique hyperbolic branch. The audit is a machine-checked certificate that records both the cosine branch's compliance with the composition law and its rejection by the physical side conditions.

/-- 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 audit does not prove that the composition law alone forces the standard cost function. The audit does not claim that the cosine branch is a valid recognition cost. The audit does not change the main cost uniqueness theorem, which remains proved.

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: