On attention heads and bilinear forms

This blueprint covers every numbered result of On attention heads and bilinear forms (arXiv:2609.22990v1), all of which are formalized in Lean: the lemmas, propositions and theorems of the main text and of Appendices A, B and C, together with the definitions they are stated in. Numbering follows arXiv:2609.22990v1; Theorems 1 and 2 of the introduction restate Theorems 3 and 5. Definitions numbered A1–A3 are auxiliary: they collect notation that the paper introduces in the running text. Each result has a proof outline and links to its Lean declarations; in the dependency graph, green means that the statement and its proof are both formalized. The empirical observations and the two remarks of the main text, which are stated without proof, are not formalized.