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.
Root reflections preserve the root set
Statement
Assume the Axiom of Choice. Let be a Cartan subalgebra of a finite-dimensional complex semisimple Lie algebra with root set (Root and root space). For roots , the reflected functional (Root reflection defined by a coroot) is again a root.
Facts & Assumptions
Given: The Axiom of Choice, such and roots .
The Axiom of Choice is The Axiom of Choice; it licenses the root-string, coroot, and reflection facts in [L1] and [L2].
The set of indices with a root or zero is a nonempty interval of consecutive integers with (The root-string property).
The reflection is , and (Root reflection defined by a coroot, Cartan integers are integers, Coroot of a Lie-algebra root).
Proof
By [L1] applied to the pair there are integers with and such that for every with .
By [L2] we may rewrite , and the index satisfies because . Hence with , so by step 1.1.
Finally : if then is a scalar multiple of , so would mean ; but then and are proportional roots and the reflection of a nonzero functional is nonzero because is an involutive linear automorphism of (Root reflection defined by a coroot) with . Hence , as claimed.
Depends on
Used by
Dependency tree · two levels
16 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
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed., Chapter II (standard reference, not scraped)