-- Maclain Hunter: Coherence Score Bounds
-- Exact authored source SHA-256: a2a5c4da4b0602feec70eb02bea120499d45d7c68b837311032d8274213b8349
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

def clampNumerator (raw scale : Int) : Int := max 0 (min scale raw)
theorem finite_fixed_point_clamp_bounds (raw scale : Int) (positive : 0 < scale) :
    0 ≤ clampNumerator raw scale ∧ clampNumerator raw scale ≤ scale :=
  ⟨Int.le_max_left 0 (min scale raw),
   Int.max_le.mpr ⟨Int.le_of_lt positive, Int.min_le_left scale raw⟩⟩
#print axioms finite_fixed_point_clamp_bounds

end HunterAuthored