Fermat certificates for every homogeneous odd source
ProvedHodgeComputer.Fermat.certificatealgebraic-geometryfermathodge-computer
For each and every homogeneous polynomial of degree satisfying , the Fermat sextic admits a Diamond certificate: a rational vector field homogeneous of degree , with common denominator relatively prime to , satisfying . Divisibility is in the localization with denominators relatively prime to ; there is no bound on denominator degree.
Preamble
import Definitions.Def_HodgeComputerFermat
Formal statement
theorem HodgeComputer.Fermat.certificate
(q : ℕ) (hq : q = 1 ∨ q = 2)
(A : HodgeComputer.AmbientPoly HodgeComputer.Fermat.n)
(hA : A.IsHomogeneous (HodgeComputer.Fermat.d * q))
(hodd : HodgeComputer.Fermat.OddSource A) :
HodgeComputer.HasCertificate
HodgeComputer.Fermat.F
A
HodgeComputer.Fermat.d
q := by
sorry
Source
Benjamin E. Diamond, Hodge Structures in Sextic Fourfolds Equipped with an Involution, https://arxiv.org/abs/2603.29157, Section 3; subset Euler construction specialized to the sign-flip involution. Formalization: https://github.com/hodge-computer/sextics/blob/39daa1c576de10ace509adb1faa500080a5619a9/formal/lean/HodgeComputer/Constructions/Fermat.lean (site counterpart with inferred degree).