Prove2Me

Polarized split · K3 remainder — instance data

Definition
HodgeComputerPolarizedK3Remainder

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

algebraic-geometryhodge-computerpolarized-k3-remainder

The exact fixed polynomials and pole parameter for “Polarized split · K3 remainder”, over C\mathbb C with coordinates X0,X1,X2,Y0,Y1,Y2X_0,X_1,X_2,Y_0,Y_1,Y_2:

F=12⋅(f(X+Y)+f(X−Y)).F=\frac12\cdot\bigl(f(X+Y)+f(X-Y)\bigr). q=1,A=X0⋅X1⋅X2⋅Y0⋅Y1⋅Y2.q=1,\qquad A=X_{0} \cdot X_{1} \cdot X_{2} \cdot Y_{0} \cdot Y_{1} \cdot Y_{2}.

where

X=(X0,X1,X2),Y=(Y0,Y1,Y2)t=57f(a,b,c)=a6+b6+c6+t⋅(a5⋅b+2⋅b5⋅c+3⋅c5⋅a+a2⋅b3⋅c)\begin{aligned} X&=(X_0,X_1,X_2),\quad Y=(Y_0,Y_1,Y_2) \\ t&=\frac57 \\ f(a,b,c)&=a^6+b^6+c^6+t\cdot(a^5\cdot b+2\cdot b^5\cdot c+3\cdot c^5\cdot a+a^2\cdot b^3\cdot c) \end{aligned}
Definition code
import Definitions.Def_DiamondCertificate

set_option autoImplicit false
noncomputable section
namespace HodgeComputer.PolarizedK3Remainder
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 : ℂ))) + (((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ)))) + (((((25 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((50 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ)))) + (((((50 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((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 / 7 : ℂ))) + ((((((10 : 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 := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((((30 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((25 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((((30 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((15 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (5 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((150 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((((10 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((75 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (6 : ℕ))) + ((((10 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (5 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ)))) + (((((50 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * (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)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((100 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ)))) + (((((100 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((((15 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((((50 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (6 : ℕ))) + (((((75 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ)))) + (((((150 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + (((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ)))) + ((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 : ℂ))) + (((((5 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((((15 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (5 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (6 : ℕ))) + ((((10 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (5 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 7 : ℂ))) + ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (6 : ℕ)))
def A : HodgeComputer.AmbientPoly n := ((((((MvPolynomial.X (R := ℂ) (0 : Fin 6)) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6)))
def q : ℕ := 1
end HodgeComputer.PolarizedK3Remainder
Source
https://github.com/hodge-computer/sextics/blob/83fbf5c9a0afe9136ce4f1ed324d085a2c899bd0/data/polarized-k3-remainder/instance.rec
Read-back

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

n. The declaration defines the natural number nn to be 55.

d. The declaration defines the natural number dd to be 66.

F. For the fixed value n=5n=5, the declaration defines FF as an element of the polynomial ring C[x0,x1,x2,x3,x4,x5]\mathbb C[x_0,x_1,x_2,x_3,x_4,x_5], where xix_i is the formal indeterminate indexed by i∈{0,1,2,3,4,5}i\in\{0,1,2,3,4,5\}, by the formula

F=∑i=05xi6+15∑i=02(xi4xi+32+xi2xi+34)+17(5x05x1+25x04x3x4+50x03x1x32+5x02x13x2+15x02x12x4x5+15x02x1x2x42+50x02x33x4+5x02x43x5+10x0x13x3x5+30x0x12x2x3x4+25x0x1x34+30x0x1x3x42x5+15x0x25+150x0x23x52+10x0x2x3x43+75x0x2x54+10x15x2+50x14x4x5+5x13x2x32+100x13x2x42+15x12x32x4x5+100x12x43x5+15x1x2x32x42+50x1x2x44+75x24x3x5+150x22x3x53+5x35x4+5x32x43x5+15x3x55+10x45x5).\begin{aligned} F={}&\sum_{i=0}^{5}x_i^6+15\sum_{i=0}^{2}\bigl(x_i^4x_{i+3}^2+x_i^2x_{i+3}^4\bigr)\\ &+\frac17\Bigl(\begin{aligned} & 5x_{0}^{5}x_{1}+25x_{0}^{4}x_{3}x_{4}+50x_{0}^{3}x_{1}x_{3}^{2}\\ & +5x_{0}^{2}x_{1}^{3}x_{2}+15x_{0}^{2}x_{1}^{2}x_{4}x_{5}+15x_{0}^{2}x_{1}x_{2}x_{4}^{2}\\ & +50x_{0}^{2}x_{3}^{3}x_{4}+5x_{0}^{2}x_{4}^{3}x_{5}+10x_{0}x_{1}^{3}x_{3}x_{5}\\ & +30x_{0}x_{1}^{2}x_{2}x_{3}x_{4}+25x_{0}x_{1}x_{3}^{4}+30x_{0}x_{1}x_{3}x_{4}^{2}x_{5}\\ & +15x_{0}x_{2}^{5}+150x_{0}x_{2}^{3}x_{5}^{2}+10x_{0}x_{2}x_{3}x_{4}^{3}\\ & +75x_{0}x_{2}x_{5}^{4}+10x_{1}^{5}x_{2}+50x_{1}^{4}x_{4}x_{5}\\ & +5x_{1}^{3}x_{2}x_{3}^{2}+100x_{1}^{3}x_{2}x_{4}^{2}+15x_{1}^{2}x_{3}^{2}x_{4}x_{5}\\ & +100x_{1}^{2}x_{4}^{3}x_{5}+15x_{1}x_{2}x_{3}^{2}x_{4}^{2}+50x_{1}x_{2}x_{4}^{4}\\ & +75x_{2}^{4}x_{3}x_{5}+150x_{2}^{2}x_{3}x_{5}^{3}+5x_{3}^{5}x_{4}\\ & +5x_{3}^{2}x_{4}^{3}x_{5}+15x_{3}x_{5}^{5}+10x_{4}^{5}x_{5} \end{aligned}\Bigr). \end{aligned}

All numerical coefficients in this formula are interpreted in C\mathbb C, and 1/71/7 is the inverse of the nonzero complex number 77.

A. For the fixed value n=5n=5, the declaration defines AA as the polynomial x0x1x2x3x4x5x_0x_1x_2x_3x_4x_5 in C[x0,x1,x2,x3,x4,x5]\mathbb C[x_0,x_1,x_2,x_3,x_4,x_5], where xix_i is the formal indeterminate indexed by i∈{0,1,2,3,4,5}i\in\{0,1,2,3,4,5\}.

q. The declaration defines the natural number qq to be 11.

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