Quadratic pullback · residual density — instance data

Definition

HodgeComputerQuadraticCubicPullback

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

algebraic-geometryhodge-computerquadratic-cubic-pullback

The exact fixed polynomials and pole parameter for “Quadratic pullback · residual density”, over $\mathbb C$ with coordinates $X_0,X_1,X_2,Y_0,Y_1,Y_2$ :

F=\sum_{i=0}^5 Q_i^3.

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

where

\begin{aligned} Q_0&=X_{0}^{2} + \frac{5 \cdot X_{1} \cdot X_{2}}{7} + \frac{5 \cdot Y_{0} \cdot Y_{1}}{7} \\ Q_1&=\frac{5 \cdot X_{0} \cdot X_{2}}{11} + X_{1}^{2} + \frac{5 \cdot Y_{1} \cdot Y_{2}}{11} \\ Q_2&=\frac{5 \cdot X_{0} \cdot X_{1}}{13} + X_{2}^{2} + \frac{5 \cdot Y_{0} \cdot Y_{2}}{13} \\ Q_3&=\frac{5 \cdot X_{0} \cdot X_{1}}{17} + Y_{0}^{2} + \frac{5 \cdot Y_{1} \cdot Y_{2}}{17} \\ Q_4&=\frac{5 \cdot X_{1} \cdot X_{2}}{19} + \frac{5 \cdot Y_{0} \cdot Y_{2}}{19} + Y_{1}^{2} \\ Q_5&=\frac{5 \cdot X_{0} \cdot X_{2}}{23} + \frac{5 \cdot Y_{0} \cdot Y_{1}}{23} + Y_{2}^{2} \end{aligned}

Definition code

import Definitions.Def_DiamondCertificate

set_option autoImplicit false
noncomputable section
namespace HodgeComputer.QuadraticCubicPullback
def n : ℕ := 5
def d : ℕ := 6
def F : HodgeComputer.AmbientPoly n := (((((((((((((((((((((((((((((((((((((((((((((((((((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (6 : ℕ)) + (((((15 : 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 / 7 : ℂ))) + (((((15 : 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 : ℂ))) + ((((888750 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 10793861 : ℂ))) + ((((1687250 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 16194277 : ℂ))) + (((((2599425 : 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 / 1002001 : ℂ))) + (((((75 : 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 / 289 : ℂ))) + ((((((375 : 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 / 2197 : ℂ))) + ((((((375 : 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 / 4913 : ℂ))) + (((((((150 : 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 / 49 : ℂ))) + ((((((375 : 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 / 12167 : ℂ))) + ((((((375 : 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 / 1331 : ℂ))) + (((((75 : 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 / 529 : ℂ))) + (((((75 : 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 / 49 : ℂ))) + (((((15 : 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 / 11 : ℂ))) + (((((((150 : 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 / 121 : ℂ))) + (((((15 : 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 / 13 : ℂ))) + (((((((150 : 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 / 169 : ℂ))) + (((((15 : 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 / 17 : ℂ))) + (((((((150 : 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 / 289 : ℂ))) + ((((((375 : 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 / 2197 : ℂ))) + ((((((375 : 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 / 4913 : ℂ))) + ((((((375 : 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 / 12167 : ℂ))) + (((((((150 : 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 / 529 : ℂ))) + ((((((375 : 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 / 1331 : ℂ))) + (((((15 : 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 / 23 : ℂ))) + ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (6 : ℕ))) + (((((15 : 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 / 11 : ℂ))) + ((((900250 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (1 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 2352637 : ℂ))) + ((((((375 : 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 / 343 : ℂ))) + ((((((375 : 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 / 6859 : ℂ))) + (((((75 : 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 / 361 : ℂ))) + (((((75 : 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 / 121 : ℂ))) + ((((((375 : 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 / 343 : ℂ))) + ((((((375 : 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 / 6859 : ℂ))) + (((((((150 : 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 / 361 : ℂ))) + (((((15 : 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 / 19 : ℂ))) + ((MvPolynomial.X (R := ℂ) (2 : Fin 6)) ^ (6 : ℕ))) + (((((15 : 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 / 13 : ℂ))) + (((((75 : 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 / 169 : ℂ))) + ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (6 : ℕ))) + (((((15 : 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 / 17 : ℂ))) + ((((1563750 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 4173281 : ℂ))) + ((((1132000 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 15069223 : ℂ))) + (((((33613425 : 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 / 55190041 : ℂ))) + (((((15 : 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 / 19 : ℂ))) + (((((15 : 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 / 23 : ℂ))) + ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (6 : ℕ))) + ((((780500 : MvPolynomial (Fin 6) ℂ) * ((MvPolynomial.X (R := ℂ) (4 : Fin 6)) ^ (3 : ℕ))) * ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (3 : ℕ))) * MvPolynomial.C (σ := Fin 6) (1 / 6539203 : ℂ))) + ((MvPolynomial.X (R := ℂ) (5 : Fin 6)) ^ (6 : ℕ)))
def A : HodgeComputer.AmbientPoly n := (((MvPolynomial.X (R := ℂ) (0 : Fin 6)) ^ (3 : ℕ)) * ((MvPolynomial.X (R := ℂ) (3 : Fin 6)) ^ (3 : ℕ)))
def q : ℕ := 1
end HodgeComputer.QuadraticCubicPullback

Source

https://github.com/hodge-computer/sextics/blob/83fbf5c9a0afe9136ce4f1ed324d085a2c899bd0/data/quadratic-cubic-pullback/instance.rec

Read-back

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

The definition $n$ is the natural number $5$ .

The definition $d$ is the natural number $6$ .

The definition $F$ is the following element of the polynomial ring $R=\mathbb C[X_0,X_1,X_2,Y_0,Y_1,Y_2]$ in six algebraically independent variables, corresponding in order to indices $0,1,2,3,4,5$ :

\begin{aligned} F={}&\left(X_0^2+\frac57(X_1X_2+Y_0Y_1)\right)^3\\ &+\left(X_1^2+\frac5{11}(X_0X_2+Y_1Y_2)\right)^3\\ &+\left(X_2^2+\frac5{13}(X_0X_1+Y_0Y_2)\right)^3\\ &+\left(Y_0^2+\frac5{17}(X_0X_1+Y_1Y_2)\right)^3\\ &+\left(Y_1^2+\frac5{19}(X_1X_2+Y_0Y_2)\right)^3\\ &+\left(Y_2^2+\frac5{23}(X_0X_2+Y_0Y_1)\right)^3. \end{aligned}

The definition $A$ is the element $A=X_0^3Y_0^3$ of $\mathbb C[X_0,X_1,X_2,Y_0,Y_1,Y_2]$ , where $(X_0,X_1,X_2,Y_0,Y_1,Y_2)$ are the six polynomial variables corresponding in order to indices $0,1,2,3,4,5$ .

The definition $q$ is the natural number $1$ .

Human review

Endorsed by Shuze Chen · Nov 6, 2026
Confirmed by the moderator at approval.
Endorsed by benediamond · Nov 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph