Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Eight planes · contact arrangement — instance data

Definition
HodgeComputerEightPlaneConfiguration

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

algebraic-geometryeight-plane-configurationhodge-computer

The exact fixed polynomials and pole parameter for “Eight planes · contact arrangement”, over C\mathbb CC with coordinates X0,X1,X2,Y0,Y1,Y2X_0,X_1,X_2,Y_0,Y_1,Y_2X0​,X1​,X2​,Y0​,Y1​,Y2​:

F=F0+∑i=025pi⋅Qi⋅Hi.F=F_0+\sum_{i=0}^2\frac5{p_i}\cdot Q_i\cdot H_i.F=F0​+i=0∑2​pi​5​⋅Qi​⋅Hi​. q=1,A=X03⋅Y03.q=1,\qquad A=X_{0}^{3} \cdot Y_{0}^{3}.q=1,A=X03​⋅Y03​.

where

F0=∑i=02(Xi6+Yi6)Qi=Xi2+Yi2,i=0,1,2Hi=ℓi3⋅ni+mi3⋅oi+ℓi2⋅oi2ℓi=17⋅∑j=02(j+i+1)⋅Xjmi=111⋅∑j=02(2⋅j+i+1)⋅Yjni=113⋅∑j=02(j+1)i+1⋅Xjoi=117⋅∑j=02(j+2)i+1⋅Yj(p0,p1,p2)=(7,11,13)\begin{aligned} F_0&=\sum_{i=0}^{2}(X_i^6+Y_i^6) \\ Q_i&=X_i^2+Y_i^2,\quad i=0,1,2 \\ H_i&=\ell_i^3\cdot n_i+m_i^3\cdot o_i+\ell_i^2\cdot o_i^2 \\ \ell_i&=\frac17\cdot\sum_{j=0}^2(j+i+1)\cdot X_j \\ m_i&=\frac1{11}\cdot\sum_{j=0}^2(2\cdot j+i+1)\cdot Y_j \\ n_i&=\frac1{13}\cdot\sum_{j=0}^2(j+1)^{i+1}\cdot X_j \\ o_i&=\frac1{17}\cdot\sum_{j=0}^2(j+2)^{i+1}\cdot Y_j \\ (p_0,p_1,p_2)&=(7,11,13) \end{aligned}F0​Qi​Hi​ℓi​mi​ni​oi​(p0​,p1​,p2​)​=i=0∑2​(Xi6​+Yi6​)=Xi2​+Yi2​,i=0,1,2=ℓi3​⋅ni​+mi3​⋅oi​+ℓi2​⋅oi2​=71​⋅j=0∑2​(j+i+1)⋅Xj​=111​⋅j=0∑2​(2⋅j+i+1)⋅Yj​=131​⋅j=0∑2​(j+1)i+1⋅Xj​=171​⋅j=0∑2​(j+2)i+1⋅Yj​=(7,11,13)​
Definition code
import Definitions.Def_DiamondCertificate

set_option autoImplicit false
noncomputable section
namespace HodgeComputer.EightPlaneConfiguration
def n : ℕ := 5
def d : ℕ := 6
def F : HodgeComputer.AmbientPoly n := ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((31218 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (6 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 31213 : ℂ)) + ((((40 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (5 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 31213 : ℂ))) + ((((60 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (5 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 31213 : ℂ))) + ((((1600 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 343343 : ℂ))) + (((((360 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 31213 : ℂ))) + ((((4455 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 405769 : ℂ))) + ((((3265 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 9020557 : ℂ))) + (((((60 : 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 / 99127 : ℂ))) + (((((80 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((17995 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + (((((120 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((7505 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2393209 : ℂ))) + ((((4140 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 343343 : ℂ))) + (((((12120 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 343343 : ℂ))) + (((((25380 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 405769 : ℂ))) + (((((18840 : 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 / 9020557 : ℂ))) + ((((((240 : 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 / 99127 : ℂ))) + ((((((320 : 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 := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + (((((124000 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + ((((((480 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + (((((522260 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 16752463 : ℂ))) + ((((37260 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 405769 : ℂ))) + (((((28260 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 9020557 : ℂ))) + ((((((360 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((480 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + (((((212010 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + ((((((720 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : 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 / 99127 : ℂ))) + (((((1329600 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 16752463 : ℂ))) + ((((710 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 31213 : ℂ))) + (((((2580 : 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 / 31213 : ℂ))) + (((((71160 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 405769 : ℂ))) + (((((665400 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 99226127 : ℂ))) + ((((((12720 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1090397 : ℂ))) + ((((((21440 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1090397 : ℂ))) + (((((65610 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2025023 : ℂ))) + ((((((45600 : 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 / 1090397 : ℂ))) + (((((22674000 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184277093 : ℂ))) + (((((166500 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 405769 : ℂ))) + ((((((125880 : 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 := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 9020557 : ℂ))) + (((((((720 : 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 := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + (((((((960 : 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 := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((93720 : 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 / 1288651 : ℂ))) + (((((((1440 : 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))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((922380 : 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 := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2393209 : ℂ))) + ((((140715 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 405769 : ℂ))) + (((((235530 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 9020557 : ℂ))) + ((((((143100 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1288651 : ℂ))) + ((((((331920 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1288651 : ℂ))) + (((((304260 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1288651 : ℂ))) + ((((((1102680 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1288651 : ℂ))) + (((((22486950 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 16752463 : ℂ))) + ((((34950 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 131938037 : ℂ))) + (((((167325 : 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 / 131938037 : ℂ))) + (((((248090 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 131938037 : ℂ))) + (((((668300 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 131938037 : ℂ))) + ((((((1246785 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : 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 / 131938037 : ℂ))) + (((((39587650 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1715194481 : ℂ))) + (((((254565 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 18848291 : ℂ))) + ((((((695320 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 18848291 : ℂ))) + ((((((33880365 : 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 / 245027783 : ℂ))) + (((((5962430 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 22275253 : ℂ))) + ((((244215 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 18848291 : ℂ))) + (((((1002195 : 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 / 18848291 : ℂ))) + (((((61115240 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + (((((216859245 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + ((((249197420 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + ((((1215 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (5 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 49049 : ℂ))) + (((((450 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 3773 : ℂ))) + (((((185440 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 637637 : ℂ))) + (((((1120160 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 99226127 : ℂ))) + ((((((4320 : 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 := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((((7680 : 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 / 155771 : ℂ))) + (((((793395 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + ((((((17280 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + (((((37499200 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184277093 : ℂ))) + (((((63680 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 91091 : ℂ))) + ((((((3104240 : 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)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 99226127 : ℂ))) + (((((((5760 : 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 / 155771 : ℂ))) + (((((((10240 : 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 := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((((175410 : 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 := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1090397 : ℂ))) + (((((((23040 : 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 := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((((135620000 : 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 := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184277093 : ℂ))) + (((((59100 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 57967 : ℂ))) + ((((((688440 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 9020557 : ℂ))) + (((((((51840 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((((122880 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + ((((((9371640 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + (((((((414720 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + ((((((61808220 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 16752463 : ℂ))) + (((((80 : 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 / 99127 : ℂ))) + ((((((240 : 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 / 99127 : ℂ))) + ((((((320 : 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 := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((8700 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1090397 : ℂ))) + (((((((480 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((57920 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1288651 : ℂ))) + ((((((4320 : 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)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + (((((((7680 : 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 / 155771 : ℂ))) + (((((((51840 : 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))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + ((((((122880 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((4860 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((((17280 : 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 / 155771 : ℂ))) + ((((((1161960 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2025023 : ℂ))) + ((((((414720 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((491520 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + ((((31000 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (5 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 57967 : ℂ))) + (((((626460 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 9020557 : ℂ))) + ((((((64800 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : 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 / 184093 : ℂ))) + ((((((153600 : MvPolynomial (Fin 6) ℂ) * (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 / 184093 : ℂ))) + (((((9760910 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + ((((((518400 : 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 / 184093 : ℂ))) + (((((64869400 : 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 / 16752463 : ℂ))) + (((((120 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((360 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((480 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((11930 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : 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 / 1090397 : ℂ))) + (((((((720 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((4320 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 75803 : ℂ))) + ((((((5760 : 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 / 155771 : ℂ))) + (((((((10240 : 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)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + (((((((64800 : 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))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + ((((((153600 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((6480 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((((23040 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((((209870 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 289289 : ℂ))) + ((((((518400 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (0 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((614400 : 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 / 184093 : ℂ))) + (((49589 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (6 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 49049 : ℂ))) + ((((3375 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (5 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 49049 : ℂ))) + ((((128780 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 637637 : ℂ))) + ((((712960 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 99226127 : ℂ))) + (((((3240 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + (((((5760 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((487755 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + (((((12960 : 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 / 155771 : ℂ))) + ((((21766400 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184277093 : ℂ))) + ((((301520 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 637637 : ℂ))) + (((((2748960 : 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 / 99226127 : ℂ))) + ((((((8640 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((((15360 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + (((((1859895 : 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 / 14175161 : ℂ))) + ((((((34560 : MvPolynomial (Fin 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 / 155771 : ℂ))) + (((((94326720 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184277093 : ℂ))) + ((((75120 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 91091 : ℂ))) + (((((7008360 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 99226127 : ℂ))) + ((((((455040 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 2025023 : ℂ))) + ((((((1034240 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 2025023 : ℂ))) + (((((562860 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1090397 : ℂ))) + ((((((3340800 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 2025023 : ℂ))) + (((((493383120 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184277093 : ℂ))) + ((((2104240 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1451318407 : ℂ))) + (((((1019160 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 131938037 : ℂ))) + (((((16813600 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1451318407 : ℂ))) + (((((33134100 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1451318407 : ℂ))) + ((((((81897720 : 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 / 1451318407 : ℂ))) + (((((1349734240 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 18867139291 : ℂ))) + (((((8977240 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 207331201 : ℂ))) + ((((((2696160 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 18848291 : ℂ))) + ((((((954313560 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : 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 / 2695305613 : ℂ))) + (((((1433297120 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2695305613 : ℂ))) + ((((7250535 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 207331201 : ℂ))) + (((((32310400 : 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 / 207331201 : ℂ))) + (((((216172800 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 385043659 : ℂ))) + (((((4527451800 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2695305613 : ℂ))) + ((((4984688000 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2695305613 : ℂ))) + ((((500 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (5 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 637 : ℂ))) + (((((939320 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 9020557 : ℂ))) + ((((((86400 : 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 / 184093 : ℂ))) + ((((((204800 : 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 := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((13469240 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + ((((((691200 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : 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 / 184093 : ℂ))) + (((((963700 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((240 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((720 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((960 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((1140 : 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 / 64141 : ℂ))) + (((((((1440 : 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))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 99127 : ℂ))) + ((((((102080 : 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 := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1288651 : ℂ))) + ((((((8640 : MvPolynomial (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)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + (((((((15360 : MvPolynomial (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)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + (((((((86400 : MvPolynomial (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)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + ((((((204800 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((9720 : 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 / 155771 : ℂ))) + ((((((34560 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 155771 : ℂ))) + ((((((2003160 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2025023 : ℂ))) + ((((((691200 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((819200 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (1 : Fin 6))) * (MvPolynomial.X (R := ℂ) (2 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((74842 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (6 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 57967 : ℂ))) + ((((509045 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 9020557 : ℂ))) + (((((54000 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + (((((128000 : 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 / 184093 : ℂ))) + ((((603765 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1090397 : ℂ))) + (((((432000 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 184093 : ℂ))) + ((((51468875 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 16752463 : ℂ))) + ((((9412020 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1715194481 : ℂ))) + (((((62085015 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1715194481 : ℂ))) + (((((106920360 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1715194481 : ℂ))) + (((((1486370 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 14175161 : ℂ))) + ((((((566305605 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : 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 / 1715194481 : ℂ))) + (((((542511880 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1715194481 : ℂ))) + (((((38527855 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + ((((((164423170 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + ((((((313889655 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : 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 / 245027783 : ℂ))) + (((((299349720 : 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 / 245027783 : ℂ))) + ((((24249915 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + (((((128600795 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + (((((376100840 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + (((((809485665 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + ((((772902080 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 245027783 : ℂ))) + (((158399 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (6 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 158389 : ℂ))) + ((((15 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (5 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 22627 : ℂ))) + ((((10 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (5 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 9317 : ℂ))) + ((((5575 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1742279 : ℂ))) + (((((1305 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 158389 : ℂ))) + ((((3030 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 294151 : ℂ))) + ((((1515 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 158389 : ℂ))) + (((((50200 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 1742279 : ℂ))) + (((((130590 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2059057 : ℂ))) + ((((149150 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2059057 : ℂ))) + ((((33015 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 1742279 : ℂ))) + (((((118095 : 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 / 1742279 : ℂ))) + (((((3882330 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 22649627 : ℂ))) + (((((740280 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2059057 : ℂ))) + ((((579340 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2059057 : ℂ))) + ((((5600 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (5 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 248897 : ℂ))) + (((((2400 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 22627 : ℂ))) + (((((927325 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 3235661 : ℂ))) + (((((2239350 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 3235661 : ℂ))) + (((((290535 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 294151 : ℂ))) + ((((154840 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (3 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (5 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 294151 : ℂ))) + (((251777 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (6 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 248897 : ℂ))) + ((((18080 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (5 : ℕ))) * (MvPolynomial.X (R := ℂ) (5 : Fin 6))) * MvPolynomial.C (σ := Fin 6) (1 / 248897 : ℂ))) + ((((737865 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (4 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (2 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 3235661 : ℂ))) + ((((1795265 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 3235661 : ℂ))) + ((((3164115 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (2 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (4 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 3235661 : ℂ))) + ((((281505 : MvPolynomial (Fin 6) ℂ) * (MvPolynomial.X (R := ℂ) (4 : Fin 6))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (5 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 294151 : ℂ))) + (((403911 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (6 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 294151 : ℂ)))
def A : HodgeComputer.AmbientPoly n := (((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ)) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ)))
def q : ℕ := 1
end HodgeComputer.EightPlaneConfiguration
Source
https://github.com/hodge-computer/sextics/blob/83fbf5c9a0afe9136ce4f1ed324d085a2c899bd0/data/eight-plane-configuration/instance.rec
Read-back

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

The definition nnn is the natural number 555.

The definition ddd is the natural number 666.

The definition FFF is the following element of the polynomial ring R=C[X0,X1,X2,Y0,Y1,Y2]R=\mathbb C[X_0,X_1,X_2,Y_0,Y_1,Y_2]R=C[X0​,X1​,X2​,Y0​,Y1​,Y2​] in six algebraically independent variables, corresponding in order to indices 0,1,2,3,4,50,1,2,3,4,50,1,2,3,4,5:

F=3121831213X06+4031213X05X1+6031213X05X2+1600343343X04X12+36031213X04X1X2+4455405769X04X22+32659020557X04Y02+6099127X04Y0Y1+8099127X04Y0Y2+1799514175161X04Y12+12099127X04Y1Y2+75052393209X04Y22+4140343343X03X13+12120343343X03X12X2+25380405769X03X1X22+188409020557X03X1Y02+24099127X03X1Y0Y1+32099127X03X1Y0Y2+12400014175161X03X1Y12+48099127X03X1Y1Y2+52226016752463X03X1Y22+37260405769X03X23+282609020557X03X2Y02+36099127X03X2Y0Y1+48099127X03X2Y0Y2+21201014175161X03X2Y12+72099127X03X2Y1Y2+132960016752463X03X2Y22+71031213X02X14+258031213X02X13X2+71160405769X02X12X22+66540099226127X02X12Y02+127201090397X02X12Y0Y1+214401090397X02X12Y0Y2+656102025023X02X12Y12+456001090397X02X12Y1Y2+22674000184277093X02X12Y22+166500405769X02X1X23+1258809020557X02X1X2Y02+72099127X02X1X2Y0Y1+96099127X02X1X2Y0Y2+937201288651X02X1X2Y12+144099127X02X1X2Y1Y2+9223802393209X02X1X2Y22+140715405769X02X24+2355309020557X02X22Y02+1431001288651X02X22Y0Y1+3319201288651X02X22Y0Y2+3042601288651X02X22Y12+11026801288651X02X22Y1Y2+2248695016752463X02X22Y22+34950131938037X02Y04+167325131938037X02Y03Y1+248090131938037X02Y03Y2+668300131938037X02Y02Y12+1246785131938037X02Y02Y1Y2+395876501715194481X02Y02Y22+25456518848291X02Y0Y13+69532018848291X02Y0Y12Y2+33880365245027783X02Y0Y1Y22+596243022275253X02Y0Y23+24421518848291X02Y14+100219518848291X02Y13Y2+61115240245027783X02Y12Y22+216859245245027783X02Y1Y23+249197420245027783X02Y24+121549049X0X15+4503773X0X14X2+185440637637X0X13X22+112016099226127X0X13Y02+4320155771X0X13Y0Y1+7680155771X0X13Y0Y2+79339514175161X0X13Y12+17280155771X0X13Y1Y2+37499200184277093X0X13Y22+6368091091X0X12X23+310424099226127X0X12X2Y02+5760155771X0X12X2Y0Y1+10240155771X0X12X2Y0Y2+1754101090397X0X12X2Y12+23040155771X0X12X2Y1Y2+135620000184277093X0X12X2Y22+5910057967X0X1X24+6884409020557X0X1X22Y02+51840184093X0X1X22Y0Y1+122880184093X0X1X22Y0Y2+937164014175161X0X1X22Y12+414720184093X0X1X22Y1Y2+6180822016752463X0X1X22Y22+8099127X0X1Y04+24099127X0X1Y03Y1+32099127X0X1Y03Y2+87001090397X0X1Y02Y12+48099127X0X1Y02Y1Y2+579201288651X0X1Y02Y22+4320155771X0X1Y0Y13+7680155771X0X1Y0Y12Y2+51840184093X0X1Y0Y1Y22+122880184093X0X1Y0Y23+4860155771X0X1Y14+17280155771X0X1Y13Y2+11619602025023X0X1Y12Y22+414720184093X0X1Y1Y23+491520184093X0X1Y24+3100057967X0X25+6264609020557X0X23Y02+64800184093X0X23Y0Y1+153600184093X0X23Y0Y2+976091014175161X0X23Y12+518400184093X0X23Y1Y2+6486940016752463X0X23Y22+12099127X0X2Y04+36099127X0X2Y03Y1+48099127X0X2Y03Y2+119301090397X0X2Y02Y12+72099127X0X2Y02Y1Y2+432075803X0X2Y02Y22+5760155771X0X2Y0Y13+10240155771X0X2Y0Y12Y2+64800184093X0X2Y0Y1Y22+153600184093X0X2Y0Y23+6480155771X0X2Y14+23040155771X0X2Y13Y2+209870289289X0X2Y12Y22+518400184093X0X2Y1Y23+614400184093X0X2Y24+4958949049X16+337549049X15X2+128780637637X14X22+71296099226127X14Y02+3240155771X14Y0Y1+5760155771X14Y0Y2+48775514175161X14Y12+12960155771X14Y1Y2+21766400184277093X14Y22+301520637637X13X23+274896099226127X13X2Y02+8640155771X13X2Y0Y1+15360155771X13X2Y0Y2+185989514175161X13X2Y12+34560155771X13X2Y1Y2+94326720184277093X13X2Y22+7512091091X12X24+700836099226127X12X22Y02+4550402025023X12X22Y0Y1+10342402025023X12X22Y0Y2+5628601090397X12X22Y12+33408002025023X12X22Y1Y2+493383120184277093X12X22Y22+21042401451318407X12Y04+1019160131938037X12Y03Y1+168136001451318407X12Y03Y2+331341001451318407X12Y02Y12+818977201451318407X12Y02Y1Y2+134973424018867139291X12Y02Y22+8977240207331201X12Y0Y13+269616018848291X12Y0Y12Y2+9543135602695305613X12Y0Y1Y22+14332971202695305613X12Y0Y23+7250535207331201X12Y14+32310400207331201X12Y13Y2+216172800385043659X12Y12Y22+45274518002695305613X12Y1Y23+49846880002695305613X12Y24+500637X1X25+9393209020557X1X23Y02+86400184093X1X23Y0Y1+204800184093X1X23Y0Y2+1346924014175161X1X23Y12+691200184093X1X23Y1Y2+963700184093X1X23Y22+24099127X1X2Y04+72099127X1X2Y03Y1+96099127X1X2Y03Y2+114064141X1X2Y02Y12+144099127X1X2Y02Y1Y2+1020801288651X1X2Y02Y22+8640155771X1X2Y0Y13+15360155771X1X2Y0Y12Y2+86400184093X1X2Y0Y1Y22+204800184093X1X2Y0Y23+9720155771X1X2Y14+34560155771X1X2Y13Y2+20031602025023X1X2Y12Y22+691200184093X1X2Y1Y23+819200184093X1X2Y24+7484257967X26+5090459020557X24Y02+54000184093X24Y0Y1+128000184093X24Y0Y2+6037651090397X24Y12+432000184093X24Y1Y2+5146887516752463X24Y22+94120201715194481X22Y04+620850151715194481X22Y03Y1+1069203601715194481X22Y03Y2+148637014175161X22Y02Y12+5663056051715194481X22Y02Y1Y2+5425118801715194481X22Y02Y22+38527855245027783X22Y0Y13+164423170245027783X22Y0Y12Y2+313889655245027783X22Y0Y1Y22+299349720245027783X22Y0Y23+24249915245027783X22Y14+128600795245027783X22Y13Y2+376100840245027783X22Y12Y22+809485665245027783X22Y1Y23+772902080245027783X22Y24+158399158389Y06+1522627Y05Y1+109317Y05Y2+55751742279Y04Y12+1305158389Y04Y1Y2+3030294151Y04Y22+1515158389Y03Y13+502001742279Y03Y12Y2+1305902059057Y03Y1Y22+1491502059057Y03Y23+330151742279Y02Y14+1180951742279Y02Y13Y2+388233022649627Y02Y12Y22+7402802059057Y02Y1Y23+5793402059057Y02Y24+5600248897Y0Y15+240022627Y0Y14Y2+9273253235661Y0Y13Y22+22393503235661Y0Y12Y23+290535294151Y0Y1Y24+154840294151Y0Y25+251777248897Y16+18080248897Y15Y2+7378653235661Y14Y22+17952653235661Y13Y23+31641153235661Y12Y24+281505294151Y1Y25+403911294151Y26.\begin{aligned} F={}&\frac{31218}{31213}X_0^{6}+\frac{40}{31213}X_0^{5}X_1+\frac{60}{31213}X_0^{5}X_2\\ &+\frac{1600}{343343}X_0^{4}X_1^{2}+\frac{360}{31213}X_0^{4}X_1X_2+\frac{4455}{405769}X_0^{4}X_2^{2}\\ &+\frac{3265}{9020557}X_0^{4}Y_0^{2}+\frac{60}{99127}X_0^{4}Y_0Y_1+\frac{80}{99127}X_0^{4}Y_0Y_2\\ &+\frac{17995}{14175161}X_0^{4}Y_1^{2}+\frac{120}{99127}X_0^{4}Y_1Y_2+\frac{7505}{2393209}X_0^{4}Y_2^{2}\\ &+\frac{4140}{343343}X_0^{3}X_1^{3}+\frac{12120}{343343}X_0^{3}X_1^{2}X_2+\frac{25380}{405769}X_0^{3}X_1X_2^{2}\\ &+\frac{18840}{9020557}X_0^{3}X_1Y_0^{2}+\frac{240}{99127}X_0^{3}X_1Y_0Y_1+\frac{320}{99127}X_0^{3}X_1Y_0Y_2\\ &+\frac{124000}{14175161}X_0^{3}X_1Y_1^{2}+\frac{480}{99127}X_0^{3}X_1Y_1Y_2+\frac{522260}{16752463}X_0^{3}X_1Y_2^{2}\\ &+\frac{37260}{405769}X_0^{3}X_2^{3}+\frac{28260}{9020557}X_0^{3}X_2Y_0^{2}+\frac{360}{99127}X_0^{3}X_2Y_0Y_1\\ &+\frac{480}{99127}X_0^{3}X_2Y_0Y_2+\frac{212010}{14175161}X_0^{3}X_2Y_1^{2}+\frac{720}{99127}X_0^{3}X_2Y_1Y_2\\ &+\frac{1329600}{16752463}X_0^{3}X_2Y_2^{2}+\frac{710}{31213}X_0^{2}X_1^{4}+\frac{2580}{31213}X_0^{2}X_1^{3}X_2\\ &+\frac{71160}{405769}X_0^{2}X_1^{2}X_2^{2}+\frac{665400}{99226127}X_0^{2}X_1^{2}Y_0^{2}+\frac{12720}{1090397}X_0^{2}X_1^{2}Y_0Y_1\\ &+\frac{21440}{1090397}X_0^{2}X_1^{2}Y_0Y_2+\frac{65610}{2025023}X_0^{2}X_1^{2}Y_1^{2}+\frac{45600}{1090397}X_0^{2}X_1^{2}Y_1Y_2\\ &+\frac{22674000}{184277093}X_0^{2}X_1^{2}Y_2^{2}+\frac{166500}{405769}X_0^{2}X_1X_2^{3}+\frac{125880}{9020557}X_0^{2}X_1X_2Y_0^{2}\\ &+\frac{720}{99127}X_0^{2}X_1X_2Y_0Y_1+\frac{960}{99127}X_0^{2}X_1X_2Y_0Y_2+\frac{93720}{1288651}X_0^{2}X_1X_2Y_1^{2}\\ &+\frac{1440}{99127}X_0^{2}X_1X_2Y_1Y_2+\frac{922380}{2393209}X_0^{2}X_1X_2Y_2^{2}+\frac{140715}{405769}X_0^{2}X_2^{4}\\ &+\frac{235530}{9020557}X_0^{2}X_2^{2}Y_0^{2}+\frac{143100}{1288651}X_0^{2}X_2^{2}Y_0Y_1+\frac{331920}{1288651}X_0^{2}X_2^{2}Y_0Y_2\\ &+\frac{304260}{1288651}X_0^{2}X_2^{2}Y_1^{2}+\frac{1102680}{1288651}X_0^{2}X_2^{2}Y_1Y_2+\frac{22486950}{16752463}X_0^{2}X_2^{2}Y_2^{2}\\ &+\frac{34950}{131938037}X_0^{2}Y_0^{4}+\frac{167325}{131938037}X_0^{2}Y_0^{3}Y_1+\frac{248090}{131938037}X_0^{2}Y_0^{3}Y_2\\ &+\frac{668300}{131938037}X_0^{2}Y_0^{2}Y_1^{2}+\frac{1246785}{131938037}X_0^{2}Y_0^{2}Y_1Y_2+\frac{39587650}{1715194481}X_0^{2}Y_0^{2}Y_2^{2}\\ &+\frac{254565}{18848291}X_0^{2}Y_0Y_1^{3}+\frac{695320}{18848291}X_0^{2}Y_0Y_1^{2}Y_2+\frac{33880365}{245027783}X_0^{2}Y_0Y_1Y_2^{2}\\ &+\frac{5962430}{22275253}X_0^{2}Y_0Y_2^{3}+\frac{244215}{18848291}X_0^{2}Y_1^{4}+\frac{1002195}{18848291}X_0^{2}Y_1^{3}Y_2\\ &+\frac{61115240}{245027783}X_0^{2}Y_1^{2}Y_2^{2}+\frac{216859245}{245027783}X_0^{2}Y_1Y_2^{3}+\frac{249197420}{245027783}X_0^{2}Y_2^{4}\\ &+\frac{1215}{49049}X_0X_1^{5}+\frac{450}{3773}X_0X_1^{4}X_2+\frac{185440}{637637}X_0X_1^{3}X_2^{2}\\ &+\frac{1120160}{99226127}X_0X_1^{3}Y_0^{2}+\frac{4320}{155771}X_0X_1^{3}Y_0Y_1+\frac{7680}{155771}X_0X_1^{3}Y_0Y_2\\ &+\frac{793395}{14175161}X_0X_1^{3}Y_1^{2}+\frac{17280}{155771}X_0X_1^{3}Y_1Y_2+\frac{37499200}{184277093}X_0X_1^{3}Y_2^{2}\\ &+\frac{63680}{91091}X_0X_1^{2}X_2^{3}+\frac{3104240}{99226127}X_0X_1^{2}X_2Y_0^{2}+\frac{5760}{155771}X_0X_1^{2}X_2Y_0Y_1\\ &+\frac{10240}{155771}X_0X_1^{2}X_2Y_0Y_2+\frac{175410}{1090397}X_0X_1^{2}X_2Y_1^{2}+\frac{23040}{155771}X_0X_1^{2}X_2Y_1Y_2\\ &+\frac{135620000}{184277093}X_0X_1^{2}X_2Y_2^{2}+\frac{59100}{57967}X_0X_1X_2^{4}+\frac{688440}{9020557}X_0X_1X_2^{2}Y_0^{2}\\ &+\frac{51840}{184093}X_0X_1X_2^{2}Y_0Y_1+\frac{122880}{184093}X_0X_1X_2^{2}Y_0Y_2+\frac{9371640}{14175161}X_0X_1X_2^{2}Y_1^{2}\\ &+\frac{414720}{184093}X_0X_1X_2^{2}Y_1Y_2+\frac{61808220}{16752463}X_0X_1X_2^{2}Y_2^{2}+\frac{80}{99127}X_0X_1Y_0^{4}\\ &+\frac{240}{99127}X_0X_1Y_0^{3}Y_1+\frac{320}{99127}X_0X_1Y_0^{3}Y_2+\frac{8700}{1090397}X_0X_1Y_0^{2}Y_1^{2}\\ &+\frac{480}{99127}X_0X_1Y_0^{2}Y_1Y_2+\frac{57920}{1288651}X_0X_1Y_0^{2}Y_2^{2}+\frac{4320}{155771}X_0X_1Y_0Y_1^{3}\\ &+\frac{7680}{155771}X_0X_1Y_0Y_1^{2}Y_2+\frac{51840}{184093}X_0X_1Y_0Y_1Y_2^{2}+\frac{122880}{184093}X_0X_1Y_0Y_2^{3}\\ &+\frac{4860}{155771}X_0X_1Y_1^{4}+\frac{17280}{155771}X_0X_1Y_1^{3}Y_2+\frac{1161960}{2025023}X_0X_1Y_1^{2}Y_2^{2}\\ &+\frac{414720}{184093}X_0X_1Y_1Y_2^{3}+\frac{491520}{184093}X_0X_1Y_2^{4}+\frac{31000}{57967}X_0X_2^{5}\\ &+\frac{626460}{9020557}X_0X_2^{3}Y_0^{2}+\frac{64800}{184093}X_0X_2^{3}Y_0Y_1+\frac{153600}{184093}X_0X_2^{3}Y_0Y_2\\ &+\frac{9760910}{14175161}X_0X_2^{3}Y_1^{2}+\frac{518400}{184093}X_0X_2^{3}Y_1Y_2+\frac{64869400}{16752463}X_0X_2^{3}Y_2^{2}\\ &+\frac{120}{99127}X_0X_2Y_0^{4}+\frac{360}{99127}X_0X_2Y_0^{3}Y_1+\frac{480}{99127}X_0X_2Y_0^{3}Y_2\\ &+\frac{11930}{1090397}X_0X_2Y_0^{2}Y_1^{2}+\frac{720}{99127}X_0X_2Y_0^{2}Y_1Y_2+\frac{4320}{75803}X_0X_2Y_0^{2}Y_2^{2}\\ &+\frac{5760}{155771}X_0X_2Y_0Y_1^{3}+\frac{10240}{155771}X_0X_2Y_0Y_1^{2}Y_2+\frac{64800}{184093}X_0X_2Y_0Y_1Y_2^{2}\\ &+\frac{153600}{184093}X_0X_2Y_0Y_2^{3}+\frac{6480}{155771}X_0X_2Y_1^{4}+\frac{23040}{155771}X_0X_2Y_1^{3}Y_2\\ &+\frac{209870}{289289}X_0X_2Y_1^{2}Y_2^{2}+\frac{518400}{184093}X_0X_2Y_1Y_2^{3}+\frac{614400}{184093}X_0X_2Y_2^{4}\\ &+\frac{49589}{49049}X_1^{6}+\frac{3375}{49049}X_1^{5}X_2+\frac{128780}{637637}X_1^{4}X_2^{2}\\ &+\frac{712960}{99226127}X_1^{4}Y_0^{2}+\frac{3240}{155771}X_1^{4}Y_0Y_1+\frac{5760}{155771}X_1^{4}Y_0Y_2\\ &+\frac{487755}{14175161}X_1^{4}Y_1^{2}+\frac{12960}{155771}X_1^{4}Y_1Y_2+\frac{21766400}{184277093}X_1^{4}Y_2^{2}\\ &+\frac{301520}{637637}X_1^{3}X_2^{3}+\frac{2748960}{99226127}X_1^{3}X_2Y_0^{2}+\frac{8640}{155771}X_1^{3}X_2Y_0Y_1\\ &+\frac{15360}{155771}X_1^{3}X_2Y_0Y_2+\frac{1859895}{14175161}X_1^{3}X_2Y_1^{2}+\frac{34560}{155771}X_1^{3}X_2Y_1Y_2\\ &+\frac{94326720}{184277093}X_1^{3}X_2Y_2^{2}+\frac{75120}{91091}X_1^{2}X_2^{4}+\frac{7008360}{99226127}X_1^{2}X_2^{2}Y_0^{2}\\ &+\frac{455040}{2025023}X_1^{2}X_2^{2}Y_0Y_1+\frac{1034240}{2025023}X_1^{2}X_2^{2}Y_0Y_2+\frac{562860}{1090397}X_1^{2}X_2^{2}Y_1^{2}\\ &+\frac{3340800}{2025023}X_1^{2}X_2^{2}Y_1Y_2+\frac{493383120}{184277093}X_1^{2}X_2^{2}Y_2^{2}+\frac{2104240}{1451318407}X_1^{2}Y_0^{4}\\ &+\frac{1019160}{131938037}X_1^{2}Y_0^{3}Y_1+\frac{16813600}{1451318407}X_1^{2}Y_0^{3}Y_2+\frac{33134100}{1451318407}X_1^{2}Y_0^{2}Y_1^{2}\\ &+\frac{81897720}{1451318407}X_1^{2}Y_0^{2}Y_1Y_2+\frac{1349734240}{18867139291}X_1^{2}Y_0^{2}Y_2^{2}+\frac{8977240}{207331201}X_1^{2}Y_0Y_1^{3}\\ &+\frac{2696160}{18848291}X_1^{2}Y_0Y_1^{2}Y_2+\frac{954313560}{2695305613}X_1^{2}Y_0Y_1Y_2^{2}+\frac{1433297120}{2695305613}X_1^{2}Y_0Y_2^{3}\\ &+\frac{7250535}{207331201}X_1^{2}Y_1^{4}+\frac{32310400}{207331201}X_1^{2}Y_1^{3}Y_2+\frac{216172800}{385043659}X_1^{2}Y_1^{2}Y_2^{2}\\ &+\frac{4527451800}{2695305613}X_1^{2}Y_1Y_2^{3}+\frac{4984688000}{2695305613}X_1^{2}Y_2^{4}+\frac{500}{637}X_1X_2^{5}\\ &+\frac{939320}{9020557}X_1X_2^{3}Y_0^{2}+\frac{86400}{184093}X_1X_2^{3}Y_0Y_1+\frac{204800}{184093}X_1X_2^{3}Y_0Y_2\\ &+\frac{13469240}{14175161}X_1X_2^{3}Y_1^{2}+\frac{691200}{184093}X_1X_2^{3}Y_1Y_2+\frac{963700}{184093}X_1X_2^{3}Y_2^{2}\\ &+\frac{240}{99127}X_1X_2Y_0^{4}+\frac{720}{99127}X_1X_2Y_0^{3}Y_1+\frac{960}{99127}X_1X_2Y_0^{3}Y_2\\ &+\frac{1140}{64141}X_1X_2Y_0^{2}Y_1^{2}+\frac{1440}{99127}X_1X_2Y_0^{2}Y_1Y_2+\frac{102080}{1288651}X_1X_2Y_0^{2}Y_2^{2}\\ &+\frac{8640}{155771}X_1X_2Y_0Y_1^{3}+\frac{15360}{155771}X_1X_2Y_0Y_1^{2}Y_2+\frac{86400}{184093}X_1X_2Y_0Y_1Y_2^{2}\\ &+\frac{204800}{184093}X_1X_2Y_0Y_2^{3}+\frac{9720}{155771}X_1X_2Y_1^{4}+\frac{34560}{155771}X_1X_2Y_1^{3}Y_2\\ &+\frac{2003160}{2025023}X_1X_2Y_1^{2}Y_2^{2}+\frac{691200}{184093}X_1X_2Y_1Y_2^{3}+\frac{819200}{184093}X_1X_2Y_2^{4}\\ &+\frac{74842}{57967}X_2^{6}+\frac{509045}{9020557}X_2^{4}Y_0^{2}+\frac{54000}{184093}X_2^{4}Y_0Y_1\\ &+\frac{128000}{184093}X_2^{4}Y_0Y_2+\frac{603765}{1090397}X_2^{4}Y_1^{2}+\frac{432000}{184093}X_2^{4}Y_1Y_2\\ &+\frac{51468875}{16752463}X_2^{4}Y_2^{2}+\frac{9412020}{1715194481}X_2^{2}Y_0^{4}+\frac{62085015}{1715194481}X_2^{2}Y_0^{3}Y_1\\ &+\frac{106920360}{1715194481}X_2^{2}Y_0^{3}Y_2+\frac{1486370}{14175161}X_2^{2}Y_0^{2}Y_1^{2}+\frac{566305605}{1715194481}X_2^{2}Y_0^{2}Y_1Y_2\\ &+\frac{542511880}{1715194481}X_2^{2}Y_0^{2}Y_2^{2}+\frac{38527855}{245027783}X_2^{2}Y_0Y_1^{3}+\frac{164423170}{245027783}X_2^{2}Y_0Y_1^{2}Y_2\\ &+\frac{313889655}{245027783}X_2^{2}Y_0Y_1Y_2^{2}+\frac{299349720}{245027783}X_2^{2}Y_0Y_2^{3}+\frac{24249915}{245027783}X_2^{2}Y_1^{4}\\ &+\frac{128600795}{245027783}X_2^{2}Y_1^{3}Y_2+\frac{376100840}{245027783}X_2^{2}Y_1^{2}Y_2^{2}+\frac{809485665}{245027783}X_2^{2}Y_1Y_2^{3}\\ &+\frac{772902080}{245027783}X_2^{2}Y_2^{4}+\frac{158399}{158389}Y_0^{6}+\frac{15}{22627}Y_0^{5}Y_1\\ &+\frac{10}{9317}Y_0^{5}Y_2+\frac{5575}{1742279}Y_0^{4}Y_1^{2}+\frac{1305}{158389}Y_0^{4}Y_1Y_2\\ &+\frac{3030}{294151}Y_0^{4}Y_2^{2}+\frac{1515}{158389}Y_0^{3}Y_1^{3}+\frac{50200}{1742279}Y_0^{3}Y_1^{2}Y_2\\ &+\frac{130590}{2059057}Y_0^{3}Y_1Y_2^{2}+\frac{149150}{2059057}Y_0^{3}Y_2^{3}+\frac{33015}{1742279}Y_0^{2}Y_1^{4}\\ &+\frac{118095}{1742279}Y_0^{2}Y_1^{3}Y_2+\frac{3882330}{22649627}Y_0^{2}Y_1^{2}Y_2^{2}+\frac{740280}{2059057}Y_0^{2}Y_1Y_2^{3}\\ &+\frac{579340}{2059057}Y_0^{2}Y_2^{4}+\frac{5600}{248897}Y_0Y_1^{5}+\frac{2400}{22627}Y_0Y_1^{4}Y_2\\ &+\frac{927325}{3235661}Y_0Y_1^{3}Y_2^{2}+\frac{2239350}{3235661}Y_0Y_1^{2}Y_2^{3}+\frac{290535}{294151}Y_0Y_1Y_2^{4}\\ &+\frac{154840}{294151}Y_0Y_2^{5}+\frac{251777}{248897}Y_1^{6}+\frac{18080}{248897}Y_1^{5}Y_2\\ &+\frac{737865}{3235661}Y_1^{4}Y_2^{2}+\frac{1795265}{3235661}Y_1^{3}Y_2^{3}+\frac{3164115}{3235661}Y_1^{2}Y_2^{4}\\ &+\frac{281505}{294151}Y_1Y_2^{5}+\frac{403911}{294151}Y_2^{6}. \end{aligned}F=​3121331218​X06​+3121340​X05​X1​+3121360​X05​X2​+3433431600​X04​X12​+31213360​X04​X1​X2​+4057694455​X04​X22​+90205573265​X04​Y02​+9912760​X04​Y0​Y1​+9912780​X04​Y0​Y2​+1417516117995​X04​Y12​+99127120​X04​Y1​Y2​+23932097505​X04​Y22​+3433434140​X03​X13​+34334312120​X03​X12​X2​+40576925380​X03​X1​X22​+902055718840​X03​X1​Y02​+99127240​X03​X1​Y0​Y1​+99127320​X03​X1​Y0​Y2​+14175161124000​X03​X1​Y12​+99127480​X03​X1​Y1​Y2​+16752463522260​X03​X1​Y22​+40576937260​X03​X23​+902055728260​X03​X2​Y02​+99127360​X03​X2​Y0​Y1​+99127480​X03​X2​Y0​Y2​+14175161212010​X03​X2​Y12​+99127720​X03​X2​Y1​Y2​+167524631329600​X03​X2​Y22​+31213710​X02​X14​+312132580​X02​X13​X2​+40576971160​X02​X12​X22​+99226127665400​X02​X12​Y02​+109039712720​X02​X12​Y0​Y1​+109039721440​X02​X12​Y0​Y2​+202502365610​X02​X12​Y12​+109039745600​X02​X12​Y1​Y2​+18427709322674000​X02​X12​Y22​+405769166500​X02​X1​X23​+9020557125880​X02​X1​X2​Y02​+99127720​X02​X1​X2​Y0​Y1​+99127960​X02​X1​X2​Y0​Y2​+128865193720​X02​X1​X2​Y12​+991271440​X02​X1​X2​Y1​Y2​+2393209922380​X02​X1​X2​Y22​+405769140715​X02​X24​+9020557235530​X02​X22​Y02​+1288651143100​X02​X22​Y0​Y1​+1288651331920​X02​X22​Y0​Y2​+1288651304260​X02​X22​Y12​+12886511102680​X02​X22​Y1​Y2​+1675246322486950​X02​X22​Y22​+13193803734950​X02​Y04​+131938037167325​X02​Y03​Y1​+131938037248090​X02​Y03​Y2​+131938037668300​X02​Y02​Y12​+1319380371246785​X02​Y02​Y1​Y2​+171519448139587650​X02​Y02​Y22​+18848291254565​X02​Y0​Y13​+18848291695320​X02​Y0​Y12​Y2​+24502778333880365​X02​Y0​Y1​Y22​+222752535962430​X02​Y0​Y23​+18848291244215​X02​Y14​+188482911002195​X02​Y13​Y2​+24502778361115240​X02​Y12​Y22​+245027783216859245​X02​Y1​Y23​+245027783249197420​X02​Y24​+490491215​X0​X15​+3773450​X0​X14​X2​+637637185440​X0​X13​X22​+992261271120160​X0​X13​Y02​+1557714320​X0​X13​Y0​Y1​+1557717680​X0​X13​Y0​Y2​+14175161793395​X0​X13​Y12​+15577117280​X0​X13​Y1​Y2​+18427709337499200​X0​X13​Y22​+9109163680​X0​X12​X23​+992261273104240​X0​X12​X2​Y02​+1557715760​X0​X12​X2​Y0​Y1​+15577110240​X0​X12​X2​Y0​Y2​+1090397175410​X0​X12​X2​Y12​+15577123040​X0​X12​X2​Y1​Y2​+184277093135620000​X0​X12​X2​Y22​+5796759100​X0​X1​X24​+9020557688440​X0​X1​X22​Y02​+18409351840​X0​X1​X22​Y0​Y1​+184093122880​X0​X1​X22​Y0​Y2​+141751619371640​X0​X1​X22​Y12​+184093414720​X0​X1​X22​Y1​Y2​+1675246361808220​X0​X1​X22​Y22​+9912780​X0​X1​Y04​+99127240​X0​X1​Y03​Y1​+99127320​X0​X1​Y03​Y2​+10903978700​X0​X1​Y02​Y12​+99127480​X0​X1​Y02​Y1​Y2​+128865157920​X0​X1​Y02​Y22​+1557714320​X0​X1​Y0​Y13​+1557717680​X0​X1​Y0​Y12​Y2​+18409351840​X0​X1​Y0​Y1​Y22​+184093122880​X0​X1​Y0​Y23​+1557714860​X0​X1​Y14​+15577117280​X0​X1​Y13​Y2​+20250231161960​X0​X1​Y12​Y22​+184093414720​X0​X1​Y1​Y23​+184093491520​X0​X1​Y24​+5796731000​X0​X25​+9020557626460​X0​X23​Y02​+18409364800​X0​X23​Y0​Y1​+184093153600​X0​X23​Y0​Y2​+141751619760910​X0​X23​Y12​+184093518400​X0​X23​Y1​Y2​+1675246364869400​X0​X23​Y22​+99127120​X0​X2​Y04​+99127360​X0​X2​Y03​Y1​+99127480​X0​X2​Y03​Y2​+109039711930​X0​X2​Y02​Y12​+99127720​X0​X2​Y02​Y1​Y2​+758034320​X0​X2​Y02​Y22​+1557715760​X0​X2​Y0​Y13​+15577110240​X0​X2​Y0​Y12​Y2​+18409364800​X0​X2​Y0​Y1​Y22​+184093153600​X0​X2​Y0​Y23​+1557716480​X0​X2​Y14​+15577123040​X0​X2​Y13​Y2​+289289209870​X0​X2​Y12​Y22​+184093518400​X0​X2​Y1​Y23​+184093614400​X0​X2​Y24​+4904949589​X16​+490493375​X15​X2​+637637128780​X14​X22​+99226127712960​X14​Y02​+1557713240​X14​Y0​Y1​+1557715760​X14​Y0​Y2​+14175161487755​X14​Y12​+15577112960​X14​Y1​Y2​+18427709321766400​X14​Y22​+637637301520​X13​X23​+992261272748960​X13​X2​Y02​+1557718640​X13​X2​Y0​Y1​+15577115360​X13​X2​Y0​Y2​+141751611859895​X13​X2​Y12​+15577134560​X13​X2​Y1​Y2​+18427709394326720​X13​X2​Y22​+9109175120​X12​X24​+992261277008360​X12​X22​Y02​+2025023455040​X12​X22​Y0​Y1​+20250231034240​X12​X22​Y0​Y2​+1090397562860​X12​X22​Y12​+20250233340800​X12​X22​Y1​Y2​+184277093493383120​X12​X22​Y22​+14513184072104240​X12​Y04​+1319380371019160​X12​Y03​Y1​+145131840716813600​X12​Y03​Y2​+145131840733134100​X12​Y02​Y12​+145131840781897720​X12​Y02​Y1​Y2​+188671392911349734240​X12​Y02​Y22​+2073312018977240​X12​Y0​Y13​+188482912696160​X12​Y0​Y12​Y2​+2695305613954313560​X12​Y0​Y1​Y22​+26953056131433297120​X12​Y0​Y23​+2073312017250535​X12​Y14​+20733120132310400​X12​Y13​Y2​+385043659216172800​X12​Y12​Y22​+26953056134527451800​X12​Y1​Y23​+26953056134984688000​X12​Y24​+637500​X1​X25​+9020557939320​X1​X23​Y02​+18409386400​X1​X23​Y0​Y1​+184093204800​X1​X23​Y0​Y2​+1417516113469240​X1​X23​Y12​+184093691200​X1​X23​Y1​Y2​+184093963700​X1​X23​Y22​+99127240​X1​X2​Y04​+99127720​X1​X2​Y03​Y1​+99127960​X1​X2​Y03​Y2​+641411140​X1​X2​Y02​Y12​+991271440​X1​X2​Y02​Y1​Y2​+1288651102080​X1​X2​Y02​Y22​+1557718640​X1​X2​Y0​Y13​+15577115360​X1​X2​Y0​Y12​Y2​+18409386400​X1​X2​Y0​Y1​Y22​+184093204800​X1​X2​Y0​Y23​+1557719720​X1​X2​Y14​+15577134560​X1​X2​Y13​Y2​+20250232003160​X1​X2​Y12​Y22​+184093691200​X1​X2​Y1​Y23​+184093819200​X1​X2​Y24​+5796774842​X26​+9020557509045​X24​Y02​+18409354000​X24​Y0​Y1​+184093128000​X24​Y0​Y2​+1090397603765​X24​Y12​+184093432000​X24​Y1​Y2​+1675246351468875​X24​Y22​+17151944819412020​X22​Y04​+171519448162085015​X22​Y03​Y1​+1715194481106920360​X22​Y03​Y2​+141751611486370​X22​Y02​Y12​+1715194481566305605​X22​Y02​Y1​Y2​+1715194481542511880​X22​Y02​Y22​+24502778338527855​X22​Y0​Y13​+245027783164423170​X22​Y0​Y12​Y2​+245027783313889655​X22​Y0​Y1​Y22​+245027783299349720​X22​Y0​Y23​+24502778324249915​X22​Y14​+245027783128600795​X22​Y13​Y2​+245027783376100840​X22​Y12​Y22​+245027783809485665​X22​Y1​Y23​+245027783772902080​X22​Y24​+158389158399​Y06​+2262715​Y05​Y1​+931710​Y05​Y2​+17422795575​Y04​Y12​+1583891305​Y04​Y1​Y2​+2941513030​Y04​Y22​+1583891515​Y03​Y13​+174227950200​Y03​Y12​Y2​+2059057130590​Y03​Y1​Y22​+2059057149150​Y03​Y23​+174227933015​Y02​Y14​+1742279118095​Y02​Y13​Y2​+226496273882330​Y02​Y12​Y22​+2059057740280​Y02​Y1​Y23​+2059057579340​Y02​Y24​+2488975600​Y0​Y15​+226272400​Y0​Y14​Y2​+3235661927325​Y0​Y13​Y22​+32356612239350​Y0​Y12​Y23​+294151290535​Y0​Y1​Y24​+294151154840​Y0​Y25​+248897251777​Y16​+24889718080​Y15​Y2​+3235661737865​Y14​Y22​+32356611795265​Y13​Y23​+32356613164115​Y12​Y24​+294151281505​Y1​Y25​+294151403911​Y26​.​

The definition AAA is the element A=X03Y03A=X_0^3Y_0^3A=X03​Y03​ of C[X0,X1,X2,Y0,Y1,Y2]\mathbb C[X_0,X_1,X_2,Y_0,Y_1,Y_2]C[X0​,X1​,X2​,Y0​,Y1​,Y2​], where (X0,X1,X2,Y0,Y1,Y2)(X_0,X_1,X_2,Y_0,Y_1,Y_2)(X0​,X1​,X2​,Y0​,Y1​,Y2​) are the six polynomial variables corresponding in order to indices 0,1,2,3,4,50,1,2,3,4,50,1,2,3,4,5.

The definition qqq is the natural number 111.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me