The import-free starved kill at n ≥ 123 (bulk-credited moat) #
Counting/V9Discharge.lean closes the starved census import-free from n ≥ 388, at ball radius
r = ⌊(⌊(n+8)/9⌋ − 1)/2⌋ — the radius the old moat threshold 9k ≤ n + 8 allows.
Counting/MoatSharp.lean sharpens that threshold to 12k + X ≤ 2n by keeping the bulk excess
Σ_{S₂}(deg − 3) that master_cycle_fires discards. The admissible radius rises to
r = ⌊(2n − X − 12)/24⌋,
and re-running the same discharge with it drops the import-free threshold from 388 to 123.
Why 123. The integer condition |V₉|² < |V₉|(2r+1) + t₉(3r² − r) holds on the whole
counting region from n = 111 upward; the discharge below makes the same two relaxations as the
388 route — r replaced by its uniform lower bound (24r ≥ 2n − X − 35, dropping ⌊·⌋) and the
region replaced by an H-monotone endpoint — landing the proved threshold at 123.
Route. Unlike the 388 version, the radius now depends on X, so the excess term carries
A = 2N − X − 35 rather than an X-free square. Both t₉ and A are bounded below by X-free
linear forms that are simultaneously tight at X = X_max, so pushing X to the master maximum
costs nothing: 10·t₉ ≥ 6N + 160 − 23H and 10·A ≥ 16N + 7H − 150. What remains is a two-
variable cubic that is monotone decreasing in H (every H-coefficient is negative at N ≥ 123),
so its minimum sits at 17H = 4N − 200; there 4913·gap − cubic splits exactly as a sum of
three manifestly non-negative products, and strip_cubic_sharp closes.
The arithmetic core #
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³), which is what nlinarith finds.
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.
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.
The sharp strip Moore arithmetic. On the counting region, MASTER′ together with
H ≤ X, N ≥ 123 and the sharpened radius bound 2N − X − 35 ≤ 24R forces the SQRT side
condition
(N − H)² < (N − H)(2R + 1) + (N − 4 − X − 3H)(3R² − R).
Route: moore_strip_core_sharp supplies the R-free inequality; then 12(2R+1) ≥ 2N−X−23
upgrades the ball term and 23(2N−X−35)² ≤ 4608(3R²−R) the excess term (from (2N−X−35)² ≤ 576R² and 23R² ≤ 8(3R²−R), the latter by R ≥ 8), both by the same factor 4608 = 384·12.
The graph-level dispatch #
The sharpened tier-9 girth. In a never-firing starved census, V₉ contains no cycle of
length k with 12k + X ≤ 2n — against 9k ≤ n + 8 for v9_girth.
The rebased tier-9 kill at the sharpened moat obligation. Identical to
starved_v9_kill_sqrt except that the moat obligation is 12(2r+1) + X ≤ 2n rather than
9(2r+1) ≤ n + 8: the cycle the ball count produces has length at most 2r + 1, and a V₉-cycle
that short fires v9_short_cycle_fires_sharp.
D3′ — the import-free starved kill at n ≥ 123. A never-firing starved census
(m = 2(n−2), δ ≥ 3, hs0) on 123 ≤ n cannot exist, with no external girth byline. Same
single branch as starved_dead_ge_388, run at the bulk-credited radius
r = ⌊(2n − X − 12)/24⌋ and discharged by moore_strip_arith_sharp.