Project Sandbox · almanacA0a · a reader's companion

The multiplicative grid

A polynomial can take whole-number values everywhere you look and still not have whole-number coefficients. This is the story of one small theorem that says exactly which polynomials do that on a geometric grid — and of how far that theorem has been checked.

The mathematics here is classical, and the theorem is not a new one. The question is Pólya's, from 1915; the geometric grid is Gel'fond's, from 1933, and Gramain's, from 1990; the deformed two-sided form is Harman and Hopkins', from 2016. What this record adds to them is two routine transports, set out in full further down. What is unusual is not the theorem but the record: it was proved, machine-verified and then edited into a form a stranger can check, and every claim on this page carries a statement of what warrants it.

The oldest version of the question

Take the polynomial $x (x - 1) / 2$ . Its coefficients are halves — not whole numbers — yet at every integer it returns an integer: 0, 0, 1, 3, 6, 10. The halving always cancels, because among any two consecutive integers one is even.

So "has integer coefficients" and "takes integer values" are different properties, and the second is strictly weaker. Pólya's theorem (1915) says exactly how much weaker: the polynomials taking integer values at every integer are precisely the integer combinations of the binomial polynomials $(\binom{x}{k}) = \frac{x (x - 1) (x - 2) \dots (x - k + 1)}{k!}, k = 0, 1, 2, \dots$ — for each $k$ a polynomial in $x$ of degree $k$ , with rational coefficients; $(\binom{x}{2}) = x (x - 1) / 2$ is the one above. The failure of integrality in the coefficients is entirely accounted for by changing basis. Everything below is a deformation of that sentence.

What this record proves

Pólya's sentence has three ingredients: the points where the values are tested (the integers), the numbers that the values and the coefficients are measured against (the integers again), and the binomial polynomials that mediate between the two. The theorem in this record deforms each of the three. Here they are, one at a time, in the notation this page will use; the statement follows, and nothing in it will not have been explained first.

Two variables. Throughout, $v$ and $t$ are two independent formal variables — letters about which nothing is assumed. Everything is written in terms of the square $q = v^{2}$ , for a reason that will become a hypothesis below: only even powers of $v$ ever occur, and that is what the word even means on this page. The second variable $t$ is a spectator. It is there because the question was posed for a whole family of algebras at once, one for each value of $t$ , and it rides through the argument without ever being constrained — but it has to be carried.

Two rings. Write $𝔸 = ℤ [v^{\pm 1}, t^{\pm 1}]$ for the whole-number combinations of powers of $v$ and $t$ , positive or negative. On this page integral means lies in $𝔸$ . Write $𝔽 = ℚ (v) [t^{\pm 1}]$ for the larger ring in which fractions in $v$ are also allowed — $1 / (q - 1)$ , for instance — while $t$ still appears through its powers alone. Every element of $𝔸$ is an element of $𝔽$ , and the gap between the two is the whole theorem.

The grid. In place of the integers, values are tested on the geometric progression $q^{χ}$ , where $χ$ runs over all the integers, of either sign: $\dots, q^{- 2}, q^{- 1}, 1, q, q^{2}, \dots$

The polynomials, and their values. A Laurent polynomial in $Y$ is a finite sum $f (Y) = \sum_{k} c_{k} Y^{k}$ in which the exponents $k$ are integers of either sign and the coefficients $c_{k}$ lie in $𝔽$ . Its value at a point of the grid is $f (q^{χ})$ , obtained by substituting $q^{χ}$ for $Y$ . Call $f$ grid-integral if $f (q^{χ})$ lies in $𝔸$ for every integer $χ$ . This is the deformation of "takes an integer value at every integer".

The $q$ -binomial polynomials. Set $ν_{0} (Y) = 1$ and, for $r \geq 1$ , $ν_{r} (Y) = \prod_{s = 0}^{r - 1} \frac{Y - q^{s}}{q^{r} - q^{s}} .$ For $r \geq 1$ their coefficients lie in $𝔽$ and not in $𝔸$ — already $ν_{1} (Y) = (Y - 1) / (q - 1)$ — but their values on the grid are integral, and in exactly Pólya's way: at the node $Y = q^{n}$ the value $ν_{r} (q^{n})$ is the Gaussian binomial coefficient ${(\binom{n}{r})}_{q}$ , for every integer $n$ , positive or negative. That is the $q$ -analogue of the fact that $(\binom{x}{k})$ takes the value $(\binom{n}{k})$ at $x = n$ , and it is what makes $ν_{r}$ the right replacement for $(\binom{x}{k})$ .

Theorem — the exact

q

-Pólya theorem for

{G L}_{1}

Let $f (Y)$ be a Laurent polynomial in $Y$ with coefficients in $𝔽$ . Then $f$ is grid-integral — that is, $f (q^{χ}) \in 𝔸$ for every integer $χ$ — if and only if $f$ can be written as a finite sum

f (Y) = \sum a_{u, r} Y^{u} ν_{r} (Y)

with integer shifts $u$ of either sign, indices $r \geq 0$ , and coefficients $a_{u, r}$ in $𝔸$ .

Read it against Pólya: his $ℤ$ is our $𝔸$ , his $(\binom{x}{k})$ is our $ν_{r} (Y)$ , and the shifts $Y^{u}$ are there because the grid runs in both directions. Read from right to left the theorem is the easy inclusion — each $Y^{u} ν_{r} (Y)$ is grid-integral because the Gaussian binomials lie in $𝔸$ , and sums of integral values are integral. The content is the other direction: every grid-integral Laurent polynomial is such a combination. The combination need not be unique — the second witness below shows the family is dependent — so this is a theorem about spanning, and it says exactly that.

In the paper the same objects wear more dress: the rings carry a subscript, $A_{t}$ and $F_{t}$ , as a reminder that $t$ is present; the grid coordinate carries a check mark, which records where the grid comes from in higher rank and carries nothing at ${G L}_{1}$ ; and the set of grid-integral Laurent polynomials is called the even Newton lattice and written $𝒩^{e v}$ , ev for the even powers. The theorem is stated there as the equality of that set with the span of the shifted $q$ -binomial polynomials — the same statement, with the same content. This page drops the decoration and nothing else.

Where the difficulty lives

The polynomials have coefficients in $𝔽$ ; what is required to lie in $𝔸$ are their values. If the coefficients were already in $𝔸$ there would be nothing to prove — the values would follow for free. The content is that a polynomial can fail the coefficient test and pass the value test, and that the $q$ -binomial polynomials account for every way this can happen.

One element shows the gap is real. Take the first $q$ -binomial polynomial:

ν_{1} (Y) = \frac{Y - 1}{q - 1}

Its single coefficient is $1 / (q - 1)$ . That coefficient does not lie in $𝔸$ , because $q - 1$ cannot be inverted there. But watch what the polynomial itself does on the grid:

node $Y = q^{χ}$	$ν_{1}$ evaluated there
$q^{- 2}$	$- q^{- 1} - q^{- 2}$	integral
$q^{- 1}$	$- q^{- 1}$	integral
$q^{0}$	$0$	integral
$q^{1}$	$1$	integral
$q^{2}$	$1 + q$	integral
$q^{3}$	$1 + q + q^{2}$	integral
$v^{3}$	$\frac{v^{2} + v + 1}{v + 1}$	off the grid — not integral

node

Y = q^{χ}

ν_{1}

evaluated there

q^{- 2}

- q^{- 1} - q^{- 2}

integral

q^{- 1}

- q^{- 1}

integral

q^{0}

0

integral

q^{1}

1

integral

q^{2}

1 + q

integral

q^{3}

1 + q + q^{2}

integral

v^{3}

\frac{v^{2} + v + 1}{v + 1}

off the grid — not integral

These are six nodes of a grid that runs on for ever in both directions, so the table illustrates the cancellation and is never the argument for it. What settles every node at once is the closed form $ν_{1} (q^{χ}) = (q^{χ} - 1) / (q - 1)$ , which equals $1 + q + \dots + q^{χ - 1}$ when $χ > 0$ and $- (q^{- 1} + \dots + q^{χ})$ when $χ < 0$ : a whole-number combination of powers of $q$ either way. The last row is not a grid point at all, and there the cancellation fails; that row is the subject of the third witness below. The seven tabulated values were recomputed on the project's computer-algebra oracle while this page was written.

Three ways the statement is tight

Every clause in the statement is doing work, and one value each shows it. These are the sharp edges of the result: what it delivers, what it stops short of, and the hypothesis it cannot do without.

The

q

-binomial polynomials are genuinely needed

$ν_{1}$ is grid-integral and its coefficient is not integral. The closed form above puts its value in $𝔸$ at every one of the infinitely many nodes, while its single coefficient $(q - 1)^{- 1}$ lies outside $𝔸$ . So the grid-integral Laurent polynomials form a strictly larger set than $𝔸 [Y^{\pm 1}]$ , and the theorem says something the coefficients alone do not.

It spans, and stops there

The generating family satisfies a relation: $(q - 1) ν_{1} (Y) - Y + 1 = 0$ over $𝔸$ . So the shifted $q$ -binomial polynomials span the grid-integral Laurent polynomials without being independent, and this is a spanning theorem — a basis theorem would be a stronger result and is not this one. Whether the grid-integral Laurent polynomials have a basis over $𝔸$ is not settled by this record; the last section says what is known beyond it.

The grid must be even

At the odd node $v^{3}$ the value leaves $𝔸$ : $ν_{1} (v^{3}) = \frac{v^{3} - 1}{v^{2} - 1} = \frac{v^{2} + v + 1}{v + 1}$ . Since $q = v^{2}$ , the grid is the even powers $v^{2 χ}$ , and $ν_{1}$ is integral at every one of them — but refine the grid to all powers of $v$ and integrality breaks at the first new node. The word even in the statement is a hypothesis, not a convenience.

Each of these is settled by a single value, which is worth saying plainly: one value is a complete proof of a statement of this shape, not evidence for it. Nothing here rests on a sample.

Where the statement came from

The theorem is reached from known results along a line worth setting out, because each of the four steps below changed what the question was about.

1915

Pólya — the additive origin

Integer-valued polynomials on the integers are the $ℤ$ -span of the binomial polynomials. The template for everything that follows.
1933 · 1990

Gel'fond, then Gramain — moving the grid

Ask for integrality along $1, q, q^{2}, \dots$ instead. For entire functions that is Gel'fond, 1933 — the multiplicative analogue of Pólya's problem. For polynomials it is Gramain's Proposition 2.2: for an integer $q \geq 2$ , the polynomials integral at every $q^{k}$ are generated by the Gauss binomial polynomials — which are exactly the $ν_{r}$ of this record.
2016

Harman and Hopkins — deforming the coefficients

Which $P \in ℚ (q) [x]$ satisfy $P ([n]_{q}) \in ℤ [q]$ ? Their §1 answers it on the additive grid of $q$ -integers; their §4 takes the nodes over all of $ℤ$ , which is the bilateral form this record needs. Their §4 also contains the remark that joins the two lines: setting $z = 1 + (q - 1) x$ turns evaluation at $x = [n]_{q}$ into evaluation at $z = q^{n}$ — the additive grid becomes the geometric one, node for node.
this record

What is added — two routine transports

The grid variable is inverted, so the objects are Laurent rather than polynomial; at a grid of units that is a clearing argument, not a difficulty. And the coefficients carry a free parameter $t$ , which arrives from the setting the goal was posed in and rides through as a spectator — the integrality test decomposes coefficient-wise.

How far it has been checked

The record exists in three layers — a written proof, a Julia instrument that computes the objects, and a Lean development the proof kernel accepts. The grades below are different kinds of claim, each meaning exactly what it states, and the edition keeps them distinct.

1 / 12

ink — a refereed argument

An argument written for a human reader and refereed. No kernel certifies it and no computation bounds it: the check is a referee reading the proof. The one here is the claim every other result rests on — that the proof proves the statement that was signed.

2 / 12

orange — computed over a declared range

Verified by computation over a stated bound, and over nothing else. The bound is part of the claim. Neither of these could ever be kernel-certified: no Lean declaration states what a Julia program does.

9 / 12

blue — kernel-certified

A Lean declaration states the claim and its axiom base is exactly propext, Classical.choice, Quot.sound: the three standard axioms of Lean's kernel — propositional extensionality, the axiom of choice and quotient soundness — the base every Mathlib proof shares; a certificate is clean when these three are all it needs — with no sorryAx, no custom axiom. Every one of these was measured first-hand through the Lean language server.

The computed rows are the instrument (acceptance battery 87/87, with the grid integrality checked for $r$ in $0 \dots 8$ against $χ$ in $- 9 \dots 9$ , and a negative control of 249 cases required to fail — which they do) and an independent oracle referee pin (verdict PROVED_BOUNDED, 60 positive and 5 hostile seeds, 0 disagreements).

The deliverable is the theorem with a clean axiom base. No theory of integer-valued polynomials, classical or $q$ -deformed, exists in Mathlib — not Pólya's theorem, not a $q$ -analogue. That absence is why the formal layer had to be built rather than cited.

The honest size of the result

First, what rank means here, because it is the one word on this page with two readings. Rank is the semisimple rank: the number of simple roots. ${G L}_{1}$ has none, so this record is the rank $0$ case; ${G L}_{2}$ is rank 1, ${G L}_{3}$ is rank 2, and so on. The group ${G L}_{1}$ is of course one-dimensional, which is where the second reading comes from, but nothing on this page uses it.

At ${G L}_{1}$ this is the degenerate case, and the edition says so first. The root system is empty, so the algebra is commutative and its centre is all of it; the Weyl group is trivial; the Harish–Chandra projection is the identity map. Two of the three clauses in the original goal are formalities at rank 0. The value of the record is that a small true statement was carried end to end, and that the cost and the failure modes of doing so were measured. Rank 1, which is ${G L}_{2}$ , is a separate closed record of the same programme and is cited in the paper; rank 2 and above are open, and nothing on this page bears on them.

A tested agreement is not a proof. The Julia and Lean layers are two independent implementations joined by a shared naming discipline, not by a checked morphism. Agreement between them is established by testing, over the bounds printed above, and it licenses nothing beyond them.

The ancestral result is not our result. The Harman–Hopkins bilateral quantum Pólya theorem is the ancestor of the transported argument. The reconciliation that would identify their lattice with this one is open.

What is still open

Three things, stated because an edition that lists only its results teaches a false boundary. "Open" on this page means one thing: not settled by this closed record. The programme has gone on with each of the three since the record closed, and what it holds is stated below with its warrant, because the three grades of warrant are not interchangeable.

A basis. This record proves that the grid-integral Laurent polynomials are spanned by the shifted $q$ -binomial polynomials and that this family is dependent; it exhibits no basis, and nothing certified here decides whether the set is a free module over $𝔸$ . The programme's closed, kernel-certified rank-one record ( ${G L}_{2}$ ) goes further: it exhibits bases — the bilateral elementary basis, and the affine-Grassmannian and affine-flag flow-up bases — and it proves, with the kernel's certificate, that the bilateral one-variable lattice is free on the signed bilateral Newton rows (nodes taken in the order $0, 1, - 1, 2, - 2, \dots$ ): a Laurent polynomial is integral at every signed node exactly when it has a unique expansion in those rows with integral coefficients. What no record has done is carry that statement into this record's rings — its coefficient ring has no square root of $q$ and two spectator parameters where this one has $v$ and $t$ — a routine base change of the kind this record itself performs, performed by nobody for this statement. Work resting on the rank-one record's ordered-pair basis $E_{a} E_{b}$ , $a \geq b \geq 0$ , continues in a candidate manuscript, not adopted and not kernel-certified, and a further sandbox is planned behind it.

The four-way reconciliation. That Lusztig's toral lattice, this record's lattice, the bilateral weight-Newton span and the transported Harman–Hopkins ring are one lattice under one normalisation. Two of the three identifications are argued on the programme's own shelf, none is chained, three frame differences block chaining by inspection, and the computer-algebra evidence reaches degree 7. Open in the plain sense.

Rank $\geq 2$ . The two clauses that are formalities here carry the weight there, and this record's argument does not transport. But the statement is not unknown. For ${G L}_{3}$ it is kernel-certified in full — twenty-four declarations on the clean axiom triple, no sorry, 11 August 2026 — with the closure package filed and one criterion outstanding, the Overseer's signature. For ${G L}_{n}$ , every $n$ , the programme holds an informal proof, refereed and adopted on 24 August 2026: the statement is kernel-checked, the proof is not, no closed record stands behind it, and its computational checks are bounded to declared ranges. What is open in the plain sense is the general-lattice centre conjecture beyond the ${G L}_{n}$ lattice.

This page is a companion: it explains, and the record certifies. The record-bearing edition — one row per result, joining all three layers under a stated convention frame, with per-row ancestry and a manifest of every shipped file and its hash — is a separate document, and where the two ever disagree the record is right and this page is wrong.

Every mathematical claim on this page — the theorem, the three witnesses, the tabulated values, the open problems — is drawn from that edition's register. The seven grid values and the two identities in the witnesses were recomputed fresh on the project's warm computer-algebra oracle while this page was written. The closed form for $ν_{1}$ , and the identification of $ν_{r}$ 's values with the Gaussian binomial coefficients, are cancellations from the definition quoted above — the powers of $q^{s}$ divide out — and were confirmed symbolically over a range of $r$ and $χ$ when this page was last revised.

almanacA0a · pilot edition over the closed record SandboxA/sandboxA0a · assembled by the Almanac Editor.

The multiplicative grid

The oldest version of the question

What this record proves

Where the difficulty lives

Three ways the statement is tight

Where the statement came from

Pólya — the additive origin

Gel'fond, then Gramain — moving the grid

Harman and Hopkins — deforming the coefficients

What is added — two routine transports

How far it has been checked

The honest size of the result

What is still open