A direction where the highest homogeneous component is nonzero gives full outer degree after the explicit affine coordinate change. Its leading coefficient is the scalar obtained by evaluating that component.

theorem CCDN.hypersurfaceAffineCoordinates_top_coefficient {K : Type u_1} {σ : Type u_2} [Field K] (a b : Option σ → K) (hb : b none ≠ 0) (f : MvPolynomial (Option σ) K) : ((MvPolynomial.optionEquivLeft K σ) ((hypersurfaceAffineCoordinates a b hb) f)).coeff f.totalDegree = MvPolynomial.C ((MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent f.totalDegree) f))

The top outer coefficient is a constant polynomial, and its scalar is exactly the leading homogeneous form evaluated on the chosen direction.

theorem CCDN.hypersurfaceAffineCoordinates_full_outer_degree {K : Type u_1} {σ : Type u_2} [Field K] (a b : Option σ → K) (hb : b none ≠ 0) (f : MvPolynomial (Option σ) K) (hdir : (MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent f.totalDegree) f) ≠ 0) : ((MvPolynomial.optionEquivLeft K σ) ((hypersurfaceAffineCoordinates a b hb) f)).natDegree = f.totalDegree

Nonvanishing in the direction forces the outer degree to be the original total degree, even after moving an arbitrary base point to the origin.