A machine-checked re-authoring of the ACTUS Technical Specification in Lean 4: the standard’s notations, utility functions and per-contract schedule / state-transition / payoff definitions, each linked to a formal Lean formalization, together with an embedded ACTUS Data Dictionary.