§8 · Audit · Fresh review, re-checks · 2026-10-18T05:55:21Z
Review G2 · Review G2 · Agent 2
proved ★ key step
A fresh reviewer graded 10 steps of Agent 2: 0 errors, 2 minor, 8 correct.
Review G2.
- minor: Proposition 2.5, Lemma 2.7
- correct: Strategy 2.1, Lemma 2.2, Proposition 2.3, Lemma 2.4, Computation 2.6, Theorem 2.8, Audit 2.9, Summary 2.10
Proposition 2.5 (minor): The construction is right: π(t)=diag(α(t),1) on L_α/ker α=SL2/μ₂; for α∈Φ_x, φ_α(SL2)⊆G^{θ_x}; for xα>0, Ψ=(Φ⁺∩θ_xΦ⁺)⊔{−α,δ} and dim Lie(P_α)y=17+c_x=dim B′_y (recomputed for all 90 pairs), u(c)=x{−α}(c)x_δ(±c) is θ_x-fixed, the image of (P_α)y in PGL2 is B₂⁻ (PGL2 would force xα=±α), the ideal argument over O is right, and the proper-monomorphism argument (EGA IV 18.12.6) gives the immersion. Two defects that change no claim: (i) in step 5 the bound 'Z′=closure of B′y has fibres of dimension ≤ dim Y_x−1' is asserted without proof (it holds because Z′ is the closure of the flat irreducible (B′y)_F, or by Z′=ṡ_αZ{x′} and Lemma 2.7 item 3, non-circularly since A2-7 uses only the geometric-fibre part of A2-5); (ii) Sakellaridis writes V/Γ for a geometric quotient (p. 7 of arXiv:0905.4244v3), while A2-5 proves only that the fppf quotient of 𝒫 (resp. Y_x) by R(P_α) is P_α/B′≅ℙ¹_O (resp. Spec O); since 𝒫→P_α/B′ is fppf and 𝒫×_{ℙ¹}𝒫 is the R(P_α)-orbit relation, it is also a geometric quotient. Both lines are supplied in Audit 6.5, which I checked (its 'categorical' argument covers the geometric-quotient properties).
Lemma 2.7 (minor): Re-derived items 1–3: Z_x is B-stable (B×Z_x is flat, hence the closure of its generic fibre) and contains the section y_x; τ̃⁻¹(B) is closed with underlying set |Y_{w₀}| (every geometric point lies in some Y_v by Proposition 2.3, τ̃(Y_v) lies in the cell of v·w₀, which is B iff v=w₀), and an immersion with closed image is a closed immersion; the geometric-fibre induction through P_α·closure(Y_{x′,k}) gives exactly the recursion of Computation 2.6 item 6. Defect that changes no claim: in step 4 'P_αZ_{x′} is closed' in X_O is stated without argument (step 3 proves the analogue only on geometric fibres); it follows in one line from P_α×^B X_O≅ℙ¹_O×X_O and properness of ℙ¹_O over O, with special fibre P_α(Z_{x′}∩X_κ). Supplied in Audit 6.6 step 4, which I checked.
Builds on
- —
Built on by
- —