files / problems / lonely-runner-fourteen / compute / q1 / certs / T2_p191.txt
T2(13,191) HOLDS
=================
Statement verified
------------------
For every v in (Z/14Z)^13 such that
(i) some coordinate v_i = 0,
(ii) at least two coordinates are odd,
(iii) at least two coordinates are not divisible by 7,
there exist s in Z/14Z and j in Z with
s*v + r_13(j/191) in {1,...,12}^13 (mod 14),
where r_13(t)_i = floor(14*{i*t}), so r_13(j/p)_i = floor(14*((i*j mod p))/p).
(ii)+(iii) says exactly that v is NOT disposed of by the gcd condition of
ST26 Definition 2.1 with l = k+1 = 14: for a prime q | 14, "some i has
q | v_j for all j != i" is the same as "#{ j : q does not divide v_j } <= 1".
What it gives
-------------
Combining with the other two branches of ST26 Proposition 4.4 (u' gcd-proper
-> gcd condition; u' with no zero coordinate -> t = 1/14):
every u in pi^{-1}_{14*191 -> 191}(1,2,...,13) is (13,191,14)-proper,
hence (1,2,...,13) is eventually (13,191)-proper, i.e. (1,2,...,13) is not in
J(13,191). In the form of ST26 Proposition 1.4:
THEOREM. Every (u_1,...,u_13) in Z^13_{>0} with gcd(u_1,...,u_13) = 1 and
u_i = i (mod 191) for all i has the lonely runner property,
i.e. there is t with ||t u_i|| >= 1/14 for all i.
ST26 prove the analogue only when k+1 AND p are both odd primes. Here
k+1 = 14 is composite, so their Proposition 1.4 does not apply, and this
statement is not covered by the published record. LRC(13) remains open:
ST26 Section 7 names computing I(13,p,1) (about 1.1e17 tuples at p=191 under
their Section 5.1 reduction) as the k=13 bottleneck, and that is untouched
here.
How it was decided
------------------
Reformulation (see ATTACK.md 2026-08-22). With B^{(j)}_i = floor(14*{i j/p}),
call (s,j) a constraint and say coordinate i taking value a HITS it when
s*a + B^{(j)}_i is 0 or 13 mod 14. Then v has no witness iff the sets
hit(i, v_i) cover all 14p constraints. So the question is set-cover
feasibility in 13 variables of 14 values -- not an enumeration over the
14^13 - 13^13 - 1 = 7.9e14 candidate vectors.
tool compute/q1/cover.c (backtracking over constraints, MRV + counting bound)
command ./cover --k 13 --p 191
result RESULT UNSAT ... T2(13,191) HOLDS
nodes 102905279 bound_cuts 80243639 dead_cuts 8002240
seconds 240.73 constraints 1181 (after dropping s=0, merging (s,j)~(-s,p-j))
Two exact reductions are used and both are asserted at run time, not assumed:
* every s=0 constraint is hit by every v, because some coordinate of
r_13(j/p) is always 0 or 13 -- equivalently (1,...,13) has no witness time
in (1/p)Z, which is Goddyn-Wong tightness. cover.c aborts if this fails.
* (s,j) and (-s, p-j) induce the same hitting set; duplicates merged.
Independent checks
------------------
1. Reformulation vs brute force. compute/q1/check_unsaved.py enumerates ALL
of Z_m^k directly from the paper's definitions and agrees:
k=5, m=6 (composite): p-independent 64 obstructions; p=31 0
k=7, m=8 (composite): p-independent 2596 obstructions; p=59 0
cover.c returns SAT / UNSAT matching each of those four.
check_unsaved.py --selftest also re-proves ST26 Proposition 4.1 outright at
k=4 and k=6 by exhausting N_k.
2. Second decision procedure. compute/q1/cover_bdd.c sweeps coordinates
forward carrying the surviving pair set, keeps the FULL 14p pair set with
none of cover.c's reductions, and agrees on k=5 p=6, k=5 p=31, k=7 p=8,
k=7 p=59, k=8 p=9. It state-explodes before k=13 (no dominance pruning),
so it does NOT independently confirm p=191. Recorded as a limit.
3. Split/unsplit agreement. ./cover --k 13 --p 191 --split 2 --part {0,1}
and the unsplit run give the same verdict; unsplit is reproducible at
exactly 102905279 nodes.
4. Adversarial sampling at p=191 (compute/q1/spotcheck.c, which rebuilds the
pair sets from scratch and shares no code with either search). Zero
unsaved-and-needed vectors from:
sparse (support <= 3) 342576 needing a witness
ap (v_i = a i + b, and all 2-coordinate perturbations) 2918238
perturb (Hamming ball radius 2 about two known obstructions) 59178
random (20,000,000 uniform with a forced zero) 19936642
Positive control: the same tool finds 24300 obstructions in the sparse
family at p = 14 (the p-independent grid), so it is not blind.
Related facts established the same day
--------------------------------------
* T1(191) -- the same statement WITHOUT the gcd branch, which is what the
2026-08-17 campaign was searching for -- is FALSE. Witness
v = 2*(1,...,13) mod 14 = (2,4,6,8,10,12,0,2,4,6,8,10,12), in N_13, no
witness among all 2674 pairs (s,j). It is entirely even, so gcd-proper.
python3 check_unsaved.py --k 13 --p 191 --v 2,4,6,8,10,12,0,2,4,6,8,10,12
* T2(13,14) -- the p-independent statement -- is FALSE, with a genuine
(non-gcd-proper) obstruction v = (1,1,1,0,1,1,1,5,1,6,1,2,1). So p
dependence is required and 191 is doing real work.