Coarse support tails below the paper scale

The single clean threshold 2^756 < p, together with the simultaneous tenth-moment divisor estimate, discharges the non-cubic middle-game, primitive-endgame, cage, and split-sign support inequalities.

theorem BGS.Markoff.twentyFour_support_margin : 24 ^ 15 * 2 ^ 687 < 2 ^ 756

theorem BGS.Markoff.sixtyEight_support_margin : 68 ^ 15 * 2 ^ 1374 < 2 ^ 1512

theorem BGS.Markoff.cageCoefficient_support_margin : 100522 ^ 10 * 2 ^ 916 < 2 ^ 2268

theorem BGS.Markoff.seven_le_of_twoPow756_lt {p : ℕ} (hp : 2 ^ 756 < p) : 7 ≤ p

theorem BGS.Markoff.twentyFour_mul_lt_rpow_one_div_six_of_twoPow756 {p T : ℕ} (hp : 2 ^ 756 < p) (hmoment : T ^ 10 ≤ 2 ^ 458 * p) : ↑(24 * T) < ↑p ^ (1 / 6)

The linear-tail theorem at the unified clean support cutoff.

theorem BGS.Markoff.sixtyEight_mul_square_lt_rpow_one_div_three_of_tenthMoment {p T : ℕ} (hpCoefficient : 68 ^ 15 * 2 ^ 1374 < p ^ 2) (hmoment : T ^ 10 ≤ 2 ^ 458 * p) : ↑(68 * T ^ 2) < ↑p ^ (1 / 3)

The weighted primitive-endgame divisor term is below p^(1/3).

theorem BGS.Markoff.preliminary_sixtyEight_mul_divisorSum_sq_lt_rpow_one_div_three_of_twoPow756 {p : ℕ} (hp : 2 ^ 756 < p) : ↑(68 * ((p - 1).divisors.card + (p + 1).divisors.card) ^ 2) < ↑p ^ (1 / 3)

theorem BGS.Markoff.cageCoefficient_mul_square_lt_sqrt_of_tenthMoment {p T : ℕ} (hpCoefficient : 100522 ^ 10 * 2 ^ 916 < p ^ 3) (hmoment : T ^ 10 ≤ 2 ^ 458 * p) : ↑(100522 * T ^ 2) < √↑p

The cage coefficient times the squared divisor sum is below sqrt p.

theorem BGS.Markoff.preliminary_cageCoefficient_mul_divisorSum_sq_lt_sqrt_of_twoPow756 {p : ℕ} (hp : 2 ^ 756 < p) : ↑(100522 * ((p - 1).divisors.card + (p + 1).divisors.card) ^ 2) < √↑p

theorem BGS.Markoff.coarse_endgamePrimitiveTrace_explicitInequality {p orbitExponent coefficient : ℕ} (hp : 2 ^ 756 < p) (horbit : ↑orbitExponent ≤ 2 * ↑p ^ (1 / 6)) (hcoefficient : coefficient ≤ 34) : ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

Primitive trace inclusion--exclusion above the unified support cutoff.

theorem BGS.Markoff.coarse_endgamePrimitiveTrace_explicitInequality_of_card_sub_one {p orbitExponent orbitOrder coefficient : ℕ} (hp : 2 ^ 756 < p) (hmul : orbitExponent * orbitOrder = p - 1) (horder : ↑p ^ (5 / 6) ≤ ↑orbitOrder) (hcoefficient : coefficient ≤ 34) : ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

theorem BGS.Markoff.coarse_endgamePrimitiveTrace_explicitInequality_of_card_add_one {p orbitExponent orbitOrder coefficient : ℕ} (hp : 2 ^ 756 < p) (hmul : orbitExponent * orbitOrder = p + 1) (horder : ↑p ^ (5 / 6) ≤ ↑orbitOrder) (hcoefficient : coefficient ≤ 34) : ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

theorem BGS.Markoff.coarse_four_lt_rpow_five_div_six {p : ℕ} (hp : 2 ^ 756 < p) : 4 < ↑p ^ (5 / 6)

theorem BGS.Markoff.coarse_cageWitness_explicitInequality {p coefficient : ℕ} (hp : 2 ^ 756 < p) (hcoefficient : coefficient ≤ 100522) : ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

Cage connectivity inequality above the unified support cutoff.

theorem BGS.Markoff.coarse_halfOrderThreshold {p : ℕ} (hp : 2 ^ 756 < p) : ↑p ^ (5 / 6) ≤ ↑((p - 1) / 2)

The half-order sign threshold is automatic above 2^756.