Cyclic triple cover · complementary character — instance data

Definition

HodgeComputerCyclicTripleResidual

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

algebraic-geometrycyclic-triple-residualhodge-computer

The exact fixed polynomials and pole parameter for “Cyclic triple cover · complementary character”, over $\mathbb C$ with coordinates $X_0,X_1,X_2,Y_0,Y_1,Y_2$ :

F=X_2^6+t\cdot X_2^3\cdot C+H.

q=1,\qquad A=X_0^3\cdot Y_0^3.

where

\begin{aligned} t&=\frac57 \\ C&=X_{0}^{3} + X_{0} \cdot Y_{1} \cdot Y_{2} + X_{1} \cdot Y_{0} \cdot Y_{1} \\ H&=X_{0}^{6} + \frac{5}{7}\cdot X_{0}^{3}\cdot X_{1}\cdot Y_{0}\cdot Y_{1} + \frac{5}{7}\cdot X_{0}^{2}\cdot Y_{0}\cdot Y_{1}\cdot Y_{2}^{2} + \frac{5}{7}\cdot X_{0}\cdot X_{1}\cdot Y_{1}^{3}\cdot Y_{2} + X_{1}^{6} + Y_{0}^{6} + Y_{1}^{6} + Y_{2}^{6} \end{aligned}

Definition code

import Definitions.Def_DiamondCertificate

set_option autoImplicit false
noncomputable section
namespace HodgeComputer.CyclicTripleResidual
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 := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((((5 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * (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))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (6 : ℕ))) + ((((((5 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (6 : ℕ))) + ((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 : ℕ)))
def q : ℕ := 1
end HodgeComputer.CyclicTripleResidual

Source

https://github.com/hodge-computer/sextics/blob/83fbf5c9a0afe9136ce4f1ed324d085a2c899bd0/data/cyclic-triple-residual/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_1Y_0Y_1+X_0^3X_2^3+X_0^2Y_0Y_1Y_2^2\\ &\qquad+X_0X_1Y_1^3Y_2+X_0X_2^3Y_1Y_2+X_1X_2^3Y_0Y_1\bigr). \end{aligned}

The definition $A$ is the element $A=X_0^3Y_0^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