Powered-image index two for the weighted trace curve

Three always-present monomials of the nonzero-weight trace closure have exponents (1,0), (2,1), and (0,1). Their support determinant is 2. Retaining this exact sparse-support certificate lowers the source-to-powered image index bound from the generic bidegree value 8 to 2.

theorem BGS.Markoff.weightedTraceTorusClosure_poweredImageIndex_le_two {K : Type u_1} [Field K] {p : ℕ} [CharP K p] (alpha beta : K) (hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmPrime : ¬p ∣ m) (hnPrime : ¬p ∣ n) : let f := weightedTraceTorusClosurePolynomial alpha beta; have hf := ⋯; Module.finrank (↥(CorvajaZannier.PoweredImageOverFirst f m n)) (CorvajaZannier.PlaneCurveFunctionField f) ≤ 2

The exact support determinant gives powered-image index at most two for every prime-to-characteristic pair of powers.