almanacA0a

The centre of the even hybrid family quantum GL₁

Issued by Project Sandbox · assembled 2026-08-13 · the pilot edition

ACCEPTED deposited 2026-09-17 doi 10.5281/zenodo.22808195 rows freeze at deposit

This is the edition of record, deposited in the EU Open Research Repository as 10.5281/zenodo.22808195 on 2026-09-17; a correction is a new version with its own DOI. It has been accepted by the record's owner as a faithful account of a closed record that claims exactly what its warrants support. Deposit and outward authorisation are both still ahead of it, each a separate human act. Its rows freeze at deposit.

What this is

A complete record of one small mathematical result, in three layers, with a per-claim account of what warrants each one.

For G = GL₁: the even hybrid family integral form is an A_t-subalgebra; the Harish–Chandra projection restricts to an isomorphism Z(U^ev) ≅ (N^ev)^W; and the even Newton lattice is exactly the A_t-span of the shifted divided classes. The three layers are an informal manuscript, a Julia instrument, and a Lean development.

What makes this an almanac is the concordance below: one row per result, joining the three layers under a convention frame in which all the names denote one object, and recording per row what actually certifies it. The concordance performs the alignment a reader would otherwise do by hand; that joining is what makes these three layers an edition.

The scope of the claim

GL₁ is the degenerate case, and the edition says so first. The root system is empty, the Weyl group trivial, the algebra commutative, and the Harish–Chandra projection the identity map. The value of this record is that a small true statement was carried end to end — signed before it was proved, refereed, kernel-certified, refuted where false, and edited into a form a stranger can check — and that the cost and the failure modes were measured. The rank ≥ 2 cases are the open frontier and nothing here settles them.

A tested agreement is not a proof. The Julia and Lean layers are two independent implementations joined by a naming discipline, not by a checked morphism. No object in this edition has a machine-checked correspondence between its two realisations.

Ancestry: these manuscripts predate the ancestry rule

The signed goal predates criterion 13 (adopted 2026-08-05); the proof manuscript carries its declaration. Ancestry is therefore discharged at edition level, and the signed file is not touched — its hash is bound into the closure signature, and trading a checkable anchor for a tidier manuscript would be the wrong way round. Every row below carries its own ancestry: a card, or "none located" with the search that failed behind it. Every "none located" in this edition carries the search that produced it.

The certification split

The three grades are distinct kinds of warrant, and the edition keeps them distinct. The warrant describes the row, never the sandbox — the sandbox is closed with a clean axiom triple, and that does not make every row kernel-certified.

grade	rows	what it means
ink — a refereed argument	1 of 12	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.
orange — computed over a declared range	2 of 12	Verified by computation over a stated bound, and over nothing else. The bound is part of the claim.
blue — kernel-certified	9 of 12	A Lean declaration states this row's claim and its `#print axioms` result is exactly the three standard axioms of Lean's kernel — propositional extensionality (`propext`), the axiom of choice (`Classical.choice`) and quotient soundness (`Quot.sound`) — the base every Mathlib proof shares; a certificate is clean when these three are all it needs — with no `sorryAx` and no custom axiom.

Every axiom result was measured first-hand through the Lean language server. The two computed rows are the instrument and the oracle referee pin, and neither could ever be kernel-certified: no Lean declaration states what a Julia program does.

A disclosure the edition carries on its face. This edition cites the sandbox's closure certification, and that record is internally inconsistent about how many declarations were certified — 13 in the signature, 8 in the approval state, 5 in the log it cites, which does not contain the endpoint it names. The mathematics is independently sound: 16 declarations were verified first-hand and every one returned the clean triple. What is defective is the retained evidence, and its repair is a separate act awaiting signature.

The concordance

12 rows · all kept · every row carries ancestry. An incomplete row stays in the edition with its missing field shown as null, so the edition always displays its true state.

A0a-01-clause-i blue — kernel-certified U^ev = N^ev is an A_t-subalgebra of U.

informal: informal/proofv0a.tex · Proposition (clause i), line 111
CAS object: az / newton — closure of grid-integrality under products
Lean: HybridQuantumLean.A1.GL1Newton.clause_i
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: Current Sandbox symbols: q = v^2, t = z^2; A_t = Z[v^{±1}, t^{±1}]; F_t = Q(v)[t^{±1}]; Y̌ = (T^+)^2 with ev_χ(Y̌) = q^χ, unshifted and t-free. NOTE the Lean sources predate the 2026-08-10 migration and are written in the LEGACY symbols (A_z, Q = q^2, z): the Lean 'A_z' IS this row's A_t and the Lean 'Q' IS this row's q. Restated by the edition; the sources were not migrated.
ancestry: lit-harman-q-polya-qbinomial-basis — REFEREED AND CONFIRMED 2026-08-13 from the arXiv source with re-derived probes (the single-pass caveat F-A1 is DISCHARGED). Card written in retired notation; frame restated by the edition (ANCESTRY.md §3.1).
notes: Measured by the Editor 2026-08-13, clean triple, no sorryAx. The proof is the elementary one — N^ev is an intersection of preimages ev_χ^{-1}(A_t) of a subring under ring homomorphisms — and does not depend on the Harman–Hopkins content; the citation is ancestry for the IDEA, not a dependency.

A0a-02-clause-ii blue — kernel-certified The Harish–Chandra projection restricts to an isomorphism of A_t-algebras HC : Z(U^ev) → (N^ev)^W, and this isomorphism is the identity map of N^ev.

informal: informal/proofv0a.tex · Proposition (clause ii), line 134
CAS object: none — No computational claim. U is commutative because Φ = ∅, so HC = id and W is trivial; the content is definitional unwinding, not computation. The ledge
Lean: HybridQuantumLean.A1.GL1Newton.clause_ii
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: As row 01. Three frames must be kept apart and this is the row where they collide: (a) De Concini–Procesi carry the ρ-shift in the map γ and land in k[2P]^W — TWICE the weight lattice — over k(q) with NO integral form and NO family parameter; (b) the programme carries the shift in the COORDINATES; (c) the GL2 card's two-frame trap — N^ev is Newton in the UNSHIFTED Y̌_i = (T_i^+)^2 while s_1-invariance is natural in the SHIFTED coordinates, and ν_d(Y_shifted) seeds are NOT valid inputs. At GL1 the Weyl group is trivial so the invariance condition is VACUOUS; the row is therefore degenerate and proves nothing about higher rank.
ancestry: gl2-hc-image-theorem (ours, the in-programme predecessor the manuscript actually cites) PLUS lit-dcp-generic-harish-chandra-isomorphism and lit-jantzen-harish-chandra-even-torus (the literature ancestors, located 2026-08-10 after the manuscript closed). THE MANUSCRIPT ITSELF CITES ONLY THE FIRST — the edition's ancestry is richer than the manuscript's citation, and states the difference explicitly (ANCESTRY.md §4).
notes: Measured by the Editor 2026-08-13, clean triple. TWO limits a reader must carry: (1) the predecessor card gl2-hc-image-theorem records '✅ FULLY CERTIFIED' AND, in the same field, 'NOT yet: abstract U_A form + necessity/⊆ (λ-transcendence layer), two-variable even-grid bridge' — the tick and the limit travel together; (2) this row is the Φ = ∅ degeneration, where the theorem is nearly trivial. Its value is that it pins the GL1 case of a statement whose rank ≥ 2 cases are the open frontier — not that it is hard.

A0a-03-clause-iii blue — kernel-certified N^ev = S = Σ_{u∈Z} Σ_{r≥0} A_t · Y̌^u ν_r(Y̌) — the even Newton lattice is exactly the A_t-span of the shifted divided classes.

informal: informal/proofv0a.tex · Theorem (thm:iii), line 181
CAS object: newton vs mem_span — agreement of the evaluation-defined predicate with the span-defined predicate
Lean: HybridQuantumLean.A1.GL1Newton.Nev_eq_span
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: As row 01, PLUS the transport that makes the citation apply at all. Their grid is ADDITIVE (integrality imposed at the q-integers x = [n]_q); ours is MULTIPLICATIVE (Y̌ = q^m). The two are exchanged by the node-preserving substitution Y̌ = 1 + (q−1)x, which is invertible over Q(q) but not over Z[q^{±1}], so it does NOT map Z[q^{±1}][x] into Z[q^{±1}][Y̌]. Because integrality is imposed AT THE NODES and the nodes correspond, the substitution nevertheless carries their lattice ISOMORPHICALLY onto ours, taking each of their basis elements to nu_k(Y̌) term by term. (Corrected 2026-08-13: this edition previously denied it was a lattice isomorphism, which was false — the transport is legitimate precisely because it is one; what fails is only the naive map of coefficient lattices.) Their Gaussian binomial is ONE-SIDED (differs from the symmetric convention by a unit power of q: integrality survives, explicit coefficients do not). Their §1 works over Z[q], a PROPER subring of A_t; the bilateral statement needed here is §4, where the localization inverts q ONLY — not t, not cyclotomic factors. NAME COLLISION, and the migration made it worse: their z is our Y̌; our free parameter is t; today's letter z is the square root of t.
ancestry: lit-harman-q-polya-qbinomial-basis (refereed and CONFIRMED 2026-08-13; F-A1 DISCHARGED — C1 referee pass run 2026-08-13, both cards CONFIRMED with no correction from the arXiv LaTeX source with re-derived probes; report corpus/reports/HARMAN-HOPKINS-C1-REFEREE-PASS-2026-08-13.md. TWO LIMITS SURVIVE, properties of the source not defects: the lattice-FREENESS probe is unrun (two-way integrality does not give equality of lattices), and the Lusztig-Cartan-form sentence stays an unproved remark, grade literature-remark) + lit-harman-bilateral-q-integer-localization (the pre-existing 2026-07-16 card, NOT under that caveat). The manuscript transports the argument; it does not import the theorem.
notes: Measured by the Editor 2026-08-13, clean triple. This is the substantive theorem of the sandbox. TWO things the edition will not let a reader conflate: (1) it must NOT be read as 'the Harman–Hopkins lattice IS our Newton lattice' — the four-way lattice reconciliation T^Lus = N = T_WN = T_HH is OPEN on the shelf (F-A3); (2) the finite degree d is ESSENTIAL to the §4 integrality test, which is what licenses the manuscript's WINDOWED reverse inclusion — that is load-bearing, not a convenience. Non-vacuity is separately proved: see row 08. SPAN, NOT BASIS, AND IT CANNOT BE UPGRADED: the generating family is provably NOT independent — from nu_1(X) = (X−1)/(q−1) one gets the A_t-relation (q−1)·nu_1(Ycheck) − Ycheck·nu_0 + nu_0 = 0. Harman-Hopkins prove FREE generation over Z[q]; clause (iii) asserts only equality of a lattice with a span, which is the correct and weaker form. 'Basis', 'free module' and 'freely generated' must never be written beside this row. What remains open is whether N^ev is free over A_t on some OTHER family — not whether this one is free, which is settled in the negative.

A0a-04-lemma-grid blue — kernel-certified For all m ∈ Z and r ≥ 0, B_r(m) = ν_r(q^m) ∈ Z[q^{±1}] — the grid values of the divided classes are integral, including at negative nodes.

informal: informal/proofv0a.tex · Lemma (lem:grid), line 194
CAS object: nu_grid + az — integrality of ν_r(q^χ) on the bilateral grid
Lean: HybridQuantumLean.A1.GL1Newton.Az_nuGrid
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: As row 03. The one-sided Gaussian convention is what the grid values are expressed in; the basis denominator q^{binom(k,2)}[k]_q! is where a normalisation error would hide, which is why it was probed on the oracle (49/49 over 0 ≤ n,k ≤ 6).
ancestry: lit-harman-q-polya-qbinomial-basis (refereed and CONFIRMED 2026-08-13; F-A1 DISCHARGED — C1 referee pass run 2026-08-13, both cards CONFIRMED with no correction from the arXiv LaTeX source with re-derived probes; report corpus/reports/HARMAN-HOPKINS-C1-REFEREE-PASS-2026-08-13.md. TWO LIMITS SURVIVE, properties of the source not defects: the lattice-FREENESS probe is unrun (two-way integrality does not give equality of lattices), and the Lusztig-Cartan-form sentence stays an unproved remark, grade literature-remark) + the programme companion card even-newton-gaussian-grid-values. THE COMPANION CARD IS CITED FOR FORWARD GRID-INTEGRALITY ONLY: its stronger sentence — that the even-generated span EQUALS the Verma-saturated Newton lattice — is REFUTED (even-gaussian-span-not-newton-lattice-refuted), CORRECTED 2026-08-13, the printed witness was FALSE in this frame: nu_1(q^3) = q^2+q+1 IS integral. The true witness sits on the ODD grid — nu_1(v^3) = (v^2+v+1)/(v+1) is NOT in A_t — which is precisely why the goal reads 'even'. Verified on the CAS kernel, identity sha256 0f8f7d63dd6a37e4886d7cbb71edfc9e1f503705e3354bb52f25692f676eb64d. The false form was transported from the card, whose own frame is the RETIRED notation where its q is today's v; restating it without migrating the symbol is the inverted-dictionary defect recurring. Forward integrality on a grid never implies saturation of the lattice. CLASSICAL ANCESTOR NOW HELD (2026-08-13): Gramain, LNM 1415, §2 Prop 2.2, p. 124 — the Gauss binomial polynomials generating the multiplicative-grid integer-valued module; our nu_r IS his G_r exactly. CORRECTED 2026-08-13 (reverse pass): Gramain's printed exponent is NEGATIVE — he DIVIDES by q^{n(n-1)/2} where this edition first read him as multiplying. So G_n = nu_n EXACTLY: his normalization IS ours, not ours up to a unit. SETTLED FROM THE PAGE'S OWN CONTENT, independent of the glyph: p.125 states 'On voit que G_n(q^n) = 1', and nu_n(q^n) = 1 by construction, so the exponent MUST be negative — a positive one would give G_n(q^n) = q^{n(n-1)}. WITHDRAWN: the earlier claim 'G_n = q^{n(n-1)} * nu_n' and its CAS certificate b058e9158de16756c6f9fe4f2a9660f74402f0fea850bd3602aa46e225236e04. The certificate is not false — it faithfully certifies the identity for the formula that was TYPED INTO IT, which carried a dropped minus. A MACHINE CERTIFICATE CERTIFIES ITS INPUT, NOT THE SOURCE. See gaps/GAPS.md F-A6. The correction makes this row STRONGER: exact coincidence of normalizations, not agreement up to a unit. This upgrades the divided classes' ancestry from a q-deformed analogue to a classical statement on our own grid. CARD: lit-gramain-geometric-progression-integer-valued-basis. CITE BY ARTICLE, NEVER BY VOLUME (trap found by the Librarian, 2026-08-13): LNM 1415 is a VOLUME whose articles number independently, and a naive search for 'Proposition 2.2' in it lands FIRST on a different article's statement about primes p^k dividing a binomial-type coefficient. The citation must read 'Gramain, LNM 1415, Prop 2.2, p. 124' — never 'LNM 1415 Prop 2.2'. ANCESTRY.md §8.6.
notes: Certified via the parent A1 machinery (CenterNewtonZ.nuNewton_zpow_grid_mem), consumed rather than reproved. Independently corroborated over a declared range: ledger claims G1 (0≤m<r≤8), G2 (0≤r≤m≤10), G3 (1≤n≤5, 0≤r≤5), plus battery sweep r ∈ 0..8 × χ ∈ −9..9 = 171 cases, all integral, measured 87/87 PASS on 2026-08-13. The theorem is unbounded; the computations are not, and the edition does not let the second stand in for the first.

A0a-05-lemma-fwd blue — kernel-certified For every u ∈ Z and r ≥ 0, Y̌^u ν_r(Y̌) ∈ N^ev; hence S ⊆ N^ev.

informal: informal/proofv0a.tex · Lemma (lem:fwd), line 254
CAS object: newton on nuGen witnesses
Lean: HybridQuantumLean.A1.GL1Newton.Newton_nuGen
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: As row 03.
ancestry: lit-harman-q-polya-qbinomial-basis (refereed and CONFIRMED 2026-08-13; F-A1 DISCHARGED — C1 referee pass run 2026-08-13, both cards CONFIRMED with no correction from the arXiv LaTeX source with re-derived probes; report corpus/reports/HARMAN-HOPKINS-C1-REFEREE-PASS-2026-08-13.md. TWO LIMITS SURVIVE, properties of the source not defects: the lattice-FREENESS probe is unrun (two-way integrality does not give equality of lattices), and the Lusztig-Cartan-form sentence stays an unproved remark, grade literature-remark).
notes: The easy leg of clause (iii). Corroborated over declared ranges −2≤u≤2, 0≤r≤4, −3≤m≤4 (ledger F2/F3), with a control (control.coefficientwise-coarsening at r=2) that must and does REFUTE.

A0a-06-lemma-rev blue — kernel-certified If g ∈ N^ev is an even toral POLYNOMIAL of degree ≤ d, then g = Σ_{r≤d} c_r ν_r(Y̌) with all c_r ∈ A_t. The windowed reverse inclusion.

informal: informal/proofv0a.tex · Lemma (lem:rev), line 276
CAS object: expand — the triangular Newton-coordinate sweep
Lean: HybridQuantumLean.A1.GL1Newton.mem_span_of_Newton
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: As row 03, and THE FINITE DEGREE d IS ESSENTIAL — Harman–Hopkins Lemma 4.2 tests integrality at nodes 0..d and concludes for all of Z. The window is a hypothesis of the source, not an artefact of our proof.
ancestry: lit-harman-q-polya-qbinomial-basis (refereed and CONFIRMED 2026-08-13; F-A1 DISCHARGED — C1 referee pass run 2026-08-13, both cards CONFIRMED with no correction from the arXiv LaTeX source with re-derived probes; report corpus/reports/HARMAN-HOPKINS-C1-REFEREE-PASS-2026-08-13.md. TWO LIMITS SURVIVE, properties of the source not defects: the lattice-FREENESS probe is unrun (two-way integrality does not give equality of lattices), and the Lusztig-Cartan-form sentence stays an unproved remark, grade literature-remark) + lit-harman-bilateral-q-integer-localization (refereed status: pre-existing 07-16 card).
notes: The substantive leg. The Lean 'expand' was introduced to close a faithfulness finding and is re-verified non-circular (it never mentions span, Newton or nuGenSet). Corroborated at window size d = 8 (ledger R1/R2), with control.offdiagonal-not-one at (3,2) refuting as required. CAVEAT for the embedding: whether the Julia expand's truncation parameter D agrees with the Lean expand has NEVER been examined (gap G2).

A0a-07-definition-1-presented blue — kernel-certified U is the F_t-algebra on invertible pairwise commuting K_{n,±} with K_{0,±}=1, K_{m+n,±}=K_{m,±}K_{n,±}, K_{n,+}K_{n,−}=t^n; and the monomials (T^+)^w, w ∈ Z, form an F_t-basis.

informal: informal/goalv0a.tex · Definition 1 (def:U)
CAS object: none — No computational claim; this is a presentation.
Lean: HybridQuantumLean.A1.GL1Newton.Presentation.equivTorus
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: Split torus, z_i free, unshifted Verma — the programme-wide convention. The presented algebra is a quotient of the group algebra K[Z × Z] by the SINGLE remaining relation K_{1,+}K_{1,−} = t; the full family K_{n,+}K_{n,−} = t^n is DERIVED, not imposed.
ancestry: SPLIT, and the split is the finding (edition-level search, 2026-08-13). PRESENTATION HALF — PREDECESSOR LOCATED: Lusztig, Introduction to Quantum Groups, Proposition 3.2.4, via card lit-lusztig-triangular-decomposition-toral-freeness. The algebra on invertible commuting generators indexed additively by a lattice, identified with that lattice's group algebra. CITE THE PARENTHESIS: the freeness on {K_mu} is stated in Lusztig's parenthetical '(This is the group algebra of Y over Q(v).)', not in the displayed statement — a citation omitting it supports a presentation but not a basis. FAMILY-PARAMETER HALF — NONE LOCATED: no predecessor anywhere on the shelf for the second leg K_{n,-} together with an adjoined free invertible t satisfying K_{1,+}K_{1,-} = t. This is a POSITIVE absence, not a silent zero-hit: three independent cards assert it as a frame fact (lit-dcp-generic-harish-chandra-isomorphism 'no family parameter'; lit-dcp-verma-contravariant-shapovalov 'no family parameter'; the Losev-Tsymbaliuk-Vu transcript 'no central group-like z_a'). Nearest structural neighbour, and NOT a predecessor: Lacabanne's double Cartan, whose second parameter is the QUOTIENT z_i = K_i L_i^{-1}, a central root-torus variable, not an adjoined free one. Our own predecessor for this half is ours: the internal note own-habiro-le-even-hybrid-centers-explicit-torus §2, with the registry entry objects/gl4.coordinate-split-torus — both pinned by this edition's manifest and NOT distributed with it (they carry the programme's general conjecture, which is work in preparation). SEARCH OF RECORD: queries 'group algebra of the weight lattice torus Laurent Cartan part K_i invertible' (0), 'hybrid family torus' (0), 'K_n^+ K_n^-' (0), 'hybrid torus' (11), 'Cartan part' (30), 'split torus' (6), 'z_i = K_{i,+}K_{i,-}' (0), 'group algebra' (10), 'central group-like z_a' (0), 'family parameter' (9), 'generators and relations' (33); statements + objects shelves; 2026-08-13. No acquisition warranted — the absence is structural, not a gap in holdings.
notes: This row is why the goal bundle grew from four fields to eight. Wave 2 ASSUMED the presented algebra was the Laurent torus; wave 3 PROVED it (equivTorus), closing finding F1. The universal property is established for commutative target algebras only — recorded on the record as verification finding N2, not a sorry.

A0a-08-nondegeneracy blue — kernel-certified Clause (iii) is not vacuously true of a degenerate object: A_t[Ycheck^{±1}] ⊊ N^ev ⊊ K_1[Ycheck^{±1}] — strictly, on both sides, with K_1 = Frac(A_t) the ambient the certified declaration actually uses.

informal: — · Proved in the formal development; the manuscript states no counterpart.
CAS object: the separating witness: nu_1 is grid-integral and in the span, and is not Laurent
Lean: HybridQuantumLean.A1.GL1Newton.clause_iii_nondegenerate
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: As row 01. The separator is ν_1(Y̌) = (Y̌ − 1)/(q − 1), whose Y̌-coefficient (q−1)^{-1} escapes A_t while all its GRID values stay integral — which is exactly why the Newton lattice is strictly larger than the Laurent ring and the divided classes are genuinely needed.
ancestry: PREDECESSORS LOCATED, in three layers, with one caution (edition-level search, 2026-08-13). CLASSICAL: Polya 1919, via the held transcript harman-hopkins-quantum-integer-valued-polynomials, Proposition 1.1 — 'R is freely generated as an abelian group by the binomial polynomials binom(x,k)'. NOTE THE LOGICAL GAP AND DO NOT CLOSE IT SILENTLY: the source states a BASIS, not a strict inclusion. Strictness follows immediately (binom(x,2) is integer-valued and not in Z[x]), so the honest phrasing is "Polya's basis theorem, from which the strict containment is immediate", NEVER "Polya proved the strict containment". q-ANALOGUE: Harman-Hopkins §1 Props 1.1-1.2 via lit-harman-q-polya-qbinomial-basis (refereed and CONFIRMED 2026-08-13 from the arXiv source with re-derived probes; F-A1 DISCHARGED — C1 referee pass run 2026-08-13, both cards CONFIRMED with no correction from the arXiv LaTeX source with re-derived probes; report corpus/reports/HARMAN-HOPKINS-C1-REFEREE-PASS-2026-08-13.md. TWO LIMITS SURVIVE, properties of the source not defects: the lattice-FREENESS probe is unrun (two-way integrality does not give equality of lattices), and the Lusztig-Cartan-form sentence stays an unproved remark, grade literature-remark), frame: one variable, ADDITIVE grid, coefficient ring Z[q] or Z[q^{±1}], NO free parameter. OUR OWN, FOR THE WITNESS ONLY: even-gaussian-span-not-newton-lattice-refuted displays the identical separating element nu_1(Ycheck) = (Ycheck-1)/(q-1) and proves a strict inclusion — BUT OF A DIFFERENT PAIR BY A DIFFERENT MECHANISM (it separates the Gaussian-generator span from the Newton lattice via a finer-vs-coarser grid; this row separates A_t[Ycheck^{±1}] from N^ev via a non-unit coefficient (q-1)^{-1}). Predecessor for the witness; NOT for this inclusion. ACQUISITION PARTLY FULFILLED — see below. STILL WANTED: Cahen-Chabert, Integer-Valued Polynomials, AMS Surveys 48 (1997) — the standard reference, cited by our own held source, NOT on our shelf; also Polya 1915 original and Gramain 1990. Until held, the classical statement is reachable only THROUGH a quotation inside another paper, and the edition says so rather than citing what it does not hold. ACQUISITION FULFILLED 2026-08-13: Gramain LNM 1415 is now HELD (conference volume 'Cinquante Ans de Polynomes'), and its §2 PROPOSITION 2.2, printed p. 124, is the classical MULTIPLICATIVE-GRID ancestor: the polynomials P with P(q^k) in Z for all k form the Z-module generated by the Gauss binomial polynomials G_n. CORRECTED 2026-08-13 (reverse pass): Gramain's printed exponent is NEGATIVE — he DIVIDES by q^{n(n-1)/2} where this edition first read him as multiplying. So G_n = nu_n EXACTLY: his normalization IS ours, not ours up to a unit. SETTLED FROM THE PAGE'S OWN CONTENT, independent of the glyph: p.125 states 'On voit que G_n(q^n) = 1', and nu_n(q^n) = 1 by construction, so the exponent MUST be negative — a positive one would give G_n(q^n) = q^{n(n-1)}. WITHDRAWN: the earlier claim 'G_n = q^{n(n-1)} * nu_n' and its CAS certificate b058e9158de16756c6f9fe4f2a9660f74402f0fea850bd3602aa46e225236e04. The certificate is not false — it faithfully certifies the identity for the formula that was TYPED INTO IT, which carried a dropped minus. A MACHINE CERTIFICATE CERTIFIES ITS INPUT, NOT THE SOURCE. See gaps/GAPS.md F-A6. The correction makes this row STRONGER: exact coincidence of normalizations, not agreement up to a unit. FRAME: Gramain's q is a NATURAL NUMBER >= 2 over coefficient ring Z, ours an indeterminate over A_t — so q^{n(n-1)} is a unit for us and not for him; ancestor of the FORM, not a citable instance of our statement. CARD: lit-gramain-geometric-progression-integer-valued-basis (Librarian, 2026-08-13, read at source). CITE BY ARTICLE, NEVER BY VOLUME (trap found by the Librarian, 2026-08-13): LNM 1415 is a VOLUME whose articles number independently, and a naive search for 'Proposition 2.2' in it lands FIRST on a different article's statement about primes p^k dividing a binomial-type coefficient. The citation must read 'Gramain, LNM 1415, Prop 2.2, p. 124' — never 'LNM 1415 Prop 2.2'. See ANCESTRY.md §8.6.
notes: Measured first-hand 2026-08-13: the clean axiom base on the main declaration and on each of the five listed beside it. This row corrects a stale record: the source manifest of 2026-07-21 still carries finding F7 declaring these witnesses absent from the delivered cone and present only in a scratch tree /tmp/v0averify/. They are IN-TREE (NonDegeneracy.lean, committed 2026-07-20 — a day BEFORE the manifest that declares them missing), imported at Sandbox.lean:120, tracked in git, and clean. The scratch tree no longer exists. See F-E3. Three of the four witnesses named in the older record carry different identifiers in the delivered sources.

A0a-09-kz-bridge blue — kernel-certified Enlarging the ambient coefficient RING from F_t = Q(v)[t^{±1}] (not a field) to K_1 = Frac(A_t) = Q(v,t) adds no new Newton elements: the two readings cut out the same set.

informal: — · Proved in the formal development; the manuscript states no counterpart.
CAS object: none — No computational claim; a ring-theoretic containment argument.
Lean: HybridQuantumLean.A1.GL1Newton.KzBridge.Newton_mem_KzAmbient
axioms used: propext · Classical.choice · Quot.sound — the standard three, nothing else
frame: As row 01. The Lean bundle is proved over K_1 = Q(v,t), which STRICTLY CONTAINS the K_t = Q(v)[t^{±1}] that goalv0a Definition 1 names — recorded as finding F4, a strengthening. This row is what makes the strengthening harmless rather than a change of statement.
ancestry: PREDECESSOR LOCATED 2026-08-13, after the acquisition arrived — this row previously read 'none located'. CARD: lit-cahen-chabert-vandermonde-coefficient-descent (Librarian, 2026-08-13, verified at source). CAHEN-CHABERT, Integer-Valued Polynomials, AMS Surveys 48, PROPOSITION I.3.1 with REMARKS I.3.2(i)-(ii), printed p. 9 (section I.3 'Trivial cases', subsection 'Vandermonde' — NOT section I.2 Localization, which is adjacent only). Prop I.3.1: for D a domain in a field L and f of degree n with coefficients in L, if f takes values in D at n+1 points a_0..a_n of D, then d*f is in D[X] where d = prod_{i<j}(a_j - a_i) is the Vandermonde. Remark I.3.2(i) draws exactly this row's claim: 'if E is an infinite subset of K, then a polynomial with coefficients in a LARGER FIELD which maps E into D is in fact a polynomial with coefficients in K. Hence there is no lack of generality in defining Int(E,D) as a subset of K[X].' Remark I.3.2(ii) names the enlarged-ambient object Int(E,D,L) and records that it is a genuinely NEW object only when E is FINITE. Ours is infinite. FRAME: their D is our A_t = Z[v^{±1},t^{±1}] (infinite domain); their K is Frac(A_t) = Q(v,t); their L is any larger field; their E is our multiplicative grid {q^chi : chi in Z}; their Int(E,D) is N^ev. Their hypotheses hold verbatim: the nodes q^chi lie IN the domain, not merely in its fraction field. WHY THE SHARP FORM MATTERS AND THE REMARK ALONE WOULD NOT: Remark I.3.2(i) lands the coefficients in the QUOTIENT FIELD, whereas this row needs them in F_t = Q(v)[t^{±1}], which is NOT a field. Prop I.3.1 is sharper than the remark drawn from it — it lands them in (1/d)*A_t with d an EXPLICIT product of node differences. Since every node is a power of q, that d lies in Z[q^{±1}] and carries NO t, so no t can enter a denominator: the non-field landing is exactly what the explicit Vandermonde gives. ADJACENT AND EXPLICITLY REJECTED (recorded so nobody re-searches them): all of section I.2 (localizes the target domain or the evaluation set, never the ambient); IV.3 Prop IV.3.4 / Cor IV.3.5 pp.82-84 (vary the evaluation SUBRING); section IV.4 (integral closure of Int(E,D), a different question); Ch IV Exercise 3 p.91 (E in F in K with F a subfield — again the evaluation set); and Harman-Hopkins section 4 Prop 4.3, rejected earlier and still rejected. Across the whole book exactly THREE passages vary a field at all, and only p.9 varies the ambient.
notes: These five declarations are the ENTIRE contents of the release log the closure signature cites (finding F-E1). Recorded by design and not a gap: clause (ii) has NO separate K_t form, because Definition 3 takes the centre AFTER base change to Frac(A_t) = K_1, so the centre object's ambient is intrinsically K_1. The three-engine faithfulness panel graded that reading FAITHFUL unanimously across both passes. ANCESTRY UPGRADED 2026-08-13 from 'none located' to a located predecessor (Cahen-Chabert Prop I.3.1, p.9) once the acquisition arrived and was read. The failed search that preceded it is retained in ANCESTRY.md §7.3 as the honest record of what was searched before the book was held — a 'none located' that later resolves is not an error, it is the search working.

A0a-10-instrument orange — computed over a declared range The GL1Newton package computes the object set of goalv0a — the divided classes, the grid, the Newton coordinates, and the three membership predicates — and separates them as the theory requires.

informal: almanac/GL1Newton/README.md · THE INSTRUMENT (adopted into this edition 2026-08-13; ADOPT confirmed by the record owner)
CAS object: the ten GL1Newton stems + the four QFunctions stems
Lean: none — this row's subject is not a Lean statement
declared range: Acceptance battery 87/87, re-measured 2026-08-13 (Oscar 1.8.0, Julia 1.12.6). Ranges: grid integrality r ∈ 0..8 × χ ∈ −9..9 (171 cases); triangularity r ∈ 0..8; bridge identity 0 ≤ r ≤ m ≤ 8 (45 pairs); trap-4 separation k ∈ 0..6; frame controls χ ∈ −4..4, r ∈ 0..4; negative control 171 + 78 cases, all required to FAIL and doing so. newton() default verdict window χ ∈ −12..12.
frame: Current symbols throughout (q, v, t) — the package was migrated on 2026-08-10, unlike the Lean sources and unlike every card. Stems are IDENTIFIERS, not notation: the three-world same-name contract survives the migration by design.
ancestry: AN INSTRUMENT — this row records a Julia package, and criterion 13 binds results, so ancestry is owed by results alone; owing a predecessor search to an instrument would be a category error (ruled at the form level, 2026-08-13). Recorded in this category shape, replacing the field's previous 'none located' wording — an assertion dressed as a finding — corrected 2026-08-13.
notes: NOT kernel-certified and cannot be: NO LEAN DECLARATION STATES THE CODE'S BEHAVIOUR. This is the manifest's §9 rule 1 and the record owner's explicit instruction on adoption — adoption makes the package a row, not a certificate. The 87/87 figure is the Editor's own measurement; three records carry '70/70' and a static count of the test file gives 83 (finding F-E4). The edition ships the number it measured and names the discrepancy rather than repeating a figure it could not reproduce.

A0a-11-n1-referee-pin orange — computed over a declared range Clause (iii) is refereed independently of the proof: the evaluation-defined predicate and the span-defined predicate agree, with no disagreements, on positive samples, adversarial seeds and a separator.

informal: n1_clause3_referee_pin.jl · THE ORACLE GATE for clause (iii) (finding N1 arc, closed 2026-07-21)
CAS object: newton vs mem_span, measured non-circularly
Lean: none — this row's subject is not a Lean statement
declared range: window = 8; 60 random positive samples (x^u ν_r(x), u ∈ 0..5, r ∈ 0..4, coefficients q^{rand(−3..3)} t^{rand(−2..2)}·rand(−5..5)); 5 named adversarial seeds, all required to be REFUTED by both predicates; 1 separator (ν_1, required to be in the lattice and the span but NOT in the Laurent ring); random seed fixed at 20260721. Recorded verdict: PROVED_BOUNDED, disagreements = 0.
frame: Legacy symbols (Q, q, z) — this pin predates the 2026-08-10 migration and was NOT migrated. Its Q is today's q and its z is today's t.
ancestry: AN INSTRUMENT — this row records an oracle run, and criterion 13 binds results, so ancestry is owed by results alone; owing a predecessor search to an instrument would be a category error (ruled at the form level, 2026-08-13). Recorded in this category shape, replacing the field's previous 'none located' wording — an assertion dressed as a finding — corrected 2026-08-13.
notes: THIS ROW EXISTS BECAUSE OF A REAL DEFECT, and the edition prints the defect rather than only the fix. The substrate's original newton() was defined by ν-span, so it could NOT referee clause (iii) — the claim that the evaluation-defined lattice EQUALS the span — without circularity. The oracle gate was therefore unable to confirm the theorem independently of the proof until the predicate was redefined by evaluation. This is the strongest computational evidence in the edition and it is still a BOUNDED verdict about a Julia program (EMBEDDING_NOTE.md §2c).

A0a-12-proof-proves-the-signed-statement ink — a refereed argument The stand-alone proof proves the statement that was signed: proofv0a.tex establishes the three clauses of goalv0a.tex — no clause weakened, none strengthened, no convention changed.

informal: proofv0a.tex · THE CLAIM EVERY OTHER ROW RESTS ON, AND THE ONLY ONE NO MACHINE CAN SETTLE.
CAS object: none — no computational claim
Lean: none — this row's subject is not a Lean statement
frame: Both documents are read in the CURRENT frame (q, v, t; q = v², t = z²). The first referee read the pre-migration text in the legacy frame (Q, q, z); the migration between them was verified mechanically, not by eye, and is recorded in the chain below.
ancestry: AN EDITORIAL FACT ABOUT THIS EDITION'S OWN DOCUMENTS, not a mathematical result with predecessors — ancestry is owed by results, and owing a predecessor search to a document-comparison claim would be the category error ruled at the form level 2026-08-13 for A0a-11.
notes: THIS ROW EXISTS BECAUSE THE EDITION WAS SILENT ON ITS OWN LOAD-BEARING CLAIM. Every other row presupposes that the proof proves the signed statement, and nothing recorded it as a result with a warrant. It cannot be blue: a kernel certifies a formal statement and cannot compare two documents. It cannot be orange: no computation adjudicates whether one text proves another. It is exactly what the ink warrant is for — a written argument, read by an independent adversarial referee — which is also why an edition with zero ink rows was understating its own record rather than reporting it.

What a reader receives

85 artifacts, about 1.0 MB, containing no third-party PDF. The governing rule is that cards travel and sources do not: a card is this project's own writing about someone else's statement, carrying the convention frame under which we read it, and it ships inside the edition. The source itself is referenced by author, title and section, and never redistributed. Shipping a card is attribution; shipping a source would be redistribution.

ships	count
the almanac proper — front matter, concordance, embedding note, ancestry, authorship, manifest, gap list, verdicts	22
statement cards the ancestry resolves to	24
the project's own substrate — manuscripts (TeX and PDF), Lean sources, the Julia instrument with its dependency pin, ledgers, referee and panel reports, closure records	39

Referenced, never redistributed: Gramain (LNM 1415), 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 version — a proof that compiles today compiles against the recorded Mathlib revision.

component	pin
Lean toolchain	`leanprover/lean4:v4.30.0`
Mathlib	`c5ea00351c28e24afc9f0f84379aa41082b1188f (inputRev v4.30.0)`
Julia	`1.12.6` (Manifest is the pin; Project is intent)
OSCAR	`1.8.0` · tree `6da224b10d8658c1…`
estate commit	`a4c04990`

What the recipe does not promise: A pinned toolchain makes a re-run POSSIBLE, not IDENTICAL. Floating-point, parallel scheduling and resource-dependent search may differ. Where a result depends on a bounded search the BOUND IS PART OF THE CLAIM (CONCORDANCE.json declared_range) and must be re-runnable at that bound.

Authorship

Tamás Hausel, who directed this sandbox throughout its life. Issued by Project Sandbox. Authorship follows direction over the whole life of the work: the goal was fixed and signed before any proving budget was spent, every approval gate was a human act, and the closure signature is a human act.

The work was produced by software agents operating under the Project Sandbox Rule — a written standard that fixes the statement before the proof, requires a computer-algebra oracle to confirm a statement 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 seat that accepts it. For this pilot the Almanac Editor's post was discharged by a software agent, and the edition states this explicitly for the reader.

Formal results are certified by the Lean 4 kernel. A result counts as kernel-certified only when its axiom base is exactly the three standard axioms of Lean's kernel — propositional extensionality (propext), the axiom of choice (Classical.choice) and quotient soundness (Quot.sound) — the base every Mathlib proof shares; a certificate is clean when these three are all it needs. Per-row warrants are above and they are not uniform: the certifier certifies the Lean statement and nothing else.

The gap list

The gap list is a permanent part of every edition. It records 15 findings, and the count rose as the edition matured — every finding added after assembly was found by the form, against the edition or its author. An edition whose gap list converges to zero as it matures is one that stopped looking.

Among them: the closure-evidence inconsistency disclosed above; a stale source manifest; a recorded test count that could not be reproduced and was re-measured; and three errors by the Editor — rows claiming "none located" with no search behind them, an inverted convention dictionary written inside the section warning against it, and a machine certificate that faithfully measured a mis-transcribed formula, followed by a retraction that itself overshot. All were caught, every warrant stood unchanged, and each left a recorded lesson.