Right-inversion pairing with Euler budget seven

For bidegree (2,2) and Euler budget 7, the source cube-root branch is 3 * (56mn)^(1/3). Right-coordinate inversion divides the nonparabolic support by two. The resulting root coefficient has cube

((3/2) * 56^(1/3))^3 = 189.

The quotient-by-characteristic coefficient remains exactly 24.

noncomputable def BGS.Markoff.pairedEulerSevenCorvajaZannierTraceUpperBound (p leftOrder rightOrder : ℕ) : ℝ

The exact right-inversion-paired χ≤7 numerical bound.

Equations

• BGS.Markoff.pairedEulerSevenCorvajaZannierTraceUpperBound p leftOrder rightOrder = max (3 / 2 * (56 * ↑(leftOrder * rightOrder)) ^ (1 / 3)) (24 * (↑(leftOrder * rightOrder) / ↑p))

theorem BGS.Markoff.corvajaZannierCorollaryTwoNumericalBound_bidegree_two_euler_seven_eq_twice_paired (p leftOrder rightOrder : ℕ) : corvajaZannierCorollaryTwoNumericalBound p leftOrder rightOrder 2 2 7 = 2 * pairedEulerSevenCorvajaZannierTraceUpperBound p leftOrder rightOrder

The source χ≤7 bound is exactly twice the paired bound.

theorem BGS.Markoff.weightedTraceEquationNonparabolicLeftSupport_card_cast_le_pairedEulerSeven (p : ℕ) [Fact (Nat.Prime p)] (E : Type u_1) [Field E] [Fintype E] [CharP E p] (alpha beta : E) (Hleft Hright : Subgroup Eˣ) (hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta) : ↑(weightedTraceEquationNonparabolicLeftSupport alpha beta Hleft Hright).card ≤ pairedEulerSevenCorvajaZannierTraceUpperBound p (Nat.card ↥Hleft) (Nat.card ↥Hright)

The weighted-trace χ≤7 theorem combined with right inversion gives the exact nonparabolic left-support estimate whose root coefficient cubes to 189.