The aim of this blueprint is to “sharpen” the statement of the Haag Kastler axioms [Haag and Kastler] for Lean formalization. As originally presented they were revolutionary. However, several small details were left under-specified. This blueprint will hopefully clarify some of these details.