Cyclic coupling · pole order two — instance data

Definition

HodgeComputerCycleQ2

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

algebraic-geometrycycle-q2hodge-computer

The exact fixed polynomials and pole parameter for “Cyclic coupling · pole order two”, over $\mathbb C$ with coordinates $X_0,X_1,X_2,Y_0,Y_1,Y_2$ :

F=F_0 + \frac{X_{0}^{3} X_{1} Y_{0} Y_{1}}{2} + \frac{X_{0} X_{2}^{3} Y_{0} Y_{2}}{2} + \frac{X_{1}^{3} X_{2} Y_{1} Y_{2}}{2}.

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

where

\begin{aligned} F_0&=X_0^6+X_1^6+X_2^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.CycleQ2
def n : ℕ := 5
def d : ℕ := 6
def F : HodgeComputer.AmbientPoly n := ((((((((((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (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 / 2 : ℂ))) + (((((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 / 2 : ℂ))) + ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (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 / 2 : ℂ))) + ((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)) ^ (2 : ℕ)) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6)))
def q : ℕ := 2
end HodgeComputer.CycleQ2

Source

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

Read-back

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

HodgeComputer.CycleQ2.n is the natural-number constant $n=5$ ; this definition has no parameters or hypotheses.

HodgeComputer.CycleQ2.d is the natural-number constant $d=6$ ; this definition has no parameters or hypotheses.

HodgeComputer.CycleQ2.F is the polynomial $F=\sum_{i=0}^{5}z_i^6+\frac12 z_0^3z_1z_3z_4+\frac12 z_0z_2^3z_3z_5+\frac12 z_1^3z_2z_4z_5$ in the polynomial ring $\mathbb C[z_0,z_1,z_2,z_3,z_4,z_5]$ , where $z_i$ is the formal indeterminate with index $i$ in $\{0,1,2,3,4,5\}$ . The ambient polynomial type uses the constant $n=5$ and therefore has $n+1=6$ indeterminates; each coefficient $\frac12$ is the complex number $1/2$ . This definition has no parameters or hypotheses and defines a formal polynomial, with no restrictions on values that might later be substituted for its indeterminates.

HodgeComputer.CycleQ2.A is the polynomial $A=z_0^2z_1^2z_2^3z_3^2z_4^2z_5$ in the polynomial ring $\mathbb C[z_0,z_1,z_2,z_3,z_4,z_5]$ , where $z_i$ is the formal indeterminate with index $i$ in $\{0,1,2,3,4,5\}$ . The ambient polynomial type uses the constant $n=5$ and therefore has $n+1=6$ indeterminates. This definition has no parameters or hypotheses and defines a formal polynomial, with no restrictions on values that might later be substituted for its indeterminates.

HodgeComputer.CycleQ2.q is the natural-number constant $q=2$ ; this definition has no parameters or hypotheses.

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