Simultaneous permutations · standard sector — instance data

Definition

HodgeComputerDiagonalPermutation

by benediamond · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrydiagonal-permutationhodge-computer

The exact fixed polynomials and pole parameter for “Simultaneous permutations · standard sector”, over $\mathbb C$ with coordinates $X_0,X_1,X_2,Y_0,Y_1,Y_2$ :

F=F_0+\frac57\cdot O_1+\frac5{11}\cdot O_2+\frac5{13}\cdot O_3.

q=1,\qquad A=X_{0}^{3} \cdot Y_{0}^{3} - X_{1}^{3} \cdot Y_{1}^{3}.

where

\begin{aligned} F_0&=\sum_{i=0}^{2}(X_i^6+Y_i^6) \\ \mathcal P&=\{(i,j,k):\{i,j,k\}=\{0,1,2\}\} \\ O_1&=\sum_{(i,j,k)\in\mathcal P}X_i^3\cdot X_j\cdot Y_i\cdot Y_j \\ O_2&=\sum_{(i,j,k)\in\mathcal P}X_i^3\cdot X_j\cdot Y_k^2 \\ O_3&=\sum_{(i,j,k)\in\mathcal P}Y_i^3\cdot Y_j\cdot X_k^2 \end{aligned}

Definition code

import Definitions.Def_DiamondCertificate

set_option autoImplicit false
noncomputable section
namespace HodgeComputer.DiagonalPermutation
def n : ℕ := 5
def d : ℕ := 6
def F : HodgeComputer.AmbientPoly n := (((((((((((((((((((((((((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (6 : ℕ)) + ((((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 11 : ℂ))) + ((((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 11 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 13 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 13 : ℂ))) + ((((((5 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 11 : ℂ))) + ((((((5 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 11 : ℂ))) + ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (6 : ℕ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 11 : ℂ))) + ((((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 13 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 13 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 11 : ℂ))) + ((((((5 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (6 : ℕ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 13 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 13 : ℂ))) + ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (6 : ℕ))) + ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (6 : ℕ))) + ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (6 : ℕ)))
def A : HodgeComputer.AmbientPoly n := ((((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ)) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) - (((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ)) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))))
def q : ℕ := 1
end HodgeComputer.DiagonalPermutation

Source

https://github.com/hodge-computer/sextics/blob/83fbf5c9a0afe9136ce4f1ed324d085a2c899bd0/data/diagonal-permutation/instance.rec

Read-back

What the Lean code literally says, in plain math · GPT-6 (OpenAI Codex; independent auditor)

The definition $n$ is the natural number $5$ .

The definition $d$ is the natural number $6$ .

The definition $F$ is the following element of the polynomial ring $R=\mathbb C[X_0,X_1,X_2,Y_0,Y_1,Y_2]$ in six algebraically independent variables, corresponding in order to indices $0,1,2,3,4,5$ :

\begin{aligned} F={}&X_0^6+X_1^6+X_2^6+Y_0^6+Y_1^6+Y_2^6\\ &+\frac57\bigl((X_0^3X_1+X_0X_1^3)Y_0Y_1+(X_0^3X_2+X_0X_2^3)Y_0Y_2\\ &\qquad+(X_1^3X_2+X_1X_2^3)Y_1Y_2\bigr)\\ &+\frac5{11}\bigl((X_0^3X_1+X_0X_1^3)Y_2^2+(X_0^3X_2+X_0X_2^3)Y_1^2\\ &\qquad+(X_1^3X_2+X_1X_2^3)Y_0^2\bigr)\\ &+\frac5{13}\bigl(X_0^2(Y_1^3Y_2+Y_1Y_2^3)+X_1^2(Y_0^3Y_2+Y_0Y_2^3)\\ &\qquad+X_2^2(Y_0^3Y_1+Y_0Y_1^3)\bigr). \end{aligned}

The definition $A$ is the element $A=X_0^3Y_0^3-X_1^3Y_1^3$ of $\mathbb C[X_0,X_1,X_2,Y_0,Y_1,Y_2]$ , where $(X_0,X_1,X_2,Y_0,Y_1,Y_2)$ are the six polynomial variables corresponding in order to indices $0,1,2,3,4,5$ .

The definition $q$ is the natural number $1$ .

Human review

Endorsed by Shuze Chen · Nov 6, 2026
Confirmed by the moderator at approval.
Endorsed by benediamond · Nov 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph