The chapter 2 artifact writer #

The #eval below writes the committed verified_mlir/mlp_train_step.mlir from MlpRender.lean's faithful renderer when this module is elaborated. Nothing imports this file: the proofs import MlpRender, so building them never rewrites the artifact.