Definition keyAssignmentEvaluateAmplitudeForKey
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  let kLow := kaValueStart assignment in
  let kMid := kaValueCenter assignment in
  let kTop := kaValueEnd assignment in
    match Nat.compare key kMid with
    | Eq => kaAmplitudeAtKeyCenter assignment
    | Lt =>
      match lt_dec kLow kMid with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kLow) (INR kMid) in
          interpolate
            (kaAmplitudeAtKeyStart assignment)
            (kaAmplitudeAtKeyCenter assignment)
            f
      end
    | Gt =>
      match lt_dec kMid kTop with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kMid) (INR kTop) in
          interpolate
            (kaAmplitudeAtKeyCenter assignment)
            (kaAmplitudeAtKeyEnd assignment)
            f
      end
    end.
