PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-26 (gpt-6-sol)

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 Weyl Jacobian is independent and invariant

Statement

Assume the Axiom of Choice (The Axiom of Choice).

The Weyl Jacobian $J (t) = \prod_{α \in Φ^{+}} ∣ 1 - α (t)^{- 1} ∣^{2}$ of a compact connected Lie group $(G, T)$ is independent of the choice of positive system $Φ^{+} \subseteq Φ (G, T)$ and invariant under the action of the Weyl group $W (G, T)$ on $T$ .

Facts & Assumptions

Given: Assume the Axiom of Choice, as required by Weyl Jacobian, and let $G$ be compact connected with maximal torus $T$ , $Φ (G, T)$ its root system, and $J$ the Weyl Jacobian for a positive system $Φ^{+}$ .

[L1]

A positive system is a set of the form $Φ^{+} (v) = {α \in Φ : (α, v) > 0}$ for a regular $v$ ; it satisfies $Φ = Φ^{+} ⊔ Φ^{-}$ with $Φ^{-} = - Φ^{+}$ , so for every root $α$ exactly one of $α, - α$ is positive (Positive systems and simple roots, Roots of a compact connected Lie group).

[L2]

For a root $α$ and $t \in T$ one has $∣ α (t) ∣ = 1$ , and the root $- α$ is the character $t \mapsto α (t)^{- 1}$ ; hence $∣ 1 - α (t)^{- 1} ∣^{2} = (1 - α (t)^{- 1}) (1 - α (t)) = 2 - α (t) - α (t)^{- 1}$ , a formula invariant under $α \mapsto - α$ (Roots of a compact connected Lie group).

[L3]

The Weyl group $W (G, T) = N_{G} (T) / T$ acts on $T$ by $(g T) \cdot t = g t g^{- 1}$ ; for $g \in N_{G} (T)$ the map $t \mapsto g t g^{- 1}$ is a Lie-group automorphism of $T$ , and $g$ acts on the root system by $Ad (g) g_{α} = g_{α \circ C_{g^{- 1}}}$ , so $α \mapsto α \circ C_{g^{- 1}}$ is a bijection of $Φ$ carrying positive systems to positive systems (Compact Weyl group, Roots of a compact connected Lie group, Conjugation and the adjoint representation of a Lie group).

Proof

technique · direct

1.1L1L2

For every $t \in T$ and every root $α$ , step [L2] says the factor attached to $α$ equals $2 - α (t) - α (t)^{- 1}$ , which is exactly the factor attached to $- α$ , since $(- α) (t) = α (t)^{- 1}$ .

2.1L1step 1.1

Consequently $\prod_{α \in Φ^{+}} ∣ 1 - α (t)^{- 1} ∣^{2} = \prod_{{α, - α}} (2 - α (t) - α (t)^{- 1})$ , the product over the unordered pairs of opposite roots, because each pair contributes one factor to the product over any positive system by [L1] and the two possible choices give the same factor by step 1.1; this product does not mention $Φ^{+}$ , so $J$ is independent of the positive system.

3.1L3step 2.1

Let $g \in N_{G} (T)$ and $t \in T$ . Then $J (g t g^{- 1}) = \prod_{α \in Φ^{+}} ∣ 1 - (α \circ C_{g}) (t)^{- 1} ∣^{2}$ , and by [L3] the set ${α \circ C_{g} : α \in Φ^{+}}$ is a positive system of $Φ$ ; step 2.1 applied to this positive system shows $J (g t g^{- 1}) = J (t)$ .

4.1L3step 3.1∎

Since $g$ was an arbitrary element of the normalizer, the invariance descends to $W (G, T) = N_{G} (T) / T$ , giving $J (w \cdot t) = J (t)$ for every $w \in W (G, T)$ .

Depends on

Used by

Orthogonality identifies the Weyl numerator Lemma
Weyl integration formula Theorem

Dependency tree · two levels

35 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

Brian Conrad and Aaron Landesman, Compact Lie Groups (standard reference, not scraped)
Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)