Transport of the constructed good hyperplane to coordinates suited to the universal Noether family.

theorem CCDN.graphHyperplaneRestriction_rename {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing K] [Fintype σ] [Fintype τ] (e : σ ≃ τ) (a : τ → K) (f : MvPolynomial (Option σ) K) : (MvPolynomial.rename ⇑e) ((graphHyperplaneRestriction (a ∘ ⇑e)) f) = (graphHyperplaneRestriction a) ((MvPolynomial.rename ⇑e.optionCongr) f)

Restriction to the graph hyperplane x_none = ∑ a j * x j commutes with renaming the coordinates along an equivalence e.

theorem CCDN.exists_geometrically_good_graph_reindexed {n : ℕ} (f : MvPolynomial (Option (Option (Fin (2 + n)))) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) : ∃ (a : Option (Fin (2 + n)) → ℚ), AbsolutelyIrreducibleRat ((graphHyperplaneRestriction a) ((MvPolynomial.map (Int.castRingHom ℚ)) f))

The constructed bounded integer normal yields a geometrically integral rational graph section in the double-Option coordinates.