Cost Oscillatory Branch Audit Oscillatory Satisfies Composition Law

The oscillatory branch

The Recognition Composition Law is a rule for how the cost of recognizing two events combines. In plain terms, it says that the cost of recognizing a pair of events is a function of the costs of recognizing each event separately. A cost function that satisfies this law is a candidate for the framework's central object. The machine-checked library of formal theorems contains a proof that a particular function, defined as cost (the price, in the framework's ledger, of recognizing a ratio between two magnitudes) equal to cos(log x) - 1, satisfies this composition law. This is the declaration oscillatory_satisfies_composition_law.

The same library also proves that this oscillatory function is normalized, meaning its cost is zero when the two magnitudes are equal, and that it is reciprocal-symmetric, meaning the cost of recognizing x is the same as the cost of recognizing 1/x. These are two of the five conditions that the unique cost function J(x) = (x + 1/x)/2 - 1 satisfies. The oscillatory branch, however, fails the other two conditions. Its second log-derivative at the balance point is -1, not +1, so it fails the unit calibration condition. And at the ratio e^π, its cost is -2, which is negative, so it fails the nonnegativity requirement for a recognition cost.

The theorem oscillatory_satisfies_composition_law therefore establishes a precise fact: the composition law alone does not force the hyperbolic branch. It leaves the main cost uniqueness theorem untouched, because that theorem uses all five conditions. What this declaration does not claim is that the oscillatory branch is a valid recognition cost. It is a branch of the composition law, but calibration and positivity reject it. The audit sharpens the earlier claim from "cos is incompatible with the law" to the correct statement: "cos is a branch, but the side conditions reject it."

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

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

What this page does not claim

The oscillatory branch is a valid recognition cost. The composition law alone forces the unique cost function J(x). The oscillatory branch is the only alternative to the hyperbolic branch.

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: