A7 audit notes on A8 (E6/F4 sheaf level).  Script: e6_fibre_A7.py (python3 -I).

1. Group-case check of A8-5 step 2 (literal K_N-quotient bookkeeping).
   X = H, G = H x H, K_N = K_N^H x K_N^H acting by (k1,k2).y = k1 y k2^{-1}, lambda dominant, N >> 0.
   K_N \ O_lambda = K_N\ L^+H t^lambda L^+H / K_N: right quotient fibres over Gr^lambda with fibre H_N
   (dim <2rho,lambda> + N dim H); left K_N acts on the fibre over t^lambda through the image of
   t^{-lambda} K_N t^lambda in H_N, which has dim sum_{<a,lambda>>0} <a,lambda> = <2rho,lambda>, freely.
   So dim K_N\O_lambda = N dim H = dim X_N, NOT dim X_N + delta(lambda) = N dim H + <2rho,lambda>.
   Also m does not descend to Gr x~ (K_N\L^+X) -> K_N\LX: [g,ky] -> (g k g^{-1}) g y and g K_N g^{-1}
   is only contained in K_{N-c}, c = max|<a,lambda>|; the descended map lands in K_{N-c}\LX and its
   fibres are F' times extra directions. The two literal formulas of A8-5 are each off by the same
   amount in this example, so the difference D_k - delta(mu_k') = 0 is right, but the step is only
   justified inside a consistent (renormalized, BKV / Chen-Yi A.4) dimension theory.

2. Repair: dim F_k' = 0 by a torus-fixed-point argument (no dimension theory).
   T' := (T^theta)^0 = torus of the black coroots alpha_2..alpha_5 (rank 4). T' fixes x_mu for every
   mu in Lambda_S (tau(s x_mu) = s t^mu theta(s)^{-1} = t^mu), so every fibre F_x, x = x_mu, is T'-stable.
   (a) No root of E6 vanishes on T' (script: 0 of 72; a root orthogonal to the black D4 would be
       a w1 + b w6 with a,b integers and 2(a^2+ab+b^2) = 3, impossible). Hence for generic
       eta in X_*(T') (script: eta = 49a2+9a3+34a4+41a5 works) Z_G(eta) = T and Gr^eta = Gr_T = {t^nu}.
   (b) F_k' is projective, eta-stable, contained in Gr^{lambda_k} (A8-4); its eta-fixed points are
       t^nu, nu in W lambda_k, phi(nu) = mu_k' (tau(t^{-nu} x_mu) = t^{mu - phi(nu)}, tau^{-1}(L^+G) = L^+X
       since tau is a closed immersion for p != 2). nu - lambda_k lies in ker phi = black span,
       lambda_k is orthogonal to it, |nu| = |lambda_k|, so nu = lambda_k (script: exactly 1, k = 1,3,5).
   (c) In a T-equivariant projective embedding of Gr^{<= lambda_k}, a positive-dimensional
       eta-stable closed subvariety contains >= 2 eta-fixed points (lim_0 != lim_inf of a non-fixed
       point, or a whole component of fixed points). So F_k' = {t^{lambda_k}} and E_{mu_k',n} = k for
       n = n_0, 0 otherwise, where n_0 = delta(mu_k') - D_k (= 0 with Prop. 64).

3. Normalization-free detection criterion (A8-7).
   IC_nu|O_nu = k[delta(nu)+c] for an unknown constant c. At x_mu' only nu = mu' contributes, the stalk
   is H^*(F')[D] = k[D], so E_{mu',n} = 0 for n != n_0 := delta(mu') + c - D. At x_mu the IC_{mu'}[-n_0]
   stalk lives in degrees < n_0 - delta(mu) - c = delta(mu') - delta(mu) - D (BBD 2.1.9 / Chen-Yi Cor 14(ii)).
   The top class of H^*(F)[D] sits in degree 2 dim F - D; it must come from some IC_mu[-n] as soon as
   2 dim F >= delta(mu') - delta(mu) = 8 (more generally dim F - dim F' >= codim/2). dim F >= 7.

4. Numbers (script, k = 1,3,5 and mirror k = 1,3): <2rho,lambda_k> = 32, 80, 128 = 8(a+b) of mu_k';
   |W lambda_k| = 270; F_k^{T'} = 8 points, F_k'^{T'} = 1 point; dim Z_k = 4+24+8 = 36;
   dim(Lie Z_k cap Lie P(-nu)) = 4+18+7 = 29 at all 8 fixed points; <rho_L,nu> = -3,-2,-1,0,0,1,2,3;
   no dominant lambda_k - kappa, kappa in the black cone (box c_j <= 6).