q2 — how far down does T2(13,p) hold, and can it be proved for all large p

q1 decided T2(13,p) one prime at a time: it holds at twenty primes from 191 to 293 and fails at every prime up to 41, with p=43 not resolving in 40 minutes. q2 attacks the two ends of that gap with tools that do not search one prime at a time.

gcc -O3 -std=c11 -o cells cells.c
gcc -O3 -std=c11 -o probe probe.c

The failing end: an exact family

schema.py needs no search at all. For v = e_a + e_b — two coordinates 1, the rest 0 — a counting argument on the m-1 = 13 nonzero values of s collapses "is v unsaved at p" to a question about the other 11 speeds:

v = e_a + e_b is unsaved at p ⟺ no j ∈ Z_p has ‖i·j/p‖ ≥ 1/14 for every i ∈ {1,…,13} \ {a,b}.

So T2(13,p) fails as soon as some pair of speeds can be deleted and still leave the remaining eleven without a witness on the grid (1/p)Z, even though they have one on the circle. schema.py computes the good set G(Z) ⊆ [0,1) exactly, as a union of closed intervals over D = 14·lcm(1..13) = 5045040, and decides every p at once.

python3 schema.py --k 13

The holding end: one search for every large p at once

cells.c replaces the grid (1/p)Z by the exact cell decomposition of the circle. B_i(t) = ⌊14·frac(i t)⌋ jumps only on (1/(14 i))Z, so on each half-open cell of the arrangement generated by those 812 breakpoints the entire hitting structure is constant. Every half-open interval of length 1/p contains a point of (1/p)Z, so for p ≥ q an unsaved v must hit, for every s and every cell start c_r, at least one cell meeting [c_r, c_r + 1/q). That is again a set-cover feasibility question, and

no eligible v covers all of it ⟹ T2(13,p) holds for every integer p ≥ q.

The constraints only get stronger as q grows, so one run at q certifies an infinite tail. --strictcell is the weaker first version (long cells only, no window union); --p P reproduces q1/cover.c's own constraint set so the two programs can be compared on the same question.

Gates

python3 check_cells.py --selftest        # the reduction, from the paper
./cells --k 5 --p 31   ./cells --k 7 --p 59      # UNSAT, as q1/cover.c
./cells --k 5 --p 6    ./cells --k 7 --p 8       # SAT,   as q1/cover.c
./cells --k 13 --p 14                            # SAT,   same witness

check_cells.py --selftest checks, independently of the C: that B is constant on every half-open cell (sampled); that every window really does meet (1/p)Z inside its own cell set, for k = 5, 7, 13 and 43 values of p; that schema.py's interval arithmetic agrees with exhausting all (s,j) directly, over 1240 pair-by-p checks at k=5 and 9672 at k=13, with no mismatch; and that brute force over all of Z_6^5 agrees with the certified threshold at k=5. Grid mode reproduces q1/cover.c on all five gate cases, witnesses included.

Files