Re-check V4 · Re-check by V4

Theorem (cited) X4.1 (holds with change): I checked every quotation and page number against the PDF (printed page = PDF page): §1.1 p.2, §1.7 pp.6–7, §2.1 p.8, Axiom 2.2.1Sakellaridis's Axiom 2.2.1, relabelled (A3a): rank-one models over O. For E6/F4 it holds over every O with 2 invertible (VI run). p.9, Axioms 2.4.1/2.4.2 pp.10–11, Statement 6.3.1 pp.44–45, Theorem 6.3.2 p.45, §7 p.58, Statement 7.1.5 and Theorem 7.2.1 p.60, §8 p.63, Example 8.0.1 and Theorem 8.0.2 p.64, Corollary 8.0.4 p.65. All are correct. One standing assumption is missing: the opening of §6 (p.41) assumes no type-N reflections, i.e. no maximal-rank pair (Y,α) of type N, and that δ(X)^{-1/2}χ̃ is unramified. Theorem 6.3.2 is proved under this assumption, which is stronger in form than (S7)'s 'no type-N spherical roots'. It holds for E6/F4 by S4-5(3), so no claim changes. Minor: virtual weighted colours are built from relevant colours, which for affine X are all colours (Lemma 7.1.1).

Audit X4.2 (holds with change): I checked the skeleton step by step against pp.17, 24–27, 44, 60–62 and 64: Axiom 2.4.2Sakellaridis's Axiom 2.4.2, relabelled (A3c): Iwahori orbits at the antidominant torus points. enters at the Iwahori normalization, Axiom 2.4.1Sakellaridis's Axiom 2.4.1, relabelled (A3b): the Cartan decomposition of X(F) into K-orbits. at Theorem 4.2.2 (x∈A_X^+), Statements 6.3.1 and 7.1.5 in the proof of Theorem 7.2.1, T∩V={0} in Theorem 8.0.2, and step 6 gives H·1_{X(o)} ↔ im r. I compared (A1)–(A5)Sakellaridis's standing assumptions for his Theorem 8.0.2 (the pages' Theorem E): (A1) a characteristic-0 field and a split group with simply connected derived group; (A2) an integral model of X with a smooth open Borel orbit and invariant measures; (A3a) rank-one models over O, (A3b) the Cartan decomposition, (A3c) Iwahori orbits (his Axioms 2.2.1, 2.4.1, 2.4.2); (A4) conditions on the spherical roots and colours; (A5) X homogeneous and affine with one open Borel orbit. in classical.html #s-hypotheses and #sakellaridis-theorem item by item. L1–L6 are correct: unramified dropped, no O-model, second clause of 2.2.1 dropped, 6.3.1 implied by Theorem 6.3.2, Theorem E combination correct, 'none verified' outdated. One loss is not recorded: (A4)(A4) Spherical roots and colours: no spherical root of type N, every Levi L_γ of a simple spherical root classical, and his Statements 6.3.1 and 7.1.5 on the spherical roots and the virtual coloured weights.'s 'no spherical root of type N' omits the §6 condition 'no type-N pair (Y,α)' (p.41). It changes no verdict.

Proposition X4.3 (holds): Recomputed in v4_e6.py and v4_labels.py (exact arithmetic, θ=-w_L with w_L from a reduced word of w0(D4D4 · Unitriangularity of the Satake traces tr V_λ in the basis T_λ = 1_{Kt^λK} (Zhu (5.6.2), Lemma 5.6.3; Lusztig, Kato).)). Results: w_Lα1=(1,1,2,2,1,0); γ1=(2,1,2,2,1,0)=2ω1-ω6, γ6=-ω1+2ω6; (α1,w_Lα1)=0; the θ-fixed roots are exactly the 24 D4D4 · Unitriangularity of the Satake traces tr V_λ in the basis T_λ = 1_{Kt^λK} (Zhu (5.6.2), Lemma 5.6.3; Lusztig, Kato). roots; no root has θβ=-β. W(E6) is transitive on all 2160 ordered orthogonal pairs, and (α1,w_Lα1) lies in the orbit of (α1,α6). Hence γ1 is normalized of type G, with no type N, and L_γ = D5D5 · Comparison with C: “IC_μ is a summand of V_λ ∗ IC_0” has the same answer over F̄_q and over C (BBD §6.1, for large p). on {1..5} and {2..6}. SNF of (1-θ) on P is [1,1], so T^θ = T_L' is connected and X(X)=Zω1⊕Zω6; Λ_S=Ze1⊕Ze6. ⟨α1^∨,ρ-ρ_L⟩=1+3=4. Θ = the 6 coroots of A2 (r=4, σ=+), Θ+ = positive coroots, and both clauses of 7.1.5 hold. The Theorem 6.11.1 / §6.19 cross-check (Spin9\Spin10, q^{-n+1}, n=5) matches p.56, (6.18). The colour count via factoriality and Helgason weights aω1+bω6 is correct.

Proposition X4.4 (holds): Re-derived. B∩H=B_L∩L^θ scheme-theoretically (θ(u)∈U_{P^-}∩P=1). L^θ = Spin8, because e1≡α2^∨+α5^∨ and e6≡α2^∨+α3^∨ mod 2, so S[2]⊆T_L'. Dimension count 42-16=26. The fibrewise-open-immersion ⇒ open immersion step (EGA IV 11.3.10, 17.9.1) is correct. The X̊=U argument via EGA IV 21.12.7 is correct (a codimension-2 component contradicts affineness of U↪X_O). Measures: 2ρ-2ρ_L vanishes on α2..α5^∨. X(O)=Kx0 by Hensel+Lang. (S10) holds since H^1(F, Borel of split Spin8)=1. Edixhoven Prop 3.4 and Steinberg Thm 8.1 are applied within their hypotheses (μ2 action with 2 invertible; semisimple automorphism of a simply connected group, on geometric fibres). Unverified and correctly labelled 'cited, not checked': (a) existence over O of an E IV involution compatible with T_O⊆B_O⊆P_O. Springer–Veldkamp ch.7 treats fields only, so the citation does not cover O; the involution Int(ṅ_L)∘τ is defined over Z (ṅ_L²=(2ρ_L^∨)(-1)=1) and acts by -w_L on T, but I could not certify that it is of type E IV. (b) The Alper result number (I expect it even gives affineness).

Proposition X4.5 (holds): Re-derived in full. (1): τ is injective, K τ(x) K depends only on Kx, Cartan decomposition. Equal labels give one K-orbit because T→A_X≅S has split-torus kernel T^θ (connected, checked), so T(O)↠A_X(O). (2) Covered labels: steps 1–6 check (P-Iwahori factorization, contraction by dominant μ, open cell U_P×A_X, L^θ=[L,L] normal). Classification of labels, proved generally and not only by search: φ(ω_i^∨)=(γ1_i,γ6_i), the μ∈Q^∨ condition is m1-m3+m5-m6≡0 (3), and the uncovered labels are exactly 3kω1^∨, 3kω6^∨ with k odd. Search to a,b≤30 agrees. Wall step: |Φ(U_Q)|=16 (α1-coefficients ≤1); ζ=(4,3,5,6,4,2), ⟨β,ζ⟩=0 on Φ_M and 3 on U_Q, θζ=-ζ; φ(μ1)=3ω1^∨, min over U_Q is 0, min over U_{P∩M} is -1. The mirror image (φ(μ1')=3ω6^∨, same bounds) holds. dim M/M^θ = 46-36 = 10. Steps 9–12 are valid: z^{-1}σ(z)∈ζ(μ2)⊆S[2]⊆H, and z^k is central in M, so (J∩M)t^{μk}x0 = z^k(J∩M)x0 ⊆ B_M(O)t^{μk}x0; ⟨β,μk⟩≥-1 sends U_{P∩M}(p) into U_{P∩M}(O); then J=U_Q(O)(J∩M)U_Q^-(p). (3): 51840/(6·192)=45. No root lies in Qω1+Qω6, so there is no type T or N (Knop's lattice transport is cited).

Gap X4.6 (fails): Fails at step 4, which leaves (E) open. (E) is settled for p odd. Delorme–Sécherre, Pacific J. Math. 251 (2011) 1–21, Theorem 1.1 (= Thm 4.13; arXiv math/0612545 Thm 0.4/4.8): for G k-split, p odd, H open in G^σ, S a σ-stable maximal k-split torus containing a maximal (σ,k)-split torus A, and K the stabilizer of a special point of the apartment of S, one has G_k = ∪{j∈J} H_k y_j S_k K, with J indexing the H_k-classes of maximal (σ,k)-split tori. For M_θ (S=T, A=our S, K=G(O)) J is a single class: any such A' is G(F)-conjugate to A (Helminck–Wang Prop 10.3), hence A' = hAh^{-1} with h∈H(F̄); splitness forces h^{-1}σ(h)∈Z_H(A)“Under (A)”: assuming all of Sakellaridis's assumptions (A1)–(A5) for X at the given p-adic place, so that his Theorem 8.0.2 applies.=L^θ=Spin8; H^1(F,Spin8)=1 (Kneser), so A' is H(F)-conjugate to A. Hence G(F)=H(F)T(F)K, i.e. G(F)=K T(F) H(F), and X(F)=K T(F)x0 since H^1(F,F4)=1. To reach A_X^+: ṅ=ṅ{α1}ṅ_{w_Lα1}∈N_G(T)(O) satisfies ṅθ(ṅ)^{-1}=e1(a)∈S(O), so ṅx0∈T(O)x0, and ṅ realizes s_{γ1} on labels; similarly for γ6. So Axiom 2.4.1Sakellaridis's Axiom 2.4.1, relabelled (A3b): the Cartan decomposition of X(F) into K-orbits. holds in full, and the step (in S4-6) that the three forms of (E) are equivalent also needed this W_X-in-K argument, which S4-6 omits. (I) is genuinely unverified. No other hypothesis is open beyond the cited inputs.

Audit X4.10 (holds): The quotation matches the opening of Part 2 on p.41 word for word. Statement 6.3.1 (types G, T split, T non-split, (U,ψ) only), Theorem 6.3.2, Theorem 7.2.1 and §8 all come after it. The E6/F4 check reduces to S4-5(3), which I re-derived before: no root lies in Q⟨ω1,ω6⟩, given Knop's transport of weight lattices (cited). The unramified-parameter clause constrains χ̃, not X. Lemma 7.1.1 is not needed, because S4-3 attaches each colour to a spherical root directly.

Proposition X4.11 (holds): I checked this independently in the 78-dimensional adjoint representation over Z, with a Frenkel–Kac Chevalley basis (v4_theta0.py; Jacobi identity checked on all basis triples). C is a Lie automorphism with C²=1 and C Ad(σ_i) C = Ad(σ_i) for every simple i. The Tits lift of w_L is the same for the reduced word and its reverse. Ad(σ_L)²=I, so σ_L² lies in Z(E6)∩T(Z) = μ3∩(2-torsion) = 1, which gives σ_L²=1 independently of the SO8/triality argument. θ0²=I. On h, θ0 = -w_L (its column on α1^∨ is -(α1+α2+2α3+2α4+α5)). θ0 fixes e_j and f_j for j=2..5, so it is trivial on Spin8. tr θ0 = 26, so dim g^θ0 = 52, and the fixed space also has dimension 52 mod 3, 5 and 7. θ0(U_P)=U_P^-. Since -w_L ∉ W, θ0 is outer, and an outer involution with fixed dimension 52 is of type E IV (F4); Steinberg gives connectedness in characteristic ≠ 2. One input is cited, not checked: the group-level Chevalley involution over Z (SGA 3 XXIII, which is standard).

Proposition X4.12 (holds): I checked each hypothesis against both the arXiv PDF (Thm 0.4/4.8, Def. 3.5, §4.4) and the Pacific version (Thm 1.1, which states that x lies in the apartment of S). The residue characteristic is odd; E6 is split and connected; θ0 is an F-involution; H = G^θ0 is connected and equal to G^σ. S is (σ,F)-split, since it is F-split with S = S^-, and maximal (θ-rank 2). T is θ-stable, maximal split, and contains S. x is the hyperspecial vertex in the apartment of T, and its stabilizer is G(O) because G is simply connected. |J|=1 re-derived: with h∈H(F̄) and both tori split, c_τ = h^{-1}τ(h) lies in Z_H(S) = L^θ = Spin8, which I verified (T^θ connected, θ0 trivial on Spin8). H^1(F,Spin8)=1 by Kneser, so A' is H(F)-conjugate to S. Then G=HTK, hence G = KTH, and X(F) = KT(F)x0 since H^1(F,F4)=1. Cited and correctly labelled: Helminck–Wang 10.3, Vust/Richardson, Kneser, Bruhat–Tits.

Proposition X4.13 (holds): Verified in v4_theta0.py for i=1,6. β_i = (1,1,2,2,1,0) resp. (0,1,1,2,2,1). All brackets between g_{±α_i} and g_{±β_i} vanish, because α_i±β_i have norm 4 and are not roots; so the root SL2's commute and σ_{α_i} commutes with θ(σ_{α_i}). Ad(θ(ṅ_i)) = Ad(ṅ_i), and the exact argument gives θ(ṅ_i)=ṅ_i, i.e. ṅ_i ∈ H(Z)∩N(T). Ad(ṅ_i) acts on h by s_{α_i}s_{β_i} and is integral. On Λ_S this is λ ↦ λ-⟨α_i,λ⟩e_i, i.e. (a,b)↦(-a,a+b) for i=1, and w commutes with θ. So K-orbits are W_X-stable on labels, and with S4-12 and S4-5(1) Axiom 2.4.1Sakellaridis's Axiom 2.4.1, relabelled (A3b): the Cartan decomposition of X(F) into K-orbits. holds in full for p odd. One caveat on statement 3: 'every hypothesis holds except (I)' is true modulo the cited inputs and the paper's 'F/Q_p unramified' simplification. The node does not repeat these, but the S4b gap field lists them.

Summary X4.14 (holds): Each status in the table matches what I verified or what is labelled cited, and (E) now has status 'proved'. I spot-checked the two inherited claims that the cell rests on, S4-7 and S4-8, numerically (v4_imr.py, v4_imr2.py, v4_conj.py), at q=2,3 over exact rationals. The r(m_μ) are W_X-invariant. Their span has codimension exactly 1 in span{M_κ : a+b ≤ N} for N=10 and 13. The functional g ↦ g(y1)-g(σy1), with y1(e1)=q^{-5} and y1(e6)=q, kills every r(m_μ) and is nonzero on M_(3,0). q^{ρ_L}y1 and q^{ρ_L}σy1 are both W(E6)-conjugate to ρ-ω4 (dominant form (6,8,11,15,11,6)). I did not re-derive S4-7's symbolic identities for every q, nor S4-8's leading-coefficient claim, which cites Sakellaridis's Remark on p.62. The cell's conditional form is correct: it rests on Axiom 2.2.1Sakellaridis's Axiom 2.2.1, relabelled (A3a): rank-one models over O. For E6/F4 it holds over every O with 2 invertible (VI run). over O plus the listed cited inputs.