Four plus two · suspension remainder — instance data

Definition

HodgeComputerFourPlusTwoResidual

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

algebraic-geometryfour-plus-two-residualhodge-computer

The exact fixed polynomials and pole parameter for “Four plus two · suspension remainder”, over $\mathbb C$ with coordinates $X_0,X_1,X_2,Y_0,Y_1,Y_2$ :

F=H+B.

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

where

\begin{aligned} H&=X_{0}^{6} + \frac{5}{7}\cdot X_{0}^{5}\cdot X_{1} + \frac{5}{7}\cdot X_{0}^{3}\cdot X_{1}\cdot Y_{0}\cdot Y_{1} + \frac{10}{7}\cdot X_{0}\cdot X_{1}^{5} + \frac{10}{7}\cdot X_{0}\cdot X_{1}\cdot Y_{0}^{3}\cdot Y_{1} + X_{1}^{6} + Y_{0}^{6} + \frac{5}{7}\cdot Y_{0}^{5}\cdot Y_{1} + \frac{15}{7}\cdot Y_{0}\cdot Y_{1}^{5} + Y_{1}^{6} \\ B&=X_{2}^{6} + \frac{15}{7}\cdot X_{2}^{4}\cdot Y_{2}^{2} + \frac{10}{7}\cdot X_{2}^{2}\cdot Y_{2}^{4} + Y_{2}^{6} \end{aligned}

Definition code

import Definitions.Def_DiamondCertificate

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

Source

https://github.com/hodge-computer/sextics/blob/83fbf5c9a0afe9136ce4f1ed324d085a2c899bd0/data/four-plus-two-residual/instance.rec

Read-back

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

The declaration $n$ defines the natural number $5$ .

The declaration $d$ defines the natural number $6$ .

The declaration $F$ defines a polynomial in $R=\mathbb C[z_0,z_1,z_2,z_3,z_4,z_5]$ , where $z_i$ is the variable whose index is $i$ in the six-element index set $\{0,1,2,3,4,5\}$ , by

\begin{aligned}F={}&z_0^6+\tfrac57z_0^5z_1+\tfrac57z_0^3z_1z_3z_4+\tfrac{10}7z_0z_1^5+\tfrac{10}7z_0z_1z_3^3z_4+z_1^6+z_2^6\\&+\tfrac{15}7z_2^4z_5^2+\tfrac{10}7z_2^2z_5^4+z_3^6+\tfrac57z_3^5z_4+\tfrac{15}7z_3z_4^5+z_4^6+z_5^6.\end{aligned}

The declaration $A$ defines the polynomial $A=z_0^3z_3^3$ in $\mathbb C[z_0,z_1,z_2,z_3,z_4,z_5]$ , with the same variable indexing $0$ through $5$ .

The declaration $q$ defines 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