On attention heads and bilinear forms

This blueprint covers the results of On attention heads and bilinear forms that are formalized in Lean: Appendices A, B and C, together with Definition 6 and Theorem 4 of the main text. Numbering follows the paper. 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 remaining main-text theorems, including the accumulation theorem that applies Lemma 6, are not formalized.