Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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 sum of triangularly disjoint graded ideals is disjoint from h

Statement

Every ideal J of g~(A) is Q-graded. The sum r of all ideals with J∩h=0 also has zero intersection with h, is the unique largest such ideal, and decomposes as r=r−⊕r+, where r±=r∩n~± are separate ideals.

Facts & Assumptions

Given: The triangular decomposition and an arbitrary ideal J.

[F1]

Distinct Q-degrees are distinct Cartan weights, and the zero space is the Cartan. (Contragredient algebra has a triangular decomposition).

Proof

1.1F1given

Write x∈J as ∑β∈Sxβ with finite support. Choose h∈h for which the distinct numbers β(h) are pairwise different. Such an h exists: the product of the finitely many nonzero linear polynomials β−γ is nonzero over the infinite field C, and a nonzero polynomial cannot vanish at all complex tuples (induct on the number of variables). Applying ∏γ≠β(ad⁡h−γ(h))/(β(h)−γ(h)) to x extracts xβ and keeps it in J. Thus J is graded.

2.1F1step 1.1

If J∩h=0, every vector of J has zero degree-zero component by step 1.1. The algebraic sum of all these ideals consists of finite sums of their vectors, so it also has zero degree-zero component. It is an ideal because bracketing distributes over a finite sum, and it contains every such ideal. This proves existence, maximality and uniqueness of r.

3.1F1step 2.1∎

Cartan and positive generators preserve r+. Bracketing a degree β>0 vector with fi gives degree β−αi. If this degree is zero, the result vanishes by step 2.1; if it has mixed signs it vanishes by F1; it cannot be strictly negative unless β were zero or a forbidden fractional multiple of αi. The remaining degree is positive. Hence r+ is stable under all generators and is an ideal. The sign-changing involution proves the negative assertion. The direct sum follows from F1.

Sources

Source comparison: Kleshchev, Lemma 1.3.2 and Theorem 1.3.3(v), pp.13–16.

Depends on

Used by

Dependency tree · two levels

3 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