Scalar certificates for the graph bounds

Keeping these integer and real arguments independent of graph definitions lets them elaborate while the graph infrastructure builds.

theorem ACMax.Arithmetic.strip_cubic_sharp {N : ℤ} (hN : 123 ≤ N) : 779812849 * N + 755972700 < 20700 * N ^ 3 + 3914436 * N ^ 2

The sharp strip cubic. The single-variable inequality the n ≥ 123 region arithmetic bottoms out at, after X is pushed to its master maximum and H to the end of its range. Substituting N = 123 + u makes every coefficient non-negative (1068496017 + 1122649307u + 11552736u² + 20700u³), giving an explicit positive certificate.

theorem ACMax.Arithmetic.moore_strip_twovar_sharp {N H : ℤ} (hN : 123 ≤ N) (hH : 0 ≤ H) (hs : 17 * H ≤ 4 * N - 200) : 4608000 * (N - H) ^ 2 < 38400 * ((N - H) * (16 * N + 7 * H - 30)) + 23 * ((6 * N + 160 - 23 * H) * (16 * N + 7 * H - 150) ^ 2)

The two-variable core. After both X-eliminations the target is a cubic in (N, H):

4608000·(N−H)² < 38400·(N−H)·(Q+120) + 23·P·Q², P = 6N+160−23H, Q = 16N+7H−150.

Every H-coefficient of the gap is negative at N ≥ 123, so the minimum is at 17H = 4N − 200, and 4913·gap − cubic is identically 289(M−17H)(−c₁) + 17(M²−(17H)²)(−c₂) + (M³−(17H)³)·25921 with M = 4N − 200, −c₁ = 104512N² − 11944120N + 18478500 ≥ 0 (its larger root is ≈ 112.7) and −c₂ = 111734N + 3585580 ≥ 0. So linarith closes on those three products plus the cubic.

theorem ACMax.Arithmetic.moore_strip_core_sharp {N X H : ℤ} (hN : 123 ≤ N) (hH : 0 ≤ H) (hHX : H ≤ X) (hmaster : 10 * X + 7 * H ≤ 4 * N - 200) : 4608 * (N - H) ^ 2 < 384 * ((N - H) * (2 * N - X - 23)) + 23 * ((N - 4 - X - 3 * H) * (2 * N - X - 35) ^ 2)

The R-free core of the sharp strip discharge. On the counting region (0 ≤ H ≤ X, 10X + 7H ≤ 4N − 200) at N ≥ 123,

4608·(N−H)² < 384·(N−H)·(2N−X−23) + 23·(N−4−X−3H)·(2N−X−35)².

Both X-dependent factors are pushed to the master maximum simultaneously — 10·t ≥ 6N+160−23H and 10·A ≥ 16N+7H−150, equalities together at X = X_max — and moore_strip_twovar_sharp closes what is left.

Sigma cross-slot slack

theorem ACMax.Arithmetic.sigma_cross_arithmetic (left right total_left total_right fraction_left fraction_right : ℝ) (hleft : total_left + fraction_left ≤ 2) (hright : total_right + fraction_right ≤ 2) (hleft0 : 0 ≤ fraction_left) (hright0 : 0 ≤ fraction_right) (hleft1 : fraction_left ≤ 1) (hright1 : fraction_right ≤ 1) : (left * fraction_left + right * fraction_right) ^ 2 - (left * fraction_left) ^ 2 - (right * fraction_right) ^ 2 + left ^ 2 * total_left + right ^ 2 * total_right ≤ 2 * left ^ 2 + 2 * right ^ 2

The two sigma slack budgets absorb the unique crossing cost.