Identifiability of Deep Normalized Attention: Or, Machine Verified Proofs for Neuroalgebraic Geometry

Does the function realized by a deep normalized self-attention network determine its virtual weights? Not for every positive injective scalar normalizer: we construct a Borel normalizer for which every point of an explicit open dense set of scalar depth-two parameters has a distinct partner with exactly the same realization. For exponential softmax, however, the virtual weights are uniquely determined at every finite depth and every token count $t\ge2$, provided that the final linear map is nonzero and the score matrices before the final attention layer are not skew-symmetric; no corresponding assumption is made on any other point in the fiber. The arbitrary-depth proof, developed with Codex and formally verified in Lean~4, uses inputs with one distinguished token and repeated copies of another: a nonzero directional component of the next unknown score discrepancy appears between the two networks at second order, while the within-network token-class gap is only third order, so later layers cannot cancel the leading discrepancy.