TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Simultaneous induction: Soergel's conjecture, hard Lefschetz and the Hodge-Riemann relations hold for all elements

Facts & Assumptions

Given: A symmetric group $S_{n}$ , a finite Bruhat ideal $X \subseteq S_{n}$ (closed under $y \leq x \in X$ ), the statements $S (x)$ , $h L (x)$ , $H R (x)$ of the dictionary (Primitive subspaces, hard Lefschetz and the Hodge-Riemann signs: the dictionary of hypotheses S, hL and HR), the deformed statement packages $h L (x, s)_{ζ}$ , $H R (x, s)_{ζ}$ , $H R b a r (x, s)_{ζ}$ with lowest degree $- ℓ (x) - 1$ (The deformed Lefschetz operator L_zeta on B_x B_s), the local intersection forms $(-, -)_{y}^{x, s}$ and the sign hypotheses $S^{\pm} (y, x, s)$ (The local intersection form on Hom(B_y, B_x B_s), Primitive subspaces, hard Lefschetz and the Hodge-Riemann signs: the dictionary of hypotheses S, hL and HR), and a fixed strictly dominant $ρ$ .

[F1]

The detection theorem: under $S (< x s)$ , non-degeneracy of every local intersection form $(-, -)_{y}^{x, s}$ for $y < x s$ is equivalent to $S (x s)$ (Non-degeneracy of the local intersection forms detects Soergel's conjecture one step higher).

[F2]

The embedding theorem: under $S (< x s)$ and $H R (y)$ for $y < x s$ , the local intersection forms embed isometrically, up to a positive scalar, into the primitive Lefschetz forms of $B_{x}^{R} B_{s}^{R}$ ; consequently $H R (x, s)$ implies $S (x s)$ , and more precisely $H R (x, s)$ implies the definiteness statements $S^{\pm} (< x s, x, s)$ (Embedding theorem: local intersection forms are isometric to primitive Lefschetz forms).

[F3]

The three-case hard Lefschetz theorem for the deformed operator on $B_{x} B_{s}$ : the cases $(ζ > 0, x s < x)$ under $S (x)$ and $h L (x)$ ; $(ζ > 0, x s > x)$ under $S (\leq x)$ , the lower ascent HR statements, $H R b a r (< x, s)_{ζ}$ and $H R (x)$ ; and $(ζ = 0, x s > x)$ under $S (\leq x)$ , the lower ascent HR statements, $H R (x)$ and $h L (z)$ for all $z < x s$ ; in each case the conclusion is $h L (x, s)_{ζ}$ for the stated parameters (Hard Lefschetz for the deformed operator on B_x B_s, in the three cases).

[F4]

The deformation principle: $H R (x)$ together with $h L (x, s)_{ζ}$ for all $ζ$ in an interval implies $H R (x, s)_{ζ}$ throughout that interval, because $H R (x, s)_{ζ_{0}}$ holds for some $ζ_{0} ≫ 0$ and signatures are constant on compact parameter intervals free of parameter values where the form degenerates; on $(0, \infty)$ one applies this on a compact subinterval joining any requested positive parameter to a sufficiently large one (Hodge-Riemann relations hold for large positive deformation, and the deformation principle, Signature constancy in a Lefschetz family, the L-stable subspace lemma and the weak-Lefschetz substitute).

[F5]

The undeformed restriction lemma: if $h L (x, s)_{0}$ holds then $h L (x s)$ holds, and if $H R b a r (x, s)_{0}$ holds then the restriction of the intersection form to the top summand $B_{x s}$ satisfies HR with the ambient signs; once $S (x s)$ is known, positivity of the comparison scalar identifies this restricted form with the intrinsic normalized one, giving $H R (x s)$ and $H R b a r (x s)$ (Undeformed Lefschetz and Hodge-Riemann restrict to the next Soergel summand).

[F6]

The unit $B_{e} = R$ has character $H_{e} = {\underline{H}}_{e}$ , reduction $R$ in degree zero, multiplication form $⟨ 1, 1 ⟩ = 1$ and zero positive-degree operator. Its only nonzero Lefschetz map is $L^{0} = 1$ , and its only primitive form is positive. Thus $S (e)$ , $h L (e)$ , $H R (e)$ hold. The rank-one and rank-two carriers give concrete instances of the first two length layers; the induction below also proves these layers from the unit start (Indecomposable labels, characters and filtration ranks agree after real scalar extension, The rank-one Soergel bimodule square splits, Rank-two type-A Soergel bimodule decompositions).

[F7]

For an ascent $y s > y$ , $S (u)$ for all $u < y s$ gives the unshifted decomposition $B_{y} B_{s} = B_{y s} \oplus ⨁_{u < y s} B_{u}^{a_{u}}$ ; for a descent $y s < y$ , $S (y)$ gives $B_{y} B_{s} = B_{y} (1) \oplus B_{y} (- 1)$ . Independently, under $S (y)$ the intrinsic form on $B_{y}$ and every restriction from a reduced word for $y$ compare by a positive scalar. Their induced forms on $B_{y} B_{s}$ compare by that same scalar, so this positivity transfers tensor HR to every reduced-word embedding for either ascent or descent (Indecomposable labels, characters and filtration ranks agree after real scalar extension, Invariant forms on an indecomposable Soergel bimodule are unique up to scalar, non-degenerate, and agree with the restricted Bott-Samelson form, The trace, the invariant intersection form on Bott-Samelson bimodules and its reduction).

Statement

Let $X \subseteq S_{n}$ be a finite Bruhat ideal containing the initial ideal $X_{0} = {w : ℓ (w) \leq 2}$ and assume:

(1) $H R (z, t)_{ζ}$ holds for all $ζ \geq 0$ , all $z < z t$ with $z t \in X$ and all simple $t$ ;

(2) $H R (z, t)_{ζ}$ holds for all $ζ > 0$ , all $z t < z$ with $z \in X$ and all simple $t$ .

Then for every $x \in X$ the three statements $S (x)$ , $h L (x)$ and $H R (x)$ hold. The length-ordered induction below starts with the unit, establishes (1) and (2) on $X_{0}$ in its first two length layers, and preserves them as each next element is adjoined. It therefore gives: for every $w \in S_{n}$ , Soergel's conjecture $S (w)$ , hard Lefschetz $h L (w)$ and the Hodge-Riemann relations $H R (w)$ hold; and for every $x, s$ with $x s > x$ the strong forms $H R b a r (x, s)_{ζ}$ hold for all $ζ \geq 0$ . The induction below is finite (it runs over the finitely many elements of $S_{n}$ ) and uses no choice.

Proof

technique · induction over the finite Bruhat order; the four implications (detection, embedding, three-case hard Lefschetz and deformation) are assembled for one minimal element at a time, and the parameter intervals are kept away from the singular zero-parameter descent case

1.1basegivenF6

Unit start. The ideal $X = {e}$ satisfies $S (e)$ , $h L (e)$ and $H R (e)$ by [F6]. There are no ascent pairs with target in $X$ and no descent pairs with source in $X$ , so (1) and (2) hold vacuously. We build the global theorem from this smaller start; in particular no unproved rank-two Hodge computation is used as a base input.

2.1ihstep 1.1given

Length-ordered induction. Maintain a Bruhat ideal $X$ on which $S$ , $h L$ , $H R$ , (1) and (2) hold. Choose $x^{'}$ of smallest length outside $X$ , and write $x^{'} = x s$ with $s$ a right descent and $x \in X$ . Every element of strictly smaller length than $x^{'}$ is in $X$ ; this stronger invariant is the reason for choosing the length order. An element below $x^{'}$ has smaller length, so adjoining $x^{'}$ retains the ideal property. Assume the maintained conclusions on $X$ .

3.1step 2.1

Every lower ascent required at a new pair. Fix any right descent $t$ of $x^{'}$ and put $z = x^{'} t$ , so $ℓ (z) = ℓ (x^{'}) - 1$ . If $w < z$ and $u$ is any simple reflection with $w u > w$ , then $ℓ (w u) = ℓ (w) + 1 \leq ℓ (z) < ℓ (x^{'})$ . Hence $w u \in X$ , and (1) gives $H R (w, u)_{ζ}$ for every $ζ \geq 0$ . This supplies all lower ascent hypotheses for the hard-Lefschetz theorem at $(z, t)$ , including reflections other than $t$ , without any false comparability assertion.

4.1step 2.1step 3.1F7

Every lower deformation required at a new pair. For $w < z = x^{'} t$ , if $w t > w$ , then step 3.1 with $u = t$ supplies $H R (w, t)_{ζ}$ for every nonnegative parameter. If $w t < w$ , then $w \in X$ and (2) supplies it for every positive parameter. The maintained $S (w)$ and the positive comparison of forms in [F7] give the corresponding strong embedded statements. Thus $H R b a r (< z, t)_{ζ}$ holds for every $ζ > 0$ , with exactly the strict lower range needed in case (2).

5.1step 2.1step 3.1step 4.1F3

Hard Lefschetz for every new ascent pair. Let $t$ be a simple right descent of $x^{'}$ , i.e. $x^{'} t < x^{'}$ ; then $z : = x^{'} t \in X$ , and we apply the three-case theorem [F3] to the pair $(z, t)$ with $z t = x^{'}$ : case (2) with $ζ > 0$ uses $S (\leq z)$ , the lower ascent statements for $z$ (from (1) for $X$ ) and $H R b a r (< z, t)_{ζ}$ (from steps 3.1 and 4.1), and $H R (z)$ from the maintained induction hypothesis, and gives $h L (z, t)_{ζ}$ for all $ζ > 0$ ; case (3) with $ζ = 0$ uses the same lower ascent statements, $H R (z)$ and $h L (w)$ for all $w < z t = x^{'}$ (available since all such $w$ lie in $X$ ) and gives $h L (z, t)_{0}$ . Hence $h L (x^{'} t, t)_{ζ}$ holds for all $ζ \geq 0$ for every right descent $t$ of $x^{'}$ .

6.1step 5.1F4F7

Hodge-Riemann for every new ascent pair. Fix a right descent $t$ of $x^{'}$ and keep $z = x^{'} t \in X$ . By $H R (z)$ and the deformation principle [F4] applied on $[0, \infty)$ to the family $h L (z, t)_{ζ}$ , obtained in step 5.1 for all $ζ \geq 0$ , the relations $H R (z, t)_{ζ}$ hold for all $ζ \geq 0$ . Positive comparison in [F7] also gives $H R b a r (z, t)_{ζ}$ at every such parameter. In particular the condition (1) holds for $X \cup {x^{'}}$ : the only new pairs are those with $z t = x^{'}$ , i.e. $z = x^{'} t$ for the right descents $t$ of $x^{'}$ , and these have been verified for all $ζ \geq 0$ ; all other pairs lie in $X$ and are covered by (1) for $X$ .

7.1step 6.1step 2.1F1F2

Soergel's conjecture for $x^{'}$ . Take the chosen right descent $s$ with $x^{'} = x s$ , $x \in X$ , and the instance $H R (x, s)_{0}$ of step 6.1. Since $S (y)$ and $H R (y)$ hold for all $y < x^{'}$ , the embedding theorem [F2] gives that the local intersection forms on ${Hom}^{0} (B_{y}, B_{x} B_{s})$ , $y < x^{'}$ , are definite for the sign $S^{\pm} (y, x, s)$ and hence non-degenerate; the detection theorem [F1] then gives $S (x^{'})$ .

8.1step 5.1step 6.1step 7.1F5F7

Hard Lefschetz and Hodge-Riemann for $x^{'}$ . By [F5] applied to the pair $(x, s)$ with $h L (x, s)_{0}$ from step 5.1 we obtain $h L (x^{'})$ ; and by [F5] applied to $H R b a r (x, s)_{0}$ from step 6.1, the restriction of the intersection form to the top summand $B_{x^{'}}$ satisfies HR, which by the now established $S (x^{'})$ and the positivity of the comparison scalar [F7] is $H R (x^{'})$ .

9.1step 6.1step 7.1step 8.1F3F4

The descent condition for the enlarged ideal. Let $t$ be simple with $x^{'} t < x^{'}$ . By $S (x^{'})$ from step 7.1 and $h L (x^{'})$ from step 8.1, the positive-parameter descent case of [F3] gives $h L (x^{'}, t)_{ζ}$ for all $ζ > 0$ ; together with $H R (x^{'})$ from step 8.1, so the deformation principle [F4] applied on the interval $(0, \infty)$ gives $H R (x^{'}, t)_{ζ}$ for all $ζ > 0$ (any requested positive parameter is joined to a sufficiently large one by a compact subinterval avoiding $0$ ). The pairs with $z \in X$ and $z t < z$ are covered by (2) for $X$ ; hence (2) holds for $X \cup {x^{'}}$ . Together with step 6.1 this shows that (1) and (2) are preserved by the induction step, and with steps 7.1 and 8.1 that $S$ , $h L$ , $H R$ hold on $X \cup {x^{'}}$ .

10.1step 9.1F5F7discharge-induction: step 2.1∎

Conclusion. The finite length-ordered induction starting from ${e}$ reaches $X = S_{n}$ , so $S (w)$ , $h L (w)$ and $H R (w)$ hold for every $w \in S_{n}$ ; and for every pair $x, s$ with $x s > x$ the sequence of steps 5.1, 6.1 applied to $z = x$ gives $H R (x, s)_{ζ}$ for all $ζ \geq 0$ , hence also the strong embedded forms $H R b a r (x, s)_{ζ}$ by the positivity of the comparison scalars [F7]. The first two length layers establish the stated initial ideal $X_{0}$ . The global conclusions restricted to any Bruhat ideal give the conditional assertion of the Statement as well. No step restricts a positive middle-position operator to a summand: every passage from the tensor product to its top summand uses the zero-parameter instance and the undeformed restriction lemma [F5], and the positive parameters are handled by the deformation principle on intervals that avoid the singular value $ζ = 0$ in the descent case.

Remarks

The unit starts the induction. Its first two length layers establish the rank-one and rank-two cases; the examples companion page illustrates them but is not used as a supplier. The finite length order uses no choice axiom.
Steps 3.1-4.1 show that the lower hypotheses needed by the three-case hard-Lefschetz theorem are available one step before they are used, which is what lets the induction close without assuming any statement at the element currently being proved.

Depends on

Used by

Soergel's character conjecture for type A Theorem

Dependency tree · two levels

51 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

Elias-Williamson, The Hodge theory of Soergel bimodules (arXiv:1212.0791v2, final version; Ann. of Math. 180 (2014) 1089-1136) (standard reference, not scraped)
Riche, La theorie de Hodge des bimodules de Soergel (d'apres Soergel et Elias-Williamson), Seminaire Bourbaki no. 1139 (arXiv:1711.02464, Octobre 2017) (standard reference, not scraped)
Soergel, Kazhdan-Lusztig-Polynome und unzerlegbare Bimoduln ueber Polynomringen (arXiv:math/0403496, published J. Inst. Math. Jussieu 6 (2007) 501-525) (standard reference, not scraped)