LemmaStatement: AI-adaptedProof: 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.

Laurent binomial valuation at one over any field

Statement

Let $F$ be a field, let $F [t, t^{- 1}]$ be its Laurent polynomial ring (The Laurent polynomial ring as the principal localisation of Z[t] at t), and let $v_{1}$ be the $(t - 1)$ -adic valuation on the nonzero elements of $F [t, t^{- 1}]$ : for $0 \neq f$ , $v_{1} (f) : = \max {n \geq 0 : (t - 1)^{n} ∣ f in F [t, t^{- 1}]},$ so that $v_{1} (f) = 0$ exactly when $f (1) \neq 0$ (Discrete valuation rings). Let $A, B \in F ∖ {0}$ , let $u, v \in Z$ , put $N : = u - v$ and $f : = A t^{u} - B t^{v}$ .

If $A \neq B$ , then $v_{1} (f) = 0$ .
If $A = B$ and $N \neq 0$ , then $v_{1} (f) = 1$ when $char F = 0$ , and $v_{1} (f) = p^{v_{p} (∣ N ∣)}$ when $char F = p > 0$ ; here $v_{p}$ is the exponent of $p$ in $∣ N ∣$ , i.e. $N = p^{r} m$ with $p ∤ m$ (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise).
If $A = B$ and $N = 0$ , then $f = 0$ , and the zero element has no finite valuation.

In the intended application the Laurent polynomials $Q_{a} q_{H}^{j - i} t^{n a + j - i}$ (foot residues of the Jantzen expression) are compared by this lemma: it computes their valuation exactly when their difference is nonzero and prevents replacing valuations by an equality-of-residues indicator in positive characteristic.

Facts & Assumptions

Given: A field $F$ , nonzero $A, B \in F$ , integers $u, v$ , the Laurent polynomial $f = A t^{u} - B t^{v}$ , and the $(t - 1)$ -adic valuation $v_{1}$ of the Statement.

[F1]

The finite Laurent construction over $F$ uses sums $\sum_{k} a_{k} t^{k}$ with finite support and the coefficientwise addition and convolution multiplication. It is the field-coefficient version of The Laurent polynomial ring as the principal localisation of Z[t] at t; $t$ is a unit, and multiplying by a sufficiently large power of $t$ identifies any such sum with an ordinary polynomial.

[F2]

A DVR is the ring of nonnegative values of a surjective integer-valued valuation on a field (Discrete valuation rings). The multiplicity valuation used here is established locally in step 1.1.

[F3]

The characteristic is the least positive integer annihilating $1_{F}$ , or zero if no such integer exists (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise). Its field consequences needed here are established in step 1.1.

Proof

technique · direct

Given: The field $F$ , the Laurent polynomial ring $F [t, t^{- 1}]$ with unit $t$ , the valuation $v_{1}$ of the Statement, and the data of [F1]–[F3].

1.1F1F2F3algebra

Construct the valuation. For an ordinary nonzero polynomial $g$ , repeated division by $t - 1$ terminates as degree decreases, giving a unique factorization $g = (t - 1)^{a} g_{0}$ with $g_{0} (1) \neq 0$ ; division is explicit from $g (t) - g (1) = \sum_{j} a_{j} (t^{j} - 1)$ . For a Laurent polynomial multiply by $t^{M}$ first: since $t^{M} (1) = 1$ , the resulting multiplicity is independent of $M$ . Multiplying two factorizations multiplies their nonzero evaluations, so multiplicities add; adding them gives multiplicity at least their minimum, unless the sum is zero. Consequently $v (g / h) = v (g) - v (h)$ is a well-defined valuation on $F (t)$ , surjective since $v (t - 1) = 1$ . Its nonnegative-value ring is $F [t]_{(t - 1)}$ : cancel the powers of $t - 1$ in numerator and denominator, leaving a denominator nonzero at $1$ . This proves the DVR assertion in the sense of [F2], the zero-evaluation criterion, and invariance under Laurent units. Finally, positive field characteristic is prime: a composite least annihilator $a b$ would give $(a 1_{F}) (b 1_{F}) = 0$ with both factors nonzero. Division of an integer by that prime shows $m 1_{F} \neq 0$ if $p ∤ m$ .

1.2F1

The case $A = B$ , $N = 0$ . Then $f = A t^{u} - B t^{v} = A t^{u} - A t^{u} = 0$ by [F1], the zero element of $F [t, t^{- 1}]$ ; since $(t - 1)^{n} ∣ 0$ for every $n$ , the set in the definition of $v_{1}$ is unbounded and no finite value is assigned.

2.1F1F2step 1.1

Reduction to $N$ and to $A / B$ for $f \neq 0$ . Since $B t^{v}$ is a unit of $F [t, t^{- 1}]$ with inverse $B^{- 1} t^{- v}$ by [F1], the identity $A t^{u} - B t^{v} = B t^{v} ((A / B) t^{N} - 1)$ and [F2] give $v_{1} (A t^{u} - B t^{v}) = v_{1} ((A / B) t^{N} - 1)$ ; moreover if $N < 0$ then $t^{N} - 1 = - t^{N} (t^{- N} - 1)$ with $- t^{N}$ a unit, so $v_{1} (t^{N} - 1) = v_{1} (t^{∣ N ∣} - 1)$ by [F1] and [F2].

3.1F1F2step 1.1step 2.1

The case $A \neq B$ . Evaluating the Laurent polynomial $(A / B) t^{N} - 1$ at $t = 1$ gives $A / B - 1 \neq 0$ , so the factor $t - 1$ cannot divide $(A / B) t^{N} - 1$ : a product containing $t - 1$ would evaluate to $0$ under the ring homomorphism $f \mapsto f (1)$ with $1 \mapsto 1$ . Hence $v_{1} ((A / B) t^{N} - 1) = 0$ by [F2], and the reduction of step 2.1 gives $v_{1} (f) = 0$ .

3.2F1F2F3step 1.1step 2.1algebra

The case $A = B$ , $char F = 0$ , $N \neq 0$ . Here $f = A (t^{u} - t^{v}) = A t^{v} (t^{N} - 1)$ with $A t^{v}$ a unit, so by step 2.1 the valuation equals $v_{1} (t^{∣ N ∣} - 1)$ , while $t^{∣ N ∣} - 1 = (t - 1) (1 + t + \dots + t^{∣ N ∣ - 1})$ with second factor evaluating at $t = 1$ to $∣ N ∣ \cdot 1_{F} \neq 0$ by [F3] and therefore of valuation $0$ by [F2]; the valuation is additive on this factorisation of the nonzero polynomial $t^{∣ N ∣} - 1$ , so $v_{1} (f) = 1$ .

4.1F1F2F3step 1.1step 2.1algebra∎

The case $A = B$ , $char F = p > 0$ , $N \neq 0$ . Write $∣ N ∣ = p^{r} m$ with $r \geq 0$ and $p ∤ m$ . In characteristic $p$ the identity $(x - 1)^{p^{r}} = x^{p^{r}} - 1$ follows by iterating $(x - 1)^{p} = x^{p} - 1$ (the intermediate binomial coefficients $(\binom{p}{i})$ , $1 \leq i \leq p - 1$ , are multiples of $p$ ); applying it to $x = t^{m}$ gives $t^{∣ N ∣} - 1 = (t^{m} - 1)^{p^{r}} = (t - 1)^{p^{r}} (1 + t + \dots + t^{m - 1})^{p^{r}}$ . The second factor evaluates at $t = 1$ to $m^{p^{r}} \cdot 1_{F}$ , which is nonzero because $m \cdot 1_{F} \neq 0$ by [F3]; it thus has valuation $0$ by [F2], so $v_{1} (t^{∣ N ∣} - 1) = p^{r}$ , and step 2.1 gives $v_{1} (f) = p^{r} = p^{v_{p} (∣ N ∣)}$ .

Remarks

The lemma is a leaf computation over an arbitrary field: it is used where a denominator $t - 1$ is cleared or an integrality statement is checked at $t = 1$ , and it records explicitly that in characteristic $p$ the valuation is the full $p$ -power $p^{v_{p} (∣ N ∣)}$ , not merely the indicator of $p ∣ N$ . No choice principle is used.

Depends on

Used by

Dependency tree · two levels

26 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

Mathas, Positive Jantzen sum formulas for cyclotomic Hecke algebras, arXiv:2106.15486v2 (standard reference, not scraped)