-- Generated by the EML-lang Lean backend
-- Source module: catenary
-- Source file:   /home/monogate/monogate/forge/examples/catenary.eml
-- Verified fns:  catenary

import MachLib.EML
import MachLib.Trig
import MachLib.Forge
import MachLib.Linarith
import MachLib.FixedPoint
import MachLib.SignTactic

open MachLib
open MachLib.Real

noncomputable def H_MIN : Real := (1 : Real)
noncomputable def H_MAX : Real := (20.0 : Real)

-- ── catenary ──

noncomputable def catenary (scale : Real) (curv : Real) (x : Real) : Real :=
  (min (max (scale * (Real.cosh (curv * x))) H_MIN) H_MAX)

theorem catenary_within_envelope (scale : Real) (curv : Real) (x : Real)
    (h_scale : (-(5.0 : Real) ≤ scale ∧ scale ≤ (5.0 : Real)))
    (h_curv : (-(0.5 : Real) ≤ curv ∧ curv ≤ (0.5 : Real)))
    (h_x : (-(4.0 : Real) ≤ x ∧ x ≤ (4.0 : Real)))
    (h_clamp1 : H_MIN ≤ H_MAX) :
    (((catenary scale curv x) >= H_MIN)) ∧ (((catenary scale curv x) <= H_MAX)) := by
  unfold catenary
  refine ⟨?_, ?_⟩ <;>
    first
    | (apply lo_le_clamp <;> (first | assumption | mach_positivity))
    | apply clamp_le_hi
    | mach_positivity
    | mach_sign
    | (apply convex_comb_le <;> assumption)
    | (apply convex_comb_ge <;> assumption)
    | (apply convex_comb3_le <;> assumption)
    | (apply convex_comb3_ge <;> assumption)
    | (apply convex_comb4_le <;> assumption)
    | (apply convex_comb4_ge <;> assumption)
    | (apply convex_comb5_le <;> assumption)
    | (apply convex_comb5_ge <;> assumption)
    | (apply convex_comb6_le <;> assumption)
    | (apply convex_comb6_ge <;> assumption)
    | rfl
    | sorry  -- out of reach; left for the prover