feat: compute dynamic subgroups from weights

[eohjelle]

This PR equips every integer weight family w : Fin N → ℤ with the represented cocharacter λ_w(t) = diag(t ^ w i) and computes its three dynamic subgroups over every commutative base ring. Prove mem_weightCocharacter_parabolic_iff: P(λ_w) consists exactly of matrices with gᵢⱼ = 0 when w i < w j, expressed by Mathlib's Matrix.BlockTriangular for the decreasing weight filtration. Compute the limit entrywise, identify the Levi with matrices preserving each weight space, and identify the dynamic unipotent subgroup with block-triangular matrices acting trivially on every associated-graded weight space.

This PR advances TauCetiRoadmap/ReductiveGroups/README.md, Layer 7, milestone “Borel subgroups, maximal tori, and their conjugacy; parabolic subgroups and Levi decomposition,” specifically its instruction to keep the dynamic approach to parabolics, Levi subgroups, and unipotent radicals as a parallel route avoiding full root data. The preceding merged step #4253 computes only diag(t, 1) in GL₂; arbitrary weights are the next critical-path calculation because they produce all standard block parabolics and their Levi decompositions in GLₙ, rather than another isolated rank-one example.

Construct the extension across t = 0 explicitly: replace the (i,j) entry by C(gᵢⱼ) X^(w i - w j) when the exponent is nonnegative and by zero otherwise. Block triangularity makes its Laurent image equal to cocharacter conjugation, and determinant invariance under diagonal conjugation proves its determinant is the constant unit C(det g). Conversely, reading the negative Laurent coefficient forces every forbidden entry to vanish, including over rings with zero divisors. This reuses Mathlib's Matrix.BlockTriangular, RingHom.map_det, polynomial-to-Laurent API, and general-linear determinant homomorphism, together with Tau Ceti's weight-torus and dynamic-subgroup infrastructure; no Mathlib source is vendored. The mathematical organization follows Kempf, Instability in invariant theory, §2, and Milne, Algebraic Groups (2017), Chapter 13, as cited in the module documentation.

Add TauCeti/Algebra/AlgebraicGroup/GeneralLinear/Dynamic/Weights.lean (546 lines). Refactor Dynamic/Basic.lean so the existing GL₂ cocharacter specializes weightCocharacter; move its two generic polynomial point-map lemmas into the new foundational module and remove the former duplicated rank-one coordinate construction. After this PR, the Layer 7 milestone still needs representability of these dynamic subgroup functors by closed subgroup schemes and Borel/maximal-torus conjugacy.

Roadmap: ReductiveGroups

🤖 Prepared with Codex

[CBirkbeck]

✅ generality — now passing on 25b62a6.

[CBirkbeck]

✅ placement — now passing on 25b62a6.

[CBirkbeck]

🟡 naming — request_changes codex/gpt-5.6-sol

One definitional restatement uses a nonstandard theorem suffix.

• TauCeti/Algebra/AlgebraicGroup/GeneralLinear/Dynamic/GL2/Basic.lean:81 — dynamicCocharacter_eq_weightCocharacter is a rfl restatement of dynamicCocharacter; the TauCeti naming addendum reserves _def for such unfolding lemmas. Fix: Rename it to dynamicCocharacter_def and update its consumers, without retaining an alias.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 44s · 244.3k in / 1.4k out tokens · reviewing this diff · rubric}

[CBirkbeck]

✅ proof-quality — now passing on 25b62a6.

[CBirkbeck]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The weight cocharacter and the parabolic, limit, Levi, and unipotent characterizations faithfully match conjugation by diag(t ^ w i), including repeated weights, zero divisors, and the degenerate N = 0 case.
✅	reuse	approved	codex/gpt-5.6-sol	The weight-cocharacter and dynamic-subgroup results are genuinely new and reuse the relevant Mathlib and TauCeti APIs. The normalization theorem is justified as a public unfolding lemma for an opaque imported definition.
✅	scope	approved	codex/gpt-5.6-sol	The arbitrary-weight GLₙ calculation directly advances Layer 7’s explicit dynamic route to parabolics, Levi subgroups, and unipotent radicals. The weight-cocharacter infrastructure, generic point-map extraction, and GL₂ specialization form one coherent generalization of the merged rank-one work.
✅	attribution	approved	codex/gpt-5.6-sol	The central informal sources are credited in the relevant module documentation, and no identifiable copied or closely adapted external formalization requires additional attribution.
✅	api-design	approved	codex/gpt-5.6-sol	The canonical public surface is appropriately scoped: construction helpers remain private, the cocharacter and dynamic subgroups have characteristic pointwise and membership lemmas, and normal-form membership results carry suitable simp annotations.
✅	generality	approved	codex/gpt-5.6-sol	The arbitrary-weight API is stated at the natural level for GL_N, with integer weights and arbitrary commutative base/value rings. The GL₂ declarations are useful Borel-specific corollaries derived from the general results rather than duplicated proofs.
✅	placement	approved	codex/gpt-5.6-sol	The new weight-cocharacter and point-map material is in its natural general-linear dynamic modules, the GL₂-specific files are consistently grouped under Dynamic/GL2, and no evidently wrong import remains.
🟡	naming	changes requested	codex/gpt-5.6-sol	One definitional restatement uses a nonstandard theorem suffix.
✅	documentation	approved	codex/gpt-5.6-sol	The new and moved substantive modules have accurate module documentation, and the added public declarations are documented consistently with their statements.
✅	proof-quality	approved	codex/gpt-5.6-sol	The proofs are robust and readable; all definitional-equality normalization via change is locally documented, and substantial arguments are appropriately factored into helper lemmas.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 25b62a6. rubrics @ f854a7e. Review spend: $9.08.}

[CBirkbeck]

✅ documentation — now passing on 25b62a6.