Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-05
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The rho-shift intertwines the dot and ordinary Weyl actions

Statement

Let T be the translation operator on polynomial functions on h∗ defined by

(Tf)(λ):=f(λ−ρ).

Then f is invariant under the dot action of W if and only if Tf is invariant under the ordinary action of W.

Facts & Assumptions

Given: A Weyl-group element w∈W, the Weyl vector ρ, and the dot action w⋅λ:=w(λ+ρ)−ρ.

[F1]

The Weyl group acts linearly on h∗, and the dot action is defined by w⋅λ=w(λ+ρ)−ρ (Root reflections and the Weyl group action, The Weyl vector rho for a chosen positive system).

Proof

technique · direct
1.1F1givenalgebra

If f is dot-invariant, then for every w∈W and λ∈h∗ one has (Tf)(wλ)=f(wλ−ρ)=f(w⋅(λ−ρ))=f(λ−ρ)=(Tf)(λ), because [F1] gives w⋅(λ−ρ)=w((λ−ρ)+ρ)−ρ=wλ−ρ.

1.2F1givenalgebra

Conversely, if Tf is ordinarily W-invariant, then for every w∈W and λ∈h∗, [F1] gives f(w⋅λ)=f(w(λ+ρ)−ρ)=(Tf)(w(λ+ρ))=(Tf)(λ+ρ)=f(λ). So f is dot-invariant.

2.1step 1.1step 1.2∎

Thus translation by ρ converts the dot action into the ordinary Weyl action and intertwines their invariant polynomials.

Depends on

Used by

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources