Broken paired signs — instance data

Definition

HodgeComputerOffPaired

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

algebraic-geometryhodge-computeroff-paired

The exact fixed polynomials and pole parameter for “Broken paired signs”, 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}^{2} X_{1} X_{2} Y_{0} Y_{2}}{3} + \frac{X_{1}^{3} X_{2} Y_{1} Y_{2}}{2}.

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

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.OffPaired
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)) ^ (2 : ℕ)) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 3 : ℂ))) + ((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)) ^ (3 : ℕ)) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ)))
def q : ℕ := 1
end HodgeComputer.OffPaired

Source

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

Read-back

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

HodgeComputer.OffPaired.n. This declaration defines the natural-number constant $n$ to be $5$ . It has no parameters or hypotheses.

HodgeComputer.OffPaired.d. This declaration defines the natural-number constant $d$ to be $6$ . It has no parameters or hypotheses.

HodgeComputer.OffPaired.F. This declaration, with no parameters or hypotheses, defines the polynomial $F$ in the ring $\mathbb C[x_0,x_1,x_2,x_3,x_4,x_5]$ , where $x_i$ is the indeterminate indexed by $i\in\{0,1,2,3,4,5\}$ , by $F=x_0^6+\frac12 x_0^3x_1x_3x_4+\frac13 x_0^2x_1x_2x_3x_5+x_1^6+\frac12 x_1^3x_2x_4x_5+x_2^6+x_3^6+x_4^6+x_5^6$ . The polynomial ring has six indeterminates because its index set consists of the natural numbers less than $n+1$ , with $n=5$ ; its coefficients, including $\frac12$ and $\frac13$ , are complex numbers.

HodgeComputer.OffPaired.A. This declaration, with no parameters or hypotheses, defines the polynomial $A=x_0^3x_3^3$ in $\mathbb C[x_0,x_1,x_2,x_3,x_4,x_5]$ , where $x_i$ is the indeterminate indexed by $i\in\{0,1,2,3,4,5\}$ . The polynomial ring has complex coefficients and six indeterminates because its index set consists of the natural numbers less than $n+1$ , with $n=5$ .

HodgeComputer.OffPaired.q. This declaration defines the natural-number constant $q$ to be $1$ . It 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