almanacA0a

The theorem

Let v, t be independent indeterminates and q = v². Write A_t = ℤ[v^{±1}, t^{±1}] and F_t = ℚ(v)[t^{±1}]. For χ ∈ ℤ let ev_χ be the F_t-algebra map with ev_χ(Y̌) = q^χ, and put ν_0 = 1, ν_r(X) = ∏_{s<r} (X − q^s)/(q^r − q^s).

The polynomials have coefficients in F_t; what is required to lie in A_t are their values. That gap is the whole of the theorem — with coefficients already in A_t there would be nothing to prove.

N^ev = Σu∈ℤ Σr≥0 A_t · Y̌^u ν_r(Y̌)

The divided classes are genuinely needed, and one element shows it. It is not the case that every grid-integral Laurent polynomial already has its coefficients in A_t — that is refuted by ν_1(Y̌) = (Y̌−1)/(q−1), which lies in N^ev and not in A_t[Y̌^{±1}]: its value at Y̌ = q^χ is (q^χ−1)/(q−1) = 1 + q + ⋯ + q^{χ−1}, integral at every node, while its one coefficient (q−1)^{-1} is not in A_t. So A_t[Y̌^{±1}] ⊊ N^ev, strictly.

This is a spanning statement, not a basis theorem, and it does not improve to one. The generating family satisfies the relation (q−1)·ν_1(Y̌) − Y̌ + 1 = 0 over A_t, so it is not independent. Whether N^ev is free over A_t on some other family is open.

The evenness of the grid is a hypothesis, not a convenience. It is not the case that the divided classes stay integral when the grid is refined from the even nodes q^χ = v^{2χ} to all powers of v — that is refuted by a single value. Since q = v², at the odd node v³ one has ν_1(v³) = (v³−1)/(v²−1) = (v²+v+1)/(v+1), which is not in A_t, while ν_1 is integral at every even node. Refine the grid and the theorem fails.

Where the statement came from

The signed goal states three clauses about the even hybrid family form at rank one: that it is an A_t-subalgebra, that the Harish–Chandra projection restricts to an isomorphism onto the Weyl-invariants, and the span identity above.

At GL₁ the first two are formalities. The root system is empty, so the algebra is commutative and its centre is the whole of it; the Weyl group is trivial, so the invariance condition is empty; and the Harish–Chandra projection is the identity map. They are recorded because the goal was posed as the rank-one case of a programme about centres in higher rank, where they carry weight. The mathematics in this record is the span identity, and this edition is about that.

How the theorem descends

The statement proved here is a known theorem, reached along a line that is worth setting out, because each step changed what the question was about. Every source named below is held, and each is carded in this edition with the convention frame under which we read it.

Pólya, 1915 — the additive origin

A polynomial with rational coefficients can take integer values at every integer without having integer coefficients; binom(x,2) = x(x−1)/2 is the standard witness. Pólya's theorem is that these integer-valued polynomials are exactly the ℤ-span of the binomial polynomials binom(x,k) — the failure of integrality in the coefficients is completely accounted for by a change of basis. Everything below is a deformation of that sentence. (Über ganzwertige ganze Funktionen, Rend. Circ. Mat. Palermo 40; printed as 1919 in Harman–Hopkins §1, and the standard modern reference is Cahen–Chabert, AMS Surveys 48.)

Gel'fond and Gramain — moving the grid from arithmetic to geometric

The natural next question is what happens when integrality is imposed not at 0, 1, 2, … but along a geometric progression 1, q, q², …. For entire functions that is Gel'fond, 1933 — Gramain calls it the analogue multiplicatif of Pólya's additive problem. For polynomials it is Gramain's own Proposition 2.2: for an integer q ≥ 2, the polynomials integral at every q^k are the ℤ-module generated by the Gauss binomial polynomials — and those are exactly the divided classes ν_r of this record. He remarks that such results are sans doute classiques yet ne semblent pas disponibles dans la littérature, and proves them for that reason, which is what makes him the citable source for the result.

Gramain, Lecture Notes in Mathematics 1415, pp. 123–137; the statement is Prop. 2.2, p. 124. The volume's articles number independently, so a citation must name the article. Cahen–Chabert reach the same case only as an exercise, and attribute it to this proposition.

Harman and Hopkins — the q-deformation, and then both directions

Deforming the coefficients rather than the grid gives the quantum question: which P ∈ ℚ(q)[x] satisfy P([n]_q) ∈ ℤ[q]? Their §1 answers it on the additive grid of q-integers, with a free basis of q-binomial polynomials — Pólya's theorem, deformed. Their §4 then takes the nodes over all of ℤ rather than ℕ, inverting q in the coefficients: the bilateral form, which is the one this record needs.

And their §4 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. Their own closing observation is that adjoining square roots K² = z, v² = q produces the Cartan part of Lusztig's integral form of U_v(sl₂). That is this record's setting, arrived at from the other side: the programme's frame is the square-root cover their remark constructs.

Harman–Hopkins, Quantum integer-valued polynomials, arXiv:1601.06110, read against the arXiv source. Two of their statements are not used here: the freeness of their basis, and the Lusztig identification, which is an unproved remark in the source and is carded as one.

What this record adds to the line

Two additions, each a routine transport of the known theorem. The grid variable is inverted, so the objects are Laurent polynomials — at a grid of units this is a simple clearing argument. And the coefficients carry a free parameter t, which arrives from the hybrid family setting the goal was posed in and rides through the argument as a spectator, the integrality test decomposing coefficient-wise. No predecessor is located for that parameter; three independent cards record its absence from the sources.

What is new is that the statement is machine-checked. No theory of integer-valued polynomials, classical or q-deformed, is present in Mathlib — not Pólya's theorem, not a q-analogue. The deliverable of this record is a proof with a clean axiom base, together with a per-entry account of what warrants each piece.

One observation in this record belongs to it and to none of the ancestors: the evenness of the grid is essential, and one value shows it. ν_1 is integral at every node q^χ, and at the odd node v³ takes the value (v²+v+1)/(v+1), which is not in A_t. The divided classes do not survive refinement of the grid, and that is why the goal reads even.

How the three layers relate

The record exists as an informal manuscript, a computational instrument, and a formal development. The register below is what joins them: one entry per result, naming the same object in all three under a stated convention frame.

The instrument and the formal development are two independent implementations, joined by a shared naming discipline. Each stem — nu, grid, expand, newton — carries the same name in the manuscript, in the Julia package and in the Lean sources, and a human reading both is what identifies them. Agreement between the two is established by testing, over the bounds printed in each entry. The kernel certifies the formal statement; the instrument computes and refutes over a stated range; the register records which of the two stands behind each entry.

What warrants what

The grades below are different kinds of claim, and are given equal weight. No declaration in this development refers to the Julia package, and none is planned: a computed entry is warranted by its range and never by the kernel.

A computed entry records the range its computation ran over and an anchor to the certificate, and never the computed values themselves. A reader who wants the values follows the anchor. This edition reports that a claim’s warrant is a bounded computation; it never argues from the computation.

Each warrant below was measured on that entry’s own declaration.

The register

12 entries, every one kept and every one carrying its ancestry. An entry that could not be completed appears with its missing field named: a kept entry that says none shows the register's true extent.

The instrument

The computational layer is a standalone Julia package, GL1Newton, extracted from the development substrate and pinned. It computes the objects the theorem is about, and it is the referee that decides the span identity independently of the proof.

frame()

the base data — K = ℚ(q,t) and the polynomial ring over it

nu(R, r)

the divided class ν_r

grid(R, χ)

the grid point q^χ, two-sided over all of ℤ

nu_grid(R, r, χ)

the value ν_r(q^χ)

expand(R, f)

the Newton coordinates of f, by triangular sweep

az(c)

membership of a scalar in A_t

newton(R, f; window)

grid-integrality as a bounded verdict — it returns the window alongside the answer, so a bounded check can never be read as a proof

mem_span(R, f)

membership in the span Σ A_t ν_r — deciding that this equals newton is the theorem

laurent(R, f)

membership in A_t[Y̌^{±1}], which is strictly smaller

A second module carries the symmetric quantum-bracket family on the v-side; the identity ν_r(q^m) = v^{r(m−r)}·[m,r] is the seam between the two, and it is checked.

Why the instrument is an independent referee. Its newton predicate was originally defined by the very span the theorem computes, which made it unable to referee the theorem. It was redefined by evaluation on the grid, and the independent pin then agreed with the span predicate on every one of the 60 random positives, 5 adversarial seeds and one separator, at window 8.

The acceptance battery runs 87 of 87, re-measured for this edition. Its ranges are printed in the entries that rest on it. To re-run it, instantiate the package against the pinned manifest and call its test suite; the pins are below.

In the record: the package at SandboxA/sandboxA0a/almanac/GL1Newton/ (source src/GL1Newton.jl, battery test/runtests.jl) · the referee pin at SandboxA/sandboxA0a/n1_clause3_referee_pin.jl.

Everything in this edition

85 artifacts. Every one is listed here and every one opens. The rule is that cards travel while sources stay behind as citations: a card is this project's own writing about someone else's statement, carrying the frame under which we read it, and it ships. The source itself is referenced by author, title and section.

Held as references, cited by author, title and section: Gramain (Lecture Notes in Mathematics 1415, pages 123–137), Cahen–Chabert (AMS Surveys 48), Harman–Hopkins (arXiv:1601.06110), De Concini–Procesi, Jantzen, Lusztig, Habiro–Lê, Pólya, Pólya–Szegő, Gauss.

Reproducibility

Pinned by exact revision — a proof that compiles today compiles against that specific library revision.

A re-run at these pins reproduces the symbolic results exactly; the arithmetic is exact in fraction fields over ℤ[q], with no floating point anywhere in the record. Wall-clock time and search order may differ. Where a result is bounded, the bound is part of the claim and is re-runnable at that bound.

Authorship

Tamás Hausel, who directed this work throughout its life. Issued by Project Sandbox.

Authorship here follows direction over the whole life of the work: the statement was fixed and signed before any proving effort was spent, every approval was a human act, and the closure signature is a human act.

The work was produced by software agents operating under a written standard that fixes the statement before the proof, requires a computer-algebra oracle to confirm a statement — including against adversarial inputs — before proving effort is spent, and accepts a result as certified only on the verdict of a proof kernel. No agent approves its own work, and the seat that produces an edition is never the one that accepts it. The editorial work on this edition was done by a software agent under that standard.

Formal results are certified by the Lean 4 kernel. Per-entry warrants are in the register and they are not uniform: the certifier certifies the formal statement and nothing else.

Errata and measurements

Dated 2026-08-13. Everything below was measured directly.

Certification evidence. The closure signature of 2026-07-21 records thirteen certified declarations. The release log it cites contains five and does not contain the endpoint the signature names; a third record gives eight. The log is unaltered since it was hashed into the closure record. Sixteen declarations were checked directly on 2026-08-13 through the Lean language server, and each returned the axiom base propext, Classical.choice, Quot.sound — the standard three, nothing else.

The formal source description. The manifest of 2026-07-21 hashes seven files while declaring a five-file cone, and declares the non-degeneracy witnesses absent from the tree. They are in the tree, committed 2026-07-20, and were checked clean.

The acceptance battery. Recorded as 70/70 in three places; the test file contains 83 test statements; a re-run on 2026-08-13 gave 87/87.

Corrections to this edition. Four entries were first written as “no predecessor located” with no search behind them; searches were then run and predecessors were found for three. A convention dictionary in the ancestry section was written inverted, stating the base ring with q where the signed statement has v. A witness printed against the span identity — ν_1(q³) — was false in the current frame, having been carried over from a card written in the retired notation; the true witness is ν_1(v³) = (v²+v+1)/(v+1), at an odd node. A claim that the additive-to-multiplicative substitution is not a lattice isomorphism was false; it is one.

A withdrawn certificate, and what it cost. This edition asserted that Gramain's normalisation differed from ours by a unit, and obtained a computer-algebra certificate for it. The certificate was sound and the claim was wrong: the formula typed into it carried a dropped minus sign, invisible at ordinary resolution and absent from the scan's text layer. Gramain divides where the transcription multiplied, so his classes are ours exactly. A certificate establishes its input, not its source. The claim and the certificate are withdrawn; the matter was settled instead from a sentence on the printed page — “On voit que G_n(q^n) = 1” — which forces the sign without needing to read the glyph.