Simultaneous permutations · standard sector — certificate
OpenHodgeComputer.DiagonalPermutation.certificateFor , and the fixed of “Simultaneous permutations · standard sector”, prove the existence of a rational vector field with components homogeneous of degree and common denominator relatively prime to , satisfying . Divisibility is in the localization with denominators relatively prime to . There is no denominator degree bound. More details.
import Definitions.Def_HodgeComputerDiagonalPermutation
theorem HodgeComputer.DiagonalPermutation.certificate :
HodgeComputer.HasCertificate
(n := HodgeComputer.DiagonalPermutation.n)
HodgeComputer.DiagonalPermutation.F
HodgeComputer.DiagonalPermutation.A
HodgeComputer.DiagonalPermutation.d
HodgeComputer.DiagonalPermutation.q := by
sorry
Read-back
What the Lean code literally says, in plain math · GPT-6 (OpenAI Codex; independent auditor)
In the polynomial ring in six algebraically independent variables, corresponding in order to indices , fix the following polynomial:
Set . With the fixed natural-number parameters , , and , the theorem asserts that there exist polynomials such that all of the following hold simultaneously: ; every monomial with nonzero coefficient in has total degree ; every monomial with nonzero coefficient in has total degree ; ; writing for the total degree of , every monomial with nonzero coefficient in has total degree ; for each index , every monomial with nonzero coefficient in has total degree ; every polynomial dividing both and is a nonzero constant; and the following exact identity holds in :
Here , and the partial derivatives are formal polynomial derivatives. The homogeneity conditions concern total monomial degree and allow any to be zero. The nonnegative integer is unrestricted, so a nonzero constant denominator is allowed. There is no separately imposed homogeneity or degree condition on , and is allowed. All coefficients of the existentially quantified polynomials may be complex. The assertion is existence, with no uniqueness claim and no additional hypotheses.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.