Arithmetic criterion for the nonparabolic complement route

The complement count supplies 8 * p ≤ (d * M) ^ 2. The exact Euler-characteristic coefficient anticipated by the strengthened Corvaja--Zannier step gives d ≤ 189 * M ^ 3. Eliminating d yields the integer obstruction 8 * p ≤ 189 ^ 2 * M ^ 8.

A root-free square envelope M ^ 2 ≤ S then gives 8 * p ≤ 35721 * S ^ 4.

theorem BGS.NumberTheory.eight_mul_le_189_sq_mul_eighth_of_le_square_of_le_189_mul_cube {p d M : ℕ} (hcount : 8 * p ≤ (d * M) ^ 2) (hdegree : d ≤ 189 * M ^ 3) : 8 * p ≤ 189 ^ 2 * M ^ 8

Eliminate the maximal order d from the nonparabolic complement count using the exact coefficient 189.

theorem BGS.NumberTheory.eight_mul_le_35721_mul_fourth_of_le_189_sq_mul_eighth {p M S : ℕ} (hbad : 8 * p ≤ 189 ^ 2 * M ^ 8) (hSquare : M ^ 2 ≤ S) : 8 * p ≤ 35721 * S ^ 4

Replace M by any certified square envelope S; 189^2 = 35721.

theorem BGS.NumberTheory.eight_mul_le_35721_mul_fourth_of_count_degree_squareEnvelope {p d M S : ℕ} (hcount : 8 * p ≤ (d * M) ^ 2) (hdegree : d ≤ 189 * M ^ 3) (hSquare : M ^ 2 ≤ S) : 8 * p ≤ 35721 * S ^ 4

Combined root-free obstruction for the nonparabolic complement route.