IndisputableMonolith.Cost.OscillatoryBranchAudit

   1import Mathlib
   2import IndisputableMonolith.Cost.FunctionalEquation
   3
   4/-!
   5# Oscillatory Branch Audit for the Recognition Composition Law
   6
   7This module records a peer-audit correction about the Recognition
   8Composition Law (RCL).  The RCL alone does not select the hyperbolic
   9branch.  In log coordinates, both
  10
  11* `cosh t - 1`, and
  12* `cos t - 1`
  13
  14satisfy the same d'Alembert addition law.  The oscillatory branch is
  15excluded by the RS side conditions: it has second log-derivative `-1` at
  16the origin and is negative for nonzero small log-ratios, so it fails the
  17unit positive calibration and the nonnegative-cost requirement.
  18
  19This leaves the main cost uniqueness theorem unchanged.  It sharpens the
  20paper claim from "cos is incompatible with the RCL" to the correct statement:
  21"cos is an RCL branch, but calibration/positivity reject it."
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Cost
  26namespace OscillatoryBranchAudit
  27
  28open FunctionalEquation
  29
  30noncomputable section
  31
  32/-- The oscillatory log branch pulled back to positive ratios. -/
  33noncomputable def oscillatoryCost (x : ℝ) : ℝ :=
  34  Real.cos (Real.log x) - 1
  35
  36/-- In log coordinates the oscillatory branch is exactly `cos t - 1`. -/
  37@[simp] theorem G_oscillatoryCost (t : ℝ) :
  38    G oscillatoryCost t = Real.cos t - 1 := by
  39  simp [G, oscillatoryCost]
  40
  41/-- The oscillatory branch satisfies the same shifted d'Alembert identity as `J`. -/
  42theorem oscillatory_cosh_add_identity :
  43    CoshAddIdentity oscillatoryCost := by
  44  intro t u
  45  simp only [G_oscillatoryCost]
  46  rw [Real.cos_add, Real.cos_sub]
  47  ring
  48
  49/-- Therefore the oscillatory branch satisfies the RCL on positive ratios. -/
  50theorem oscillatory_satisfies_composition_law :
  51    SatisfiesCompositionLaw oscillatoryCost :=
  52  (composition_law_equiv_coshAdd oscillatoryCost).mpr
  53    oscillatory_cosh_add_identity
  54
  55/-- The oscillatory branch is normalized at exact balance. -/
  56theorem oscillatory_normalized : IsNormalized oscillatoryCost := by
  57  simp [IsNormalized, oscillatoryCost]
  58
  59/-- The oscillatory branch is reciprocal-symmetric. -/
  60theorem oscillatory_reciprocal : IsReciprocalCost oscillatoryCost := by
  61  intro x hx
  62  have hlog : Real.log x⁻¹ = - Real.log x := by
  63    simp [Real.log_inv]
  64  simp [oscillatoryCost, hlog, Real.cos_neg]
  65
  66/-- Its second log-derivative at balance is `-1`, not `+1`. -/
  67theorem oscillatory_second_log_derivative :
  68    deriv (deriv (G oscillatoryCost)) 0 = -1 := by
  69  have hG : G oscillatoryCost = fun t => Real.cos t - 1 := by
  70    funext t
  71    exact G_oscillatoryCost t
  72  rw [hG]
  73  have hderiv : deriv (fun t : ℝ => Real.cos t - 1) =
  74      fun t => -Real.sin t := by
  75    funext t
  76    have hcos := Real.hasDerivAt_cos t
  77    have hconst : HasDerivAt (fun _ : ℝ => (1 : ℝ)) 0 t := hasDerivAt_const t 1
  78    simpa using (hcos.sub hconst).deriv
  79  have hderiv2 : deriv (fun t : ℝ => -Real.sin t) =
  80      fun t => -Real.cos t := by
  81    funext t
  82    have hsin := Real.hasDerivAt_sin t
  83    simpa using hsin.neg.deriv
  84  calc
  85    deriv (deriv (fun t : ℝ => Real.cos t - 1)) 0
  86        = deriv (fun t : ℝ => -Real.sin t) 0 := by rw [hderiv]
  87    _ = (fun t : ℝ => -Real.cos t) 0 := by rw [hderiv2]
  88    _ = -1 := by simp
  89
  90/-- Hence it fails the RS unit calibration. -/
  91theorem oscillatory_not_calibrated :
  92    ¬ IsCalibrated oscillatoryCost := by
  93  intro h
  94  have hneg := oscillatory_second_log_derivative
  95  rw [IsCalibrated] at h
  96  linarith
  97
  98/-- The oscillatory branch is negative at one nonzero log-ratio. -/
  99theorem oscillatory_negative_at_exp_pi :
 100    oscillatoryCost (Real.exp Real.pi) = -2 := by
 101  simp [oscillatoryCost]
 102  norm_num
 103
 104/-- Consequently it is not a nonnegative recognition cost on positive ratios. -/
 105theorem oscillatory_not_nonnegative_on_positive :
 106    ¬ (∀ x : ℝ, 0 < x → 0 ≤ oscillatoryCost x) := by
 107  intro h
 108  have hpos : 0 < Real.exp Real.pi := Real.exp_pos Real.pi
 109  have hnonneg := h (Real.exp Real.pi) hpos
 110  rw [oscillatory_negative_at_exp_pi] at hnonneg
 111  norm_num at hnonneg
 112
 113/-- Audit summary: RCL admits the oscillatory branch, but RS calibration and
 114nonnegativity reject it. -/
 115structure OscillatoryBranchCert where
 116  satisfies_rcl : SatisfiesCompositionLaw oscillatoryCost
 117  normalized : IsNormalized oscillatoryCost
 118  reciprocal : IsReciprocalCost oscillatoryCost
 119  second_log_derivative_eq_neg_one :
 120    deriv (deriv (G oscillatoryCost)) 0 = -1
 121  fails_calibration : ¬ IsCalibrated oscillatoryCost
 122  fails_nonnegativity :
 123    ¬ (∀ x : ℝ, 0 < x → 0 ≤ oscillatoryCost x)
 124
 125/-- Certificate inhabitant for the oscillatory-branch audit. -/
 126theorem oscillatory_branch_audit : OscillatoryBranchCert where
 127  satisfies_rcl := oscillatory_satisfies_composition_law
 128  normalized := oscillatory_normalized
 129  reciprocal := oscillatory_reciprocal
 130  second_log_derivative_eq_neg_one := oscillatory_second_log_derivative
 131  fails_calibration := oscillatory_not_calibrated
 132  fails_nonnegativity := oscillatory_not_nonnegative_on_positive
 133
 134end
 135
 136end OscillatoryBranchAudit
 137end Cost
 138end IndisputableMonolith
 139