Coca Cola red?

Good Afternoon! I have the opportunity to do some work with a local Coca Cola distributor- so I asked for their red color definition. I’m keen to dial in the printers that will be doing their work for the most accurate reproduction of their corporate color. They gave me the red color definition in cmyk (4,100,95,0) , RGB (177, 0 25) , and hex (F40000) , with “no Pantone equivalent” With the absence of any Lab data, my thought is to just assume a CMYK source of GRACoL and derive Lab numbers from there - but surely, someone has prior experience with Coca Cola- have any of you worked with an official Lab definition of Coke red? Many thanks- Randy N