Re-check V3 · Re-check by V3

Lemma X3.1 (holds): I re-derived (a), the isomorphism (b) π_V(L0)/(L0∩V) ≅ (L0+P L0)/L0, the minors formula, the partial-sum form of dominance on Λ_S^+ (no condition on the totals, finite lower sets) and the identification φ(λ)=(λ_i−λ_{n+1−i}). I checked the formula against the label computed from A5-4's lattice definition (a saturated basis of L0∩V, without using P_x minors) at 80 random points per field over Q_2, Q_3, Q_2(√2) and F_2((t)), for n≤6 (V3/pair_v3.py). I found no defect.

Proposition X3.2 (holds): Steps 1–5 re-derived: the 2×2 block of t^λP0t^{-λ} gives ℓ(t^λx0)=φ(λ), and the minor bound val det Y_{I,J} ≥ −Σ_{i≤j}φ_i gives ℓ ≤ φ(λ) with no division by 2, so it holds in every characteristic; (iii) is Lemma A(2), whose hypotheses are met. My random checks over four fields (char 2 included) agree, with both boundary and strict cases. So does an exhaustive count of (T_λ∗φ0)(x_b), over all sublattices of cotype λ, over Z_2 and Z_3 for n=2,3,4 (V3/exhaust_v3.py): the support always lies in {b ≤ φ(λ)} and N(λ,φ(λ))=1. The method is the same minors argument as C-4; S3-2 reaches it independently through S3-1's cokernel derivation.

Proposition X3.3 (holds): Re-derived: (i) a θ fixing T_H is Ad diag(a), constant on blocks, and α²=β² forces α=−β, so no θ exists in char 2. (ii) τ(x)=ε_xε0^{-1}, L0+ε_xL0=L0+2P_xL0, and since ε_x^{-1}=ε_x the Cartan type is μ((ℓ−e)^+). (iii)/(iv) the e=0 route via λ−w0λ needs no projection and no θ-stable torus. I checked the Cartan type directly from the Smith form of g ε0 g^{-1} ε0^{-1} at 80 random points per field over Q_2, Q_3 and Q_2(√2); μ(ℓ)≠ type in 71/80 points over Q_2. I also confirmed the n=2 rows (a, max(a−e,0)) for e=0,1,2 and τ(t^{(1,0)}x0)=[[1,0],[-1,1]] over Q_2.

Theorem X3.4 (holds with change): Defect, no claim changed: step 4 (and the run's result line) say 'the statement of A5-8 holds as stated'. A5-8's statement block also says 'Input (a) holds for the three families by A5-2, A5-4 and A5-5', which is false for the pair model when e≥1. Only its displayed inclusion holds. Also, the summary's '(SG) for the involution model exactly when … odd residue characteristic' rests on S3-5 for the 'only if' part; (3) itself shows only 1_{Kx0^J}≠φ0. Re-derived: the alternating-forms input (a) and the transfer (μ(b)≤2λ at even positions plus val Pf gives μ(b)≤φ(λ)), the sphere pole-order bound and reflection matrix, the Corollary C hypotheses (i)–(v) for every F (A5-4(i) replaces Lemma A(1)'s char-0 step), and ℓ(x0^J)=(e,…,e) (checked numerically for e=0,1,2).

Proposition X3.5 (holds): Re-derived: A≅C_K by commutativity and (SG); the order ≺ refines dominance and is compatible with addition; φ is monotone, Σ_{i≤k}φ(κ)i=S_k+S{n−k}−|κ|, so top coefficients are positive and leading terms add; hence A is a domain, A^×=C^×, and only C^×φ0 generates. I recomputed the n=2 Hecke matrix over Z_2 and Z_3 from lattices: T_1 1_0=2·1_0+1_1, T_1 1_1=(q−1)1_0+1_2, T_1 1_d=q 1_{d−1}+1_{d+1}. So 1_{O_1}=(T_1−2)φ0 and x0^J∈O_1 over Q_2. The Remark is cited and I did not verify it against a source: I confirmed that the commutant of J̄ has dimension p²+(n−p)², but did not check Richardson's criterion in characteristic 2 or the Hensel/Lang step.

Correction X3.6 (holds with change): Same wording defect as S3-4: 'Its [A5-8's] statement holds' should say that its displayed inclusion holds, because A5-8's statement includes the false clause that input (a) holds for the pair model. The rest of S3-6 says this correctly. Checked: no node uses the pair-model route through (a); A5-8 is cited only by A5-5 (alternating forms), A5-10, A7-24 and C-4. A3-9 and A1-4 concern GL_4/Sp_4. The SL_2/T claim holds for every q: H_{K_SL}φ0=C[T_1²]φ0 does not contain 1_1=(T_1−2)φ0. Claim 2 (E6/F4, A6-6) is not re-derived, as labelled; I did not verify it.

Summary X3.7 (holds with change): Both verdicts are right (see inputs). Two cosmetic defects. (1) A7-25 is labelled 'holds as stated' while S3-7 asks for an addition to its corrections list. (2) The 'further path A5-8→A5-5→A5-7→A7-25' overstates the dependence: A5-7 uses A5-5 only for the central shift (A5-5 step 3) and A5-6's Lemmas 2–3, not A5-5 step 5's support bound. The conclusion is unaffected because the alternating-forms case of A5-8 is valid in every characteristic. The proposed row text is correct, and the pair-model convention matches classical.html §1 (a smooth affine O-model); X_J's non-affine special fibre is cited (Richardson), not verified by me.