Alphabeta MathHow 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.
Graded poset, rank function, and rank levels
Definition
Let be a finite poset. An element is minimal if no element is strictly below it, the dual of the maximal-element notion (Maximal element and greatest element). An element covers if and there is no with . A rank function is a map such that every minimal element has rank and
whenever covers . A poset admitting a rank function is graded. Its rank- level is
Depends on
Used by
- Deleted-position labels from a fixed reduced expression, the lexicographic shelling criterion, and Möbius data Definition
- Finite lattice congruences, interval endpoints and descending rooted-chain labels Definition
- The Boolean lattice of subsets of a finite set and its rank levels Definition
- A rank-three chain labeling translated into facets of the order complex Example
- The heap of s₁s₂s₁ in type A₂: a convex alternating chain and two commutation classes Example
- The heap of s₁s₃s₂ in type A₃: a V-shaped heap with exactly two linear extensions Example
- A convex chain (in particular a covering pair) of a finite poset occurs consecutively in some linear extension Lemma
- At most one increasing chain, rank-two diamonds, the lexicographically first chain, and the local descent replacement Lemma
- Lexicographic chain shelling and the falling-chain Möbius formula Lemma
- Weak order is a partial order with finite graded intervals; covers and the inversion-set criterion Lemma
- Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound Theorem
- Deletion-labeled Bruhat intervals are lexicographically shellable, with the explicit earlier/later chain comparison Theorem
Dependency tree · one level
2 results within one dependency step 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
- M. Keller and W. T. Trotter, Applied Combinatorics, §6.2 (standard reference, not scraped)