ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Positive roots and highest root of G_2

Example

In the $G_{2}$ model with a short simple root $α$ and a long simple root $β$ , the positive roots are $α, β, α + β, 2 α + β, 3 α + β, 3 α + 2 β,$ and the highest root is $3 α + 2 β$ .

Facts & Assumptions

Given: The $G_{2}$ model $Φ = {\pm α_{0}, \pm β_{0}, \pm (α_{0} + β_{0}), \pm (α_{0} + 2 β_{0}), \pm (α_{0} + 3 β_{0}), \pm (2 α_{0} + 3 β_{0})}$ with long root $α_{0}$ and short root $β_{0}$ . Rename the ordered base ${β_{0}, α_{0}}$ as ${α, β}$ , so $α = β_{0}$ is short and $β = α_{0}$ is long.

[L1]

In the model the roots $\pm (α_{0} + β_{0})$ , $\pm (α_{0} + 2 β_{0})$ , $\pm (α_{0} + 3 β_{0})$ , $\pm (2 α_{0} + 3 β_{0})$ occur, and the Cartan matrix relative to ${β_{0}, α_{0}}$ is the $G_{2}$ matrix (Rank-two systems A_2, B_2 and G_2, Existence of each classified root system).

[L2]

In a reduced crystallographic root system, every positive root is a nonnegative integral combination of the chosen simple roots; if the finite root system is also irreducible, it has a unique highest root (Simple roots form a signed integral basis, Existence and uniqueness of the highest root).

Verification

technique · direct

1.1

Write $α_{0}$ for the long root and $β_{0}$ for the short root of the model, so that $α = β_{0}$ , $β = α_{0}$ . The twelve roots listed in the model become, in terms of $α, β$ : $\pm α, \pm β, \pm (α + β), \pm (2 α + β), \pm (3 α + β), \pm (3 α + 2 β)$ . Hence the positive roots with respect to the base ${α, β}$ are exactly the six nonnegative combinations displayed, of heights $1, 1, 2, 3, 4, 5$ .

L1L2algebra

2.1

The root $3 α + 2 β$ has height $5$ , the largest among the positive roots, and it is the unique highest root by [L2]. Directly, each of the other five coefficient pairs $(1, 0), (0, 1), (1, 1), (2, 1), (3, 1)$ is coordinatewise at most $(3, 2)$ and is not equal to it, so every other positive root is strictly below $3 α + 2 β$ in the root order.

L2step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I, Lectures 19-24 (standard reference, not scraped)