Arithmetic core of the joint maximal-divisor algorithm

The paper's independent 2C estimate is replaced by a certified square envelope M^2 ≤ S. This removes square roots and division from both the connectivity test and the rank-refinement bound.

theorem BGS.NumberTheory.jointSquareEnvelope_failure_of_firstInterval {p n M S : ℕ} (hn : n + 2 ≤ 4 * p) (hfirst : 128 * p < (3 * M) ^ 8) (hSquare : M ^ 2 ≤ S) : 32 * (n + 2) < 3 ^ 8 * S ^ 4

A paper-style first-interval witness forces failure of the joint square test.

theorem BGS.NumberTheory.jointRankRefinement_of_firstInterval {d M C S : ℕ} (hfirst : 4 * d < 81 * M ^ 3) (hLinear : M ≤ 2 * C) (hSquare : M ^ 2 ≤ S) : 2 * d < 81 * C * S

The joint envelope shrinks the divisor range in the rank-refinement step from the paper's 162 C^3 to the root-free bound 81 C S / 2.

theorem BGS.NumberTheory.no_firstInterval_of_jointSquareEnvelope {p n M S : ℕ} (hn : n + 2 ≤ 4 * p) (hSquare : M ^ 2 ≤ S) (hpasses : 3 ^ 8 * S ^ 4 ≤ 32 * (n + 2)) : ¬128 * p < (3 * M) ^ 8

If the joint square test succeeds, no first-interval witness can exist.