Exact proof index
Exact RT-LIE proof providers, with their field, dimension and other hypotheses. Four geometric results are conditional on the inputs stated in their entries. Each source revision is bound by SHA-256.
| Result | Conditions | Source SHA-256 |
|---|---|---|
| Lemma 0.3 (Complex square roots). | Complex numbers over the complete ordered real field. Includes zero; real-square-root argument supplied. | E299AAD8F0CA2ACBC66871649E9B6F4DB6706802454F37DA9A851D3D79220633 |
| Lemma 0.2 (Quotient algebras and factorization). | Unital associative algebra, two-sided ideal, unital algebra maps. Zero quotient allowed. | E299AAD8F0CA2ACBC66871649E9B6F4DB6706802454F37DA9A851D3D79220633 |
| Lemma 0.1 (Rank–nullity). | Linear map over any field, finite-dimensional domain; target arbitrary. | E299AAD8F0CA2ACBC66871649E9B6F4DB6706802454F37DA9A851D3D79220633 |
| Theorem 6.2 (Poincaré–Birkhoff–Witt). | Alternating Lie algebra over any field; given totally ordered basis of arbitrary cardinality. Ordered monomials form a basis; associated graded is the symmetric algebra. | E299AAD8F0CA2ACBC66871649E9B6F4DB6706802454F37DA9A851D3D79220633 |
| Theorem 5.1. | Finite-dimensional semisimple Lie algebra over any characteristic-zero field; every derivation is inner. | 2EABD41F1333C7D8E5CBEC9ACFF7F77771B659C2E478F5F6C6E8800D6F5C5833 |
| Theorem 3.3 (Weyl, algebraically closed case). | Finite-dimensional semisimple complex Lie algebra and finite-dimensional complex module. | 2DE5D9C09CE2F44702373DCA83A62E3E35FB1C1003C144B8DC0F6438F0348E02 |
| Theorem 4.1 (Weyl over an arbitrary field). | Finite-dimensional semisimple Lie algebra and finite-dimensional module over any characteristic-zero field. | 2DE5D9C09CE2F44702373DCA83A62E3E35FB1C1003C144B8DC0F6438F0348E02 |
| Theorem 2.1. | Finite-dimensional complex sl2 modules; irreducible highest weights n are nonnegative integers. | 4230060F402F76CADA87DF70EAA9938E3EE8041930D425758D9CF7B56B9D1F8A |
| Proposition 2.2. | Polynomial Sym^n action of SL2 over every commutative ring; differential irreducibility asserted only over characteristic-zero fields. | 4230060F402F76CADA87DF70EAA9938E3EE8041930D425758D9CF7B56B9D1F8A |
| Theorem 4.1 (Whitehead). | Finite-dimensional semisimple Lie algebra and finite-dimensional module over any characteristic-zero field; H1 and H2 vanish. | 47E54D42F3105E00FD33A5D60321CDB0ED5799E08CF0CFE6305B908EAC8D0921 |
| Proposition 2.2. | H1 identifies derivations modulo inner derivations for adjoint coefficients; combined with Theorem4.1 gives all derivations inner. | 47E54D42F3105E00FD33A5D60321CDB0ED5799E08CF0CFE6305B908EAC8D0921 |
| Theorem 7.1 (Levi conjugacy). | Any two Levi subalgebras of a finite-dimensional Lie algebra over any characteristic-zero field are conjugate by one exp(ad a), with a in [g,rad g], hence in the nilradical; all constructions occur over the original field. | 47E54D42F3105E00FD33A5D60321CDB0ED5799E08CF0CFE6305B908EAC8D0921 |
| Theorem 7.2 (Ado). | Every finite-dimensional Lie algebra over any characteristic-zero field has a faithful finite-dimensional representation over that field; finite algebraic extension and restriction of scalars supply descent. | 47E54D42F3105E00FD33A5D60321CDB0ED5799E08CF0CFE6305B908EAC8D0921 |
| Theorem 6.1 (Serre). | Cartan matrix of finite type, complex field; arbitrary rank and number of connected components; column-coroot a_ij=alpha_i(h_j). | 39879340D7518601AA2EBC2CA983BE6273FA2B1335190C82C6821A68DCFAC2B3 |
| Corollary 6.3. | Same finite-type presentation over Q and characteristic-zero extension fields; split semisimplicity, r+|Phi| dimensions and exact scalar extension. | 39879340D7518601AA2EBC2CA983BE6273FA2B1335190C82C6821A68DCFAC2B3 |
| Theorem 9.1. | Complex semisimple Lie algebra of arbitrary finite rank and any number of components; directed diagram group includes isomorphic component permutations. Uses the finite fundamental modules proved in 14. | 39879340D7518601AA2EBC2CA983BE6273FA2B1335190C82C6821A68DCFAC2B3 |
| Theorem 5.1 (integral root basis). | Complex semisimple Lie algebra with a chosen Cartan and base; simultaneous integral root basis with opposite normalization, all ±(p+1) constants and N(-alpha,-beta)=-N(alpha,beta). Includes the exhaustive exact rank-at-most-three certificate. | 4004A9253BE6341D2D7E09BC15A1D8259D7EE8F7005D0198345DBEF0F5D1DB3F |
| Theorem 3.1. | Any complex highest weight; unique simple highest-weight quotient of the Verma module. | 22C17766D12E6032AF414DC41F7E6C21972729FCD5F1D8A4607230D4EC60BABD |
| Theorem 4.1 (highest-weight classification). | Finite-dimensional iff dominant integral; classification of finite-dimensional simple complex modules. | 22C17766D12E6032AF414DC41F7E6C21972729FCD5F1D8A4607230D4EC60BABD |
| Corollary 4.4. | Dominant integral highest weight; simple module equals the finite integrable cyclic presentation. | 22C17766D12E6032AF414DC41F7E6C21972729FCD5F1D8A4607230D4EC60BABD |
| Highest-weight rational forms, Section4.5 | Section4.5 supplies its rational form and any characteristic-zero extension. | 22C17766D12E6032AF414DC41F7E6C21972729FCD5F1D8A4607230D4EC60BABD |
| Theorem 9.1. | Finite-dimensional complex semisimple Lie algebra of rank r, including products and zero: its Cartan Weyl invariant ring has r homogeneous algebraically independent polynomial generators. Formal completion proof; no general complex reflection-group CST theorem asserted. | 252271B819FAC2E0A9CD8A5468CFEA12B3D3593587570412098D3F81D4C1BCEE |
| Theorem 2.3. | Any two negative-Killing real forms of a finite-dimensional complex semisimple Lie algebra, any rank and components, are inner-conjugate. | E3B897CBFC079A4E2AE987D725311105853B92A7F9AF46F09E36255FCCBC1A39 |
| Theorem 3.4. | Compact connected finite-dimensional Lie group with semisimple real Lie algebra: finite fundamental group and compact connected simply connected cover. | E3B897CBFC079A4E2AE987D725311105853B92A7F9AF46F09E36255FCCBC1A39 |
| Theorem 8.1 (Cartan-involution existence). | Every real form of a finite-dimensional complex semisimple algebra has a Cartan involution; inner conjugacy reduces its conjugation to theta sigma for an involution theta of a fixed compact form. | E3B897CBFC079A4E2AE987D725311105853B92A7F9AF46F09E36255FCCBC1A39 |
| Theorem 8.2 (real forms and compact involutions). | Real forms of a fixed complex semisimple algebra, including component-exchange factors, are real-isomorphic exactly when their compact involutions are conjugate under the full compact-form automorphism group. | E3B897CBFC079A4E2AE987D725311105853B92A7F9AF46F09E36255FCCBC1A39 |
| Proposition 8.3. | Maximal abelian subspaces of the Cartan minus eigenspace are conjugate under the compact connected group with Lie algebra ad k; each extends by a maximal toral subalgebra of its compact centralizer to a complex Cartan. | E3B897CBFC079A4E2AE987D725311105853B92A7F9AF46F09E36255FCCBC1A39 |
| Theorem 8.4. | All finite-dimensional real semisimple Lie algebras, including zero, arbitrary products and complex simple algebras viewed as real: real-isomorphism classification by explicit admissible directed Satake diagrams. Full parity necessity, principal sl2 reconstruction, compact normalization and diagram equivalence are proved. | E3B897CBFC079A4E2AE987D725311105853B92A7F9AF46F09E36255FCCBC1A39 |
| Proposition 8.1 (standard basis). | Finite Weyl group; standard Hecke basis over Z[v,v^-1] with q=v^2. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.1 (the canonical Hecke basis). | Finite Weyl group; unique bar-invariant canonical basis, integral KL polynomials and exact degree bounds. Positivity and Verma multiplicities are separate statements. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.3 (finite KL inversion). | Every finite Weyl group, arbitrary rank and components: the signed unitriangular KL polynomial matrix over Z[q] has inverse Q_xy=P_(w0*y,w0*x)=P_(y*w0,x*w0). Complete trace, duality and Bruhat reversal argument; no geometric multiplicity or positivity conclusion asserted. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Proposition 8.3 (dual-standard character, conditional on MP0–MP1). | Conditional on constructed mixed six operations, exact weight rules, ordinary finite-flag Bruhat geometry and the minimal-parabolic two-cell/affine-line package MP0–MP1: full dual-standard weighted character equals Hecke bar, with every boundary coefficient. No IC-purity assumption enters this deduction. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Proposition 8.4 (conditional IC–KL identification). | Conditional on the explicit mixed-operation/minimal-parabolic package, normalized mixed IC, strict boundary bounds and every-stalk weight=cohomological-degree purity: canonical-basis recognition forces nonnegative even stalk degrees and identifies KL coefficients with their dimensions. The general pointwise-purity input is not proved. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Proposition 8.5 (conditional simple-in-standard character expansion). | Conditional on the preceding actual IC stalk identity and an ordinary bounded finite-length perverse heart with constant IC simples and perverse cell standards: signed simple-in-standard Grothendieck relation and inverse-matrix standard composition coefficients, with exact transpose. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Proposition 8.6 (conditional transfer to Verma multiplicities). | Conditional on the preceding perverse IC relation and a proved exact nonzero-simple localization dictionary Delta_x -> M((x*w0) dot lambda), I_y -> L((y*w0) dot lambda), at dominant integral lambda: full algebraic conversion to P_(w,z)(1), using the unconditional finite inversion Theorem8.3. Exact localization itself remains an unsupplied input. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.6. | Finite graded modules over a finitely generated connected nonnegative real graded algebra: finite indecomposable decomposition and local degree-zero endomorphism algebra; every endomorphism of an indecomposable is a unit or nilpotent. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.7. | At the same graded finite scope: uniqueness of indecomposable decompositions and actual direct-sum cancellation. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.8. | For the finite-Weyl polynomial ring with linear forms in degree two: every finite graded projective summand of a graded free module is graded free; complete graded Nakayama proof. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.9. | Every finite Weyl group, any rank and components: homogeneous reflection-hyperplane localization of each actual Bott–Samelson object has only the specified lower graph and two-branch summands; both translation cases expanded. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.4. | Every finite Weyl group: whole graded Hom from an actual descending graph-flag bimodule to a shifted Bott–Samelson sum is right graded free with the exact support-character pairing formula. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.5. | Every object of the actual finite-Weyl Bott–Samelson idempotent closure: both primitive support maps have exact image multiplication by the product of right inversion roots; local divisibility and degreewise global equality are proved. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.6. | Every finite Weyl group: the exact right-free graded Hom formula holds for every Bott–Samelson summand, with actual extension lifting proved degree by degree. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.7. | Every finite Weyl group, including rank zero and products: one uniquely normalized indecomposable B_x for each x, all indecomposables its shifts, and B_x self-dual. Actual summands are constructed without a canonical-character assumption. Canonical characters and KL positivity are subsequently proved in Theorem8.10; the finite complex regular integral category-O transfer is proved in Theorem8.13. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.10 (primitive decomposition and orthogonality). | Finite-dimensional graded real space with a degree-two hard-Lefschetz operator: primitive decomposition and orthogonality of the exact Lefschetz forms. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.11 (continuous deformation). | Fixed nondegenerate symmetric graded form, continuous self-adjoint operators with hard Lefschetz throughout a connected interval: primitive Hodge signatures persist. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.12 (balanced invariant subspaces). | Balanced graded stable subspace of a hard-Lefschetz Hodge space: hard Lefschetz, restricted-form nondegeneracy and inherited signs. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.13 (an injective-map substitute for weak Lefschetz). | Degree-one intertwining injection in negative degrees with the exact form identity and Hodge target: Lefschetz injectivity on the source, even when its form is degenerate. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.14 (vanishing for a displaced centre). | Graded self-adjoint symmetric form on a hard-Lefschetz space centered strictly below zero: the entire form vanishes, including pairings between unequal chains. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.15 (a large-parameter rank-one extension). | Actual rank-one extension basis, square-zero middle operator and the stated mixed form identities: hard Lefschetz and standard Hodge signs for all sufficiently large positive parameters. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.16 (singular classification). | Finite Weyl group and one right simple invariant ring: classification of the actual summand category of restricted regular bimodules, at the specified top-coset normalization. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.8 (support-layer homotopy splitting). | Every chosen reduced expression in a finite Weyl group: actual standard and costandard support-layer complexes are homotopy equivalent to their single normalized graph in degree zero or a contractible complex. No braid-coherence theorem assumed. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.9 (actual right-singular descent). | Every finite Weyl group and right-simple coset: induction of its normalized singular indecomposable is the regular indecomposable of the maximal member, with no extra shift. The controlled middle-action basis is retained. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.10 (finite-Weyl Hodge theory and KL positivity). | Every finite Weyl group, including products and rank zero, over its real reflection realization: indecomposable canonical characters, hard Lefschetz, bottom-positive Hodge signs, nonnegative integer KL coefficients and nonnegative Laurent structure constants. The finite complex regular integral category-O Verma multiplicity transfer is proved in Theorem8.13. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.17 (dominant orbit inequality). | Finite Weyl group, strictly dominant a and weakly dominant b: orbit pairing inequality and exact equality condition, including closed-chamber uniqueness and the lowest dot-orbit comparison. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.18 (coatom containing a subword). | Finite Weyl reduced-subword order: every proper interval below w contains a coatom of w above its lower endpoint, proved by lifting and induction. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.19 (extremal norm). | Finite simple highest-weight module: every weight has norm at most that of an extremal weight, with equality exactly on its Weyl orbit and multiplicity one. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Lemma 8.20 (simple-root integrability). | Finite complex regular integral category O: each non-anti-dominant simple is integrable for some simple-root sl2; negative simple-root operators are injective on actual Verma-flag objects. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.11 (actual simple-wall translations). | Finite-dimensional complex semisimple Lie algebra, dominant integral lambda and one simple wall: actual exact translations have the specified one- and two-factor Verma flags and both adjunctions, proved in Section8.12. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.12 (big-projective wall effects). | At that finite ordinary simple-wall scope: translation out sends the singular anti-dominant big projective to the regular one; translation on gives two copies, so wall crossing gives two copies and preserves the structure-functor kernel. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Proposition 8.7 (free-orbit invariant jets). | Characteristic-zero field, finite linear group and a rational point with trivial stabilizer: invariant polynomials realize every finite jet. Every finite connected homogeneous quotient admits the resulting exact translated invariant surjection. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Proposition 8.8 (ambient-root projective order). | Finite complex regular integral category O, every ambient positive-root hyperplane and the specified deformed big-projective family: nonsplit root-local two-Verma residue and exact first-order endomorphism order. Its residue projectivity is proved in Section8.15.6; Sections8.14.2–8.14.7 prove the uniform Shapovalov determinant and transverse pairing. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.13 (regular integral category-O comparison and KL multiplicities). | Finite-dimensional complex semisimple Lie algebra and dominant integral lambda, including products and rank zero: actual coinvariant corner and central annihilator, full faithfulness with projective target, restriction/induction wall action, augmentation Hom and inverse projective label. The proved canonical-character theorem yields [M(w dot lambda):L(z dot lambda)]=P_(w,z)(1). | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
| Theorem 8.2 (Kazhdan–Lusztig multiplicities). | Same finite complex regular integral category-O scope: general dominant-convention KL Verma multiplicities are proved in Theorem8.13; coefficient positivity is proved by the finite-Weyl Hodge theorem8.10. | 9EE4CF2736C3B9E1D5B018EC13863127CC957648C5AEC4B33F671EB933D85897 |
Machine-readable providers · Further statement and proof scopes