{"id":"palomar/PALOMAR-2026-10-21-000012","url":"https://github.com/stalex444/pdt-hermite-signature-compositum/tree/5aa870e98236ba240561b798265c629df8c2d031","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000012-v1.json","repo":"https://github.com/stalex444/pdt-hermite-signature-compositum","tags":["math.NT","math-ph","gr-qc","cs.LO","msc:11E10","msc:11E12","msc:12D10","msc:11R04","msc:11R29","msc:11R21"],"score":0,"title":"Hermite's signature theorem and the coprime compositum, with the degree-12 compositum of x^3 - x - 1 and x^4 - x - 1","trust":"high","domain":"math.NT","source":"palomar","authors":["Stephanie Alexander"],"reviews":0,"subject":"math.NT","summary":"Kernel-checked proofs, in Lean 4 + Mathlib, of six general theorems and twelve statements about one number field. General: (1) Hermite's signature theorem for every real polynomial f, degenerate case included and with no monic hypothesis: the power-sum Hankel (Hermite) form H_f has sigPos = #R + #C+, sigNeg = #C+, rank sigPos + sigNeg = #D and radical of dimension deg f - #D, where D, R, C+ are the distinct complex roots, the real ones, and those in the upper half plane; (2) its number-field form (classical, Hermite-Sylvester; in number-field form credited to O. Taussky 1968): the trace form…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"Mathlib: NumberTheory/NumberField/Discriminant/Different.lean and RingTheory/DedekindDomain/LinearDisjoint.lean","identifier":"Mathlib commit 065356127b1dc0016f66b7283ce0ce2c4055aa55 (2026-09-16); PRs #25792 (Yang, 2025-06), #29770, #29885, #29940, #29943 (Roblot, 2025-09..11)","relationship":"adapts"}]}