# GL_n Weyl groups and length

**Verdict:** proved (in-run audit). Two agents, 6.7 minutes from A1 launch to root synthesis; completed 2026-10-22T16:02:28Z. This is not the full `/solve-maths-audit` pass.

## Problem

n>=1, k=algebraic closure of F_q, O=k[[t]], F=k((t)); G=GL_n, B upper triangular, I inverse image of B under GL_n(O)->GL_n(k). A permutation w acts on column vectors, t^lambda=diag(t^{lambda_i}), epsilon_i standard basis. Wtilde=Z^n semidirect S_n with product (lambda,w)(mu,v)=(lambda+w mu,wv). Qvee={lambda:sum lambda_i=0}; Waff=Qvee semidirect S_n. tau e_1=t e_n, tau e_i=e_{i-1} (i>1), kappa(t^lambda w)=sum lambda_i. Page defines ell(x)=dim IxI/I.

For every n, establish the exact relationships between S_n, Waff, Wtilde and Omega=<tau>, define the geometric and Coxeter lengths with the page's upper-Iwahori convention, and prove which distinctions are needed for its length-zero convolution argument. Give GL2 matrices distinguishing all three groups and n=1 exception. Optional explicit length formula only if checked with the page's convention.

Reader origins, quoted verbatim with IDs and source links: [A1 brief](briefs/A1.md). Comments 926c4718-f16d-40d7-8480-6704779c9df8 and 58fa329e-5138-4f85-86cd-d5c93ca5c2cf are merged into this one problem. Wording-only comments remain editorial proposals in the review.

## Criterion

A self-contained proof of the two semidirect products, strict inclusions when n>=2, sum-zero vs arbitrary translations, Omega and unique u tau^k decomposition, geometric/Coxeter length compatibility, and why translations are not all length zero. Distinguish parameterization of I double cosets from a vague claim 'indexes'. Explain length by a worked example. Proposed page edits only, do not edit mathematical HTML.

Does not count: identifying SL_n and GL_n lattices, using the wrong Iwahori convention, a numerical check in place of a proof, or asserting all translations have length zero.

## Checklist

- Upper Iwahori signs in s_0 and the geometric length formula.
- Finite S_n versus infinite affine group; sum-zero versus arbitrary cocharacters.
- Infinite-order τ, central scalar translations, and Ω versus the translation lattice.
- Geometric length versus Coxeter word length; n=1.
- Explicitly cited affine-cell and reflection-system inputs.
- Point convolution versus the separate generation theorem.

## References

- **Reader passage**: `subpages/case-study-1-ramifiedrelative/solve-maths/iwahori-two-levels/props/trace-affine.html` — Whole page; §§1,6; comments 926c4718-f16d-40d7-8480-6704779c9df8 and 58fa329e-5138-4f85-86cd-d5c93ca5c2cf.
- **HKP v3**: `subpages/case-study-1-ramifiedrelative/proof_graphs/two-definitions-iwahori/sources/haines-kottwitz-prasad-v3.pdf` — §§1.1–1.2,7.1, pp.1–2,19; upper Iwahori and affine reflection convention.
- **Zhu v2**: `subpages/case-study-1-ramifiedrelative/solve-maths/satake-two-levels/props/sources/zhu-satake-v2.pdf` — Example 1.2.9(2), p.12; Remark 2.1.22, p.29; double cosets and affine cell dimension.
- **Supporting explanation**: `subpages/misc/supporting/explainations/extended-affine-weyl-group/index.html` — Existing definitions, matrices and lattice-chain argument.
- **Original solve inputs**: `subpages/case-study-1-ramifiedrelative/solve-maths/iwahori-two-levels/returns/A5.json` — A5-1(a,b), A5-3(a); fresh original audit A8.json A8-9(1).

## Portfolio and registry

- A1, round 1: Monomial matrices, entry valuations, and affine alcoves; launched 2026-10-22T15:55:45Z. Return: [A1](returns/A1.json), eight nodes.
- A2, round 2: Independent matrix valuations and source audit; launched 2026-10-22T15:59:26Z. Return: [A2](returns/A2.json), 8 nodes. Fresh auditor received the exact solver return and checklist, with no root verdict.
- The group, length, examples and point-convolution claims are settled within this run; no blocked route remains.

## Presentation and files

[Published review](../../../proof_graphs/collaboration/reviews/2026-10-22.html#q3) · [verdict](verdict.md) · [tree](tree.md) · [machine-readable tree](tree.json) · briefs/ · returns/ · scripts/.

The returns mention assembly helpers; they are production bookkeeping, not mathematical computations, and are not part of the public computation archive. A2’s supplementary finite Coxeter enumeration is retained at `scripts/A2/check_lengths.py`; it is not the proof. A full audit has not been run, so there is no audit/ folder. The legacy token recorder does not parse Codex event records; tree.json records usage as unavailable rather than claiming zero tokens or a dollar cost.