HIVE-LRC: An Auditable Stopping Point after D20–D34

Cross-Prime Coupling, Exact Evaluation, and Scoped Computational Obstructions · HIVE-LRC gates D20–D34

Abstract

The Lonely Runner Conjecture asks whether, for every set of distinct positive integer speeds \(V_1,\dots,V_k\), some time places every runner at least \(1/(k+1)\) of a lap from the origin. Computer-assisted work settles \(k\le 12\); HIVE-LRC targets \(k=13\), the first open case. Under a human-in-command, verifier-linked protocol (Human Intelligence and Verifiable Exploration), gates D20–D34 explored a family of prime-product, coupling, symbolic, and search architectures. We report four internally proved theorems and one certified-in-envelope exact algorithm, together with a scoped negative-capability result: within the implemented architecture subset and the frozen resource caps, no route yields a complete \(k=13\) campaign. LRC(13) remains open; the program is archived without a terminal theorem, and every obstruction is scoped to a representation, encoding, or implementation rather than proved universal.

Lonely Runner Conjecture hỏi rằng với mọi bộ vận tốc nguyên dương khác nhau \(V_1,\dots,V_k\), có một thời điểm đặt mọi người chạy cách gốc ít nhất \(1/(k+1)\) vòng. Các công trình computer-assisted đã giải đến \(k\le 12\); HIVE-LRC nhắm \(k=13\), trường hợp mở đầu tiên. Dưới một giao thức do con người điều phối và gắn với verifier (Human Intelligence and Verifiable Exploration), các gate D20–D34 khảo sát một họ kiến trúc prime-product, coupling, symbolic và search. Chúng tôi báo cáo bốn định lý được chứng minh nội bộ và một thuật toán exact được chứng nhận trong bao, cùng một kết quả negative-capability có phạm vi: trong tập kiến trúc đã triển khai và các cap tài nguyên đóng băng, không hướng nào tạo được campaign \(k=13\) hoàn chỉnh. LRC(13) vẫn mở; chương trình được lưu trữ không kèm định lý terminal, và mọi obstruction chỉ có phạm vi trong một representation, encoding hoặc implementation, không phải phổ quát.

HIVE-LRC did not solve LRC(13), did not find a counterexample, and did not prove that no future method can work. The program was archived because no remaining route had both direct campaign leverage and a sharp, inexpensive, falsifiable first gate.

Plain-language summary

The Lonely Runner Conjecture asks whether, for every set of distinct positive integer speeds \(V_1,\dots,V_k\), there is a time \(t\) at which every runner is far from the origin:

\[ \lVert tV_i\rVert \ge \frac{1}{k+1}\quad\text{for all }i. \]

Recent computer-assisted work establishes the conjecture through \(k=12\). HIVE-LRC targeted \(k=13\), the fourteen-runner case, which remains the first unresolved case. HIVE stands for Human Intelligence and Verifiable Exploration: the Owner sets the mission and accepts accountability, a Contractor designs gates and formalizes and reviews claims, and a Builder implements only authorized work with tests and certificates. No single agent proposes, implements, verifies, and approves the same claim.

Five retained results

Theorem · proved-internal
C0 – local-content reduction.

At each odd prime the sign- and permutation-invariant local content is carried equivalently by the folded cover, the squared multiset, the split polynomial, and the full coefficient vector \((e_1,\dots,e_{13})\). It removes unnecessary labels and signs but does not by itself guarantee a bounded global integer lift.

Theorem · proved-internal
Q13 – cross-prime coupling.

The top coefficient satisfies \(e_{13}(V^2)=\left(\prod_i V_i\right)^2\), a bounded perfect square. Requiring its reconstructed residue to admit a bounded square root excludes local states before full reconstruction. On three complete finite domains it excluded 56/90, 178/240, and 335/432 states – figures specific to those domains, not universal rates.

Exact algorithm · certified-in-envelope
Certified Q13 evaluator.

An exact evaluator with three paths (enumeration, meet-in-the-middle, q-scan) under a deterministic preflight dispatcher. It returns only WITNESS, EMPTY-CERTIFIED, OPEN-INCOMPLETE, or INVALID-INPUT; a timeout, memory cap, or heuristic miss is never converted to an emptiness claim.

Theorem · proved-internal
Top-residue coset theorem.

Unit scaling gives \(e_{13}(cV)=c^{26}e_{13}(V)\), so the nonzero top residues form a union of \(26\)th-power cosets; away from the exceptional class a nonempty set is already the full quadratic-residue subgroup. This is why using fewer, larger primes does not shrink the problem.

Theorem · proved-internal
Local symbolic separability.

Independent prime-local relations admit a decision diagram whose size is additive in the number of blocks (one pilot: semantic states grew 15 → 71,280 while the diagram grew only 4 → 8 nodes, with zero Cartesian materialization). Adding Q13 breaks separability: the final diagram can stay small, but its construction must process a large coupled object – the wall moves from storage to preprocessing.

D20–D34 route timeline

Gate	Route	Status
D20	Simultaneous prime-product lift	BLOCKED
D21	Signature-narrowed seed generation	BLOCKED
D22	Implicit global-signature elimination	PARTIAL
D23	Early global realizability cuts	PASS (mechanism)
D24	Residue-stratified early cuts	PARTIAL
D25	Adaptive rational-time separation	PARTIAL
D26	Labeled-root direct CRT	PARTIAL
D27	Orbit-compressed unlabeled CRT	BLOCKED
D28	Certified bulge bridge	BLOCKED-BEFORE-BUILD
D29	Pre-reconstruction cross-prime coupling (Q13)	PARTIAL
D30	Certified bounded modular square root	PARTIAL
D31	Prime economy · residue coset theorem	PARTIAL
D32	Implicit realizability · symbolic CEGAR	PARTIAL
D33	Terminal architecture audit	PARTIAL-CLOSURE
D34	Open route triage · disposition	ARCHIVE

Scoped negative-capability statement

Within the subset of the D20–D34 architecture family that was actually implemented, under the frozen resource caps (30 minutes per exact query, 18 hours per pilot, 6 GiB RAM per process, 48 GiB disk, at most \(2^{42}\) explicit states), no route produced a complete, cap-fitting \(k=13\) campaign. Every obstruction remains specific to a representation, encoding, variable order, cut language, proof format, or implementation. This is a scoped result, not a universal lower bound, and not a proof of impossibility.

Open routes and reopen triggers

Two routes were never implemented and remain open, not refuted: algebraic / resultant elimination (a compact emptiness certificate is not indicated but the degree, coefficient-height, and proof-size explosion is plausible-not-certified), and exact lattice / CVP (standard univariate Coppersmith is subsumed by q-scan in the no-wrap regime, but multi-dimensional exact CVP, bounded-distance decoding, and proof-producing enumeration remain open). The program reopens only when a proposal supplies at least one of:

a stronger cross-prime predicate that prunes before the Q13 onset;
an exact, EMPTY-certifying evaluator in \(B_{13} < M < B_{13}^2\);
a certified non-Cartesian symbolic-compiler construction bound;
a bounded algebraic elimination formulation with degree, height, and proof-size bounds;
an exact lattice / CVP method for roots larger than \(M^{1/2}\);
a decisive resolution of one D33 closing theorem.

Final status

LRC(13):          OPEN
Active campaign:  ARCHIVED
Archive class:    ARCHIVE-WITHOUT-TERMINAL-THEOREM
Evidence ceiling: I2
BASE-SURVIVOR:    NONE
GLOBAL-WITNESS:   NONE

The largest value of the program is not a victory claim but a verifiable record that distinguishes what was proved, what holds only on finite domains, what was measured, what is blocked in one implementation, and what remains open – a clean map for the next attempt.

HIVE-LRC không giải được LRC(13), không tìm thấy phản ví dụ và không chứng minh rằng không còn phương pháp nào có thể thành công. Chương trình được lưu trữ vì không còn một bước thử tiếp theo vừa đủ sắc, vừa đủ rẻ và có khả năng bác bỏ rõ ràng để biện minh cho việc tiếp tục.

Tóm tắt phổ thông

Lonely Runner Conjecture hỏi rằng với mọi bộ \(k\) vận tốc nguyên dương khác nhau \(V_1,\dots,V_k\), có tồn tại thời điểm \(t\) sao cho mọi người chạy đều ở xa gốc:

\[ \lVert tV_i\rVert \ge \frac{1}{k+1}\quad\text{với mọi }i. \]

Các công trình computer-assisted mới nhất đã đưa kết quả đến \(k\le 12\). HIVE-LRC nhắm vào \(k=13\) (14 người chạy), hiện vẫn là trường hợp mở đầu tiên. HIVE là Human Intelligence and Verifiable Exploration: Owner đặt câu hỏi và chịu trách nhiệm, Contractor thiết kế gate và formalize/phản biện claim, Builder chỉ triển khai nhiệm vụ đã cấp phép cùng test và certificate. Không agent nào được tự đề xuất, tự code, tự kiểm và tự tuyên bố cùng một claim.

Năm kết quả được giữ lại

Định lý · proved-internal
C0 – thu gọn nội dung địa phương.

Ở mỗi prime lẻ, thông tin bất biến dưới đổi dấu và hoán vị được biểu diễn tương đương bằng folded cover, squared multiset, split polynomial và vector hệ số đầy đủ \((e_1,\dots,e_{13})\). Nó bỏ nhãn và dấu không cần thiết nhưng không tự bảo đảm có nghiệm nguyên toàn cục bị chặn.

Định lý · proved-internal
Q13 – coupling xuyên prime.

Hệ số cao nhất thỏa \(e_{13}(V^2)=\left(\prod_i V_i\right)^2\), một bình phương bị chặn. Yêu cầu residue tái dựng của nó nhận một căn bậc hai bị chặn giúp loại trạng thái trước khi tái dựng đầy đủ. Trên ba miền đầy đủ, Q13 loại 56/90, 178/240, 335/432 trạng thái – chỉ đúng trong các miền đã khai, không phải tỷ lệ phổ quát.

Thuật toán exact · certified-in-envelope
Bộ đánh giá exact cho Q13.

Ba đường exact (liệt kê, meet-in-the-middle, q-scan) dưới một dispatcher preflight xác định. Chỉ trả WITNESS, EMPTY-CERTIFIED, OPEN-INCOMPLETE, INVALID-INPUT; timeout, hết RAM hay heuristic miss không bao giờ bị đổi thành kết luận “không có nghiệm”.

Định lý · proved-internal
Định lý coset residue.

Vì \(e_{13}(cV)=c^{26}e_{13}(V)\), các residue khác zero là hợp của các coset lũy thừa bậc 26; ngoài lớp ngoại lệ, chỉ cần tập khác rỗng là đã dày bằng toàn bộ nhóm quadratic residues. Đây là lý do “dùng ít prime lớn hơn” không tự làm bài toán nhỏ đi.

Định lý · proved-internal
Nén symbolic phần địa phương.

Quan hệ độc lập theo prime có decision diagram kích thước cộng theo số block (một pilot: trạng thái ngữ nghĩa tăng 15 → 71.280 trong khi diagram chỉ 4 → 8 node, không materialize Cartesian). Thêm Q13 làm mất tính tách; diagram cuối có thể nhỏ nhưng quá trình xây phải xử lý một đối tượng coupling lớn – bức tường chuyển từ lưu trữ sang preprocessing.

Dòng thời gian D20–D34

Gate	Hướng	Trạng thái
D20	Simultaneous prime-product lift	BLOCKED
D21	Seed generation thu hẹp theo signature	BLOCKED
D22	Implicit global-signature elimination	PARTIAL
D23	Early global realizability cuts	PASS (cơ chế)
D24	Residue-stratified early cuts	PARTIAL
D25	Adaptive rational-time separation	PARTIAL
D26	Labeled-root direct CRT	PARTIAL
D27	Orbit-compressed unlabeled CRT	BLOCKED
D28	Certified bulge bridge	BLOCKED-BEFORE-BUILD
D29	Coupling xuyên prime trước tái dựng (Q13)	PARTIAL
D30	Căn bậc hai modular bị chặn chứng nhận	PARTIAL
D31	Kinh tế prime · định lý coset	PARTIAL
D32	Khả-thực-hiện ngầm · symbolic CEGAR	PARTIAL
D33	Kiểm toán kiến trúc terminal	PARTIAL-CLOSURE
D34	Triage route mở · quyết định	ARCHIVE

Phát biểu negative-capability có phạm vi

Trong phần kiến trúc D20–D34 thực sự đã triển khai, dưới các cap tài nguyên đóng băng (30 phút mỗi truy vấn exact, 18 giờ mỗi pilot, 6 GiB RAM mỗi tiến trình, 48 GiB disk, tối đa \(2^{42}\) trạng thái explicit), không hướng nào tạo được campaign \(k=13\) hoàn chỉnh nằm trong giới hạn. Mỗi obstruction chỉ đúng trong một representation, encoding, variable order, cut language, proof format hoặc implementation. Đây là kết quả có phạm vi, không phải lower bound phổ quát và không phải chứng minh bất khả thi.

Những hướng vẫn mở và điều kiện tái khởi động

Hai hướng chưa từng được triển khai và vẫn mở, chưa bị bác bỏ: đại số / resultant (chưa thấy chứng chỉ EMPTY gọn, nhưng bùng nổ degree/height/proof-size mới ở mức plausible-chưa-certified) và lattice / exact CVP (Coppersmith một biến bị q-scan bao phủ trong vùng no-wrap, nhưng CVP nhiều chiều, bounded-distance decoding và proof-producing enumeration vẫn mở). Dự án chỉ mở lại khi xuất hiện một trong:

predicate xuyên prime mới cắt được trước Q13 onset;
evaluator exact có EMPTY certificate trong \(B_{13} < M < B_{13}^2\);
symbolic compiler có construction bound không Cartesian;
elimination formulation có degree, height, proof-size bound cụ thể;
lattice / CVP exact xử lý được nghiệm lớn hơn \(M^{1/2}\);
một định lý mở của D33 được giải quyết dứt khoát.

Trạng thái cuối

LRC(13):          OPEN
Active campaign:  ARCHIVED
Archive class:    ARCHIVE-WITHOUT-TERMINAL-THEOREM
Evidence ceiling: I2
BASE-SURVIVOR:    NONE
GLOBAL-WITNESS:   NONE

Giá trị lớn nhất của chương trình không phải một tuyên bố chiến thắng mà là khả năng dừng đúng lúc, không nâng mức claim, và để lại một bản đồ đủ sạch cho lần nghiên cứu tiếp theo.

Verifiable Human–AI Exploration of the Lonely Runner Conjecture at k = 13