Paper A-1: Finite-Order Corrections to the GUE Spacing Ratio Mode: Surmise Hierarchy, Tail Asymptotics, and Implications for Many-Body Localisation Diagnostics

Paper A of the MNZI programme proved algebraically that the mode of the GUE consecutive level-spacing ratio distribution (ABGR surmise) is exactly (SquareRoot(5) - 1)/2, via the Buchanan-Atas perfect-square identity (1 + r + r^2)^2 - 4r(1 + r) = (r^2 + r - 1)^2. This companion paper analyses two sources of correction: (i) finite Hilbert-space corrections to the large-NH GUE distribution via the Nishigaki cancellation, and (ii) the systematic error of the 3 x 3 ABGR surmise relative to the exact distribution. We prove the following. (1) The exact curvature of the ABGR density at its mode is p''((SquareRoot(5) - 1)/2) = -5 / (16 * Z^2), derived from the Buchanan-Atas identity. (2) Large-NH corrections are O(N^-4) which is less than or equal to 10^-17 for all accessible MBL systems (L is greater than or equal to 14). (3) The N x N GUE surmise has tail asymptotics p(N)(r) proportional to r^-((N^2 - 1)/2), proved analytically from the Vandermonde structure; for N = 3 this gives r^-4 (ABGR) and for N = 5 this gives r^-12. (4) Fine-grid Gauss-Laguerre quadrature (200 points, Delta r = 0.002) locates the 5 x 5 mode at r(5) approximately equal to 0.6123, shifted below (SquareRoot(5) - 1)/2 by approximately 0.0057, confirming the perturbation formula sign. The dramatically lighter tail of the 5 x 5 surmise (r^-12 vs r^-4) provides a structural argument that the mode is a more robust GUE diagnostic than the mean for finite MBL systems, where right-tail sampling bias dominates mean-based estimators. All algebraic results are machine-verified in Lean 4 as sorry-free theorems (MNZI/GUE Spacing Ratio Mode.lean, Aristotle engine, Lean 4 v4.28.0, Mathlib v4.28.0, standard axioms only).