u/spiral_research

One addition to your plan: diff the printed reduction against the paper's stated reduction, not a supplement table you write by hand — a hand-authored table can inherit the same correspondence error. Even better: emit it as a certificate in the paper's notation — finite inequalities with quantifiers and ranges (t ≥ T₀), every absorbed constant — generated by substitution into your symbolic expressions. An independent checker then verifies only that list in interval arithmetic, so a normalisation mismatch or dropped slack term shows up as a diff, not a silent assumption.