{"id":"palomar/PALOMAR-2026-10-30-000002","url":"https://github.com/stalex444/bds-dixon-additive-relations/tree/2d422c1b10e3823105ae6f3b68a439dee6f8d4a7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000002-v1.json","repo":"https://github.com/stalex444/bds-dixon-additive-relations","tags":["math.NT","math.RT","cs.LO","msc:11R04","msc:11R32","msc:20B20","msc:20C15","msc:68V20"],"score":0,"title":"The additive theorem for 2-transitive Galois groups (Girstmair; Dixon, Theorem 1') and its representation-theoretic engine","trust":"high","domain":"math.NT","source":"palomar","authors":["Stephanie Alexander"],"reviews":0,"subject":"math.NT","summary":"Kernel-checked proofs, in Lean 4 + Mathlib, of the homogeneous case and, at the roots, of the printed form (relations with value in K), with coefficients in any field K of characteristic 0, of the additive theorem for 2-transitive Galois groups (Girstmair, Manuscripta Math. 39 (1982) 81-97, Proposition 4, Assertion 3, p. 86, for every field whose characteristic does not divide |G|; stated by J. D. Dixon, Acta Arith. 82 (1997) 293-302, as Theorem 1', p. 301, with its proof omitted), of its representation-theoretic engine (classical: Huppert, Endliche Gruppen I, p. 597, Satz 20.2, as cited by…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"Polynomials with nontrivial relations between their roots","identifier":"https://doi.org/10.4064/aa-82-3-293-302","relationship":"formalizes"},{"title":"Linear dependence of zeros of polynomials and construction of primitive elements","identifier":"https://doi.org/10.1007/BF01312446","relationship":"formalizes"},{"title":"Linear relations between roots of polynomials","identifier":"https://doi.org/10.4064/aa-89-1-53-96","relationship":"formalizes"}]}