Claims & evidence
Public claim ledger
Every statement carries an exact status, evidence class and scope. Proved, validated-by-computation and provisional are kept distinct, superseded claims are retained and linked to their successor.
C-D18G-COHERENCE-CUTValidated (bounded)
Coherence of the fifth-order mass separates the tight coherent family from the incoherent residual branch on bounded validation
The invariant that works measures whether the mass adds up or cancels, isolating the already-handled tight family.
C-D21-PILOTValidated (bounded)
Hard-prime pilot VALIDATED-BOUNDED: on the D20-hard primes up to 2267 every narrowed query terminates under 0.35s with a replayable certificate, and the mandatory padding-required case and timeout injection behave correctly (timeout to OPEN). This is measured bounded evidence that the per-query wall is removed, not a campaign conclusion
On a bounded pilot of the hardest primes, the new fast query works and stays honest about timeouts.
C-D22-PILOTValidated (bounded)
D22 certified pilot VALIDATED-BOUNDED: all mandatory cases run (p=197 cover matches; e1=0 stratum; repeated roots; inapplicable branch; padding-required 13-multiset; four D20-hard primes terminate; a candidate failing square-splitting yields RECONSTRUCTION-FALSE-POSITIVE; timeout injection yields OPEN). Two verifiers ACCEPT, 179 of 179 corruption rejected
On a bounded pilot the implicit engine behaves correctly on every required case and stays honest about timeouts.
C-D23-PRUNINGValidated (bounded)
Pre-2H pruning VALIDATED-BOUNDED (pilot measurements): on the certified pilot, Branch A cut 5000 of 5000 random candidate coefficient vectors and Branch B cut 7 of 7 realistic base covers at level 14, both BEFORE the 2H threshold where D22 had none. These are bounded pilot measurements, NOT a claim that every reachable state is cut
On a bounded pilot the early cuts removed every sampled candidate and every sampled cover before reconstruction; this is measured evidence on a sample, not a statement about all states.
C-D24-PRUNINGValidated (bounded)
Reachable-state pruning 55.3% VALIDATED-BOUNDED: on the actual reachable mod-84 distribution (not random candidates), the fixed refinement test-time cuts at levels 14, 28 and 42 cut 55.3% of states and the mandatory p=197 witness is cut at level 14. These fixed-level cuts are genuinely effective but give only a CONSTANT-factor reduction; the residual scale for the current architecture (about 2^83) is a size indicator, NOT a proof that every exact representation must materialize that many states
The fixed level cuts really do remove more than half the reachable states, but only by a constant factor, so the search is still too big for the current setup; that size is an indicator, not a hard floor.
C-D25-COMPOUNDINGValidated (bounded)
D25 clause compounding VALIDATED-BOUNDED (pilot measurements): the rational-time clauses COMPOUND on reachable branches. Measured on the pilot: about 32 greedy rational times reduced a 4000-branch reachable sample to a handful, at about 0.95 per-clause survival. From that rate, roughly 555 clauses would project to bring the 2^84 reachable residue space below the 2^42 caps. That ~555 figure is an EXPLORATORY PROJECTION, NOT a certified bound: it does not yet account for the new residue variables each new denominator introduces, correlations between clauses, the SAT / decision-diagram size, the proof-certificate cost, or keeping one common tuple across all moduli. So the compounding is a genuine qualitative gain over D24, but the campaign-size claim is unproven
Adding many separate clocks clearly multiplies the pruning, and a rough count suggests a few hundred could shrink the search below the limits. That count is an exploratory estimate, not a proof, since it ignores several real costs.
C0Open
LRC(13) holds
The Lonely Runner Conjecture for 13 nonzero speeds is the target. It is not solved, the project builds verifiable infrastructure and narrows the obstruction.
C-D19-LIFTOpen
The only remaining route is the prime-product lift, a real counterexample must cover simultaneously across enough primes to exceed B13 = 7^156 * 13^143, remains OPEN
Single-prime covers are killed only by requiring one cover to hold across many primes at once, that lift is the open problem.
C-D20-PRIME-PRODUCT-LIFTOpen
Simultaneous prime-product lift OPEN: rule out one common bounded 13-speed multiset inducing compatible local covers across a certified prime family whose product exceeds B13. The full machinery was built (reduction replay, applicability, QR normalization, CRT reconstruction, projective atlas, 3-valued oracle, complete generator) but the D20 enumerate-first campaign is BLOCKED at scale (cost); D21 reopens it via signature-narrowing
Whether one single global speed set can pass the cover test at many primes at once. The direct-enumeration route hit a cost wall; the narrowed route is the current attempt.
C-D21-CAMPAIGNOpen
Full signature-narrowed campaign feasibility OPEN: per-query narrowing is validated, but seeding the first prime's signature set still reduces to D20 enumeration unless a meet-in-the-middle seed generator supplies it; no campaign verdict is claimed until that is built and its cost measured
The per-prime check is fast now; whether the whole 294-prime campaign is affordable is the next open measurement.
C-D23-CAMPAIGNOpen
Full compatible-state campaign OPEN: whether the sound, materially-effective early cuts drive the surviving-state count (realizable AND base-improper at all primes AND improper at levels 14/28/42) low enough to certify emptiness within the frozen caps is not yet measured. D23-PASS establishes an effective pruning mechanism, not a campaign result
The early cuts prune strongly, but whether that is enough to check the whole search within the limits is the next open measurement.
C-D24-CLOSUREOpen
Full compatible-state closure OPEN: whether the reachable-state campaign closes within the frozen caps is not reached. The fixed-level cuts prune materially but only by a constant factor, so certified OPEN branches remain. A super-constant-in-modulus separation is needed
Closing the whole search within the limits is still open; the fixed cuts are not enough, something that scales with the modulus is needed.
C-D25-CLOSUREOpen
Full within-caps closure OPEN: the projection is favorable but not certified. The greedy hitting set left a few survivors on the sample (the finite denominator pool does not cut every branch; the rest need a larger pool or the D23 arithmetic cuts), and the multi-modulus master's SAT / decision-diagram cost at full clause count is not yet measured within caps. D25-PARTIAL: the direction is validated, full closure is not proven
The math points the right way, but closing the whole search within the limits is still open: some states survive and the cost of all the clauses together is unmeasured.
C-D26-LABELED-ROOTOpen
D26 labeled-root CRT campaign OPEN: instead of waiting to reconstruct all squared-speed coefficients past the 2H threshold (about B13 squared), maintain one correct GLOBAL labeling of the 13 speeds and CRT each V_i directly at a threshold based on B13, which is much lower. Labels, signs, permutation and scale are GLOBAL objects fixed ONCE at the tuple level, never re-canonicalized per prime or per denominator. D26 must prove the canonical labeled tuple, pin the exact direct-CRT threshold, build a label-preserving local oracle, use a prime-power factorized master, integrate the rational-time cuts, and measure the net state complexity exactly including the new variables; a full campaign runs only if the reachable state tree provably fits the caps
The D26 route keeps one fixed global labeling of the 13 speeds and reconstructs each speed directly by CRT at a lower threshold, instead of reconstructing the symmetric coefficients at the high threshold. Labels, signs and scale are fixed once at the tuple level, not per prime.
C2Validated (exact)
k=9 reproduced locally, identical to upstream
The k=9 case was recomputed locally and matched the upstream result digit for digit, the highest independently reproduced result.
C-D16-SUPPORT3-COMPLETEValidated (exact)
Support-3 closes on the full universe of all (p-1)^2 triples: tail < 11/1000 (max 0.010377 at p=353)
Scanning every triple at every one of the 109 primes shows the worst tail is 0.010377 at p=353, correcting both earlier constants (9/1000, 1/100).
C-D19-COVER-WITNESSValidated (exact)
Explicit 13-cover witnesses exist, an exact non-tight improper vector at p=197 (13 distinct speeds, zero lonely times, B5=0) refutes per-prime cyclic-cover infeasibility
Thirteen shifts of the bad set really can cover the whole group at individual primes, so single-prime separation cannot work.
C-D23-P197-CUTValidated (exact)
p=197 level-14 early cut VERIFIED: the D19 witness base-covers (0 lonely times at the base level) yet is proper at level 14 (280 lonely times, first at t=1/14), so the Branch B early cut FIRES at level 14 before any CRT reconstruction. Exact, reproduced by two verifiers
The exact test case: the p=197 cover is thrown out at the level-14 grid, exactly as required, long before the full tuple would be reconstructed.
C-D12-DEFICIT-IDENTITYProved (internal)
Exact dual-deficit identity for the non-tight margin
The gap between a candidate and a proper configuration is written as an exact sum over pairs and triples, turning a hard estimate into bookkeeping.
C-D14-PURITY-LEMMAProved (internal)
Connected cumulant = primitive relation signal + exact puncture correction
Each correlation splits exactly into a genuine structural relation plus a deterministic finite-field term, decomposable patterns cancel.
C-D15-ORBIT-IDENTITYProved (internal)
Exact projective orbit-mass identity, direction height = primitive relation height
Repeated scalar copies of a relation are compressed into one projective direction, measured by a canonical height and an exact orbit mass.
C-D16-MODULAR-RANKProved (internal)
Relation rank is over F_p: dim ker = 13 - rank_Fp >= 1 (u is a kernel witness)
Because relations hold modulo p, structural dimension must be counted modulo p, a load-bearing correction that withdrew the earlier rational-rank inference.
C-D18-DEGREE5-NECESSARYProved (internal)
A real proper vector at p=197 has best degree-4 bound 0 while degree 5 recovers 5/98, so degree 5 is the minimal information level
An honest counterexample shows a fourth-order certificate can never work, and the fifth order is exactly what is needed.
C-D18I-DUAL-46Proved (internal)
The degree-5 dual polyhedron has exactly 46 rational vertices, enumerated exhaustively, each a valid degree-5 minorant
The family of best-possible fifth-order certificates is a finite list of 46 exact members.
C-D18I-PRIMAL-DUALProved (internal)
The adaptive bound B5 = max over the 46 vertices equals the minimum p0 among distributions matching S0..S5, verified on both witnesses (5/98 and 487/3528)
The best adaptive certificate exactly equals the smallest loneliness probability consistent with the first six moments.
C-D18J-UNCOVERED-CONEProved (internal)
The region not certified by any adaptive dual vertex is exactly the p0=0 truncated moment cone (distributions on {1..13})
The uncovered set is exactly the profiles admitting a zero-loneliness companion distribution.
C-D19-PER-PRIME-INSUFFICIENTProved (internal)
Both per-prime methods, the adaptive degree-5 moment dual and cyclic-cover infeasibility, are refuted by the same explicit witnesses; single-prime covers exist and have B5=0
Neither moment nor cover methods at a single prime can settle the conjecture, since counterexample-shaped covers exist at each prime.
C-D20-BASE-NECESSARYProved (internal)
O-A: a global counterexample induces a base-level cover at every prime (necessary), but a base cover is NOT sufficient: the exact p=197 witness covers at base level yet is proper at refinement level 14. So the base-cover compatibility search is a sound one-way filter; every survivor must pass the refinement tower
A single-prime cover is a required clue for a counterexample, but not proof of one; finer time grids can break it.
C-D21-PADDINGProved (internal)
Padding decomposition: every 13-multiset cover = minimal core + padding; padding changes multiplicity, symmetric coefficients, projective orbit and CRT compatibility, so a minimal-core-only oracle is incomplete and the full 13-multiset must be queried (brute-verified p=23: 66=66)
A full 13-speed cover is a small core plus filler, and the filler matters: it shifts the fingerprint the compatibility test relies on.
C-D21-NARROWEDProved (internal)
Signature-narrowed oracle: fixing a target signature pins the squared-speed multiset up to the quadratic-residue scale action, so all matching covers are found by scanning the scale half-group in cost linear in p. Measured to terminate under 0.35s on D20-hard primes up to 2267 where full enumeration was blocked; 3-valued with replayable certificates, UNSAT-without-proof rejected, timeout OPEN. Removes the D20 per-query wall
Instead of listing every cover then filtering, D21 uses the target fingerprint to look only where a match could be, fast even at the hard primes.
C-D21-SEEDProved (internal)
Seed completeness THEOREM proved: every bounded global counterexample enters at least one retained seed. At each seed prime it is either applicable, retaining its full 13-multiset signature under complete enumeration, or inapplicable, recording that the prime divides the global speed product against FA-OB. Completeness carries padding, the QR scale orbit, permutation and sign removal by squaring, duplicate-root multiplicity and every projective singular stratum. This is unconditional on the enumeration being affordable
It is proved that a real counterexample can never slip past the seeding step: every one leaves a fingerprint that a complete scan would keep.
C-D22-IMPLICIT-STATEProved (internal)
D22 implicit CEGAR architecture PROVED-SOUND: keeping the bounded global object symbolic (coefficient master E_j and root master X_i), projecting to each prime, asking the narrowed local subproblem (MATCH-WITNESS / EMPTY-CERTIFIED / OPEN-INCOMPLETE) and generating proof-carrying cuts is sound by the one-way theorem: a bounded counterexample survives every certified cut (its base cover matches at every prime, so an empty-certified cut can never contain it; applicability and square-splitting cuts also exclude it). No certified cut ever removes a counterexample
The symbolic-and-cut architecture is proved safe: no proof-carrying cut can ever throw away a real counterexample.
C-D23-EARLY-CUTSProved (internal)
D23 early-cut SOUNDNESS proved: every early cut (arithmetic realizability or refinement impropriety) is a NECESSARY condition for a bounded counterexample, so their combination discards no counterexample. Applied BEFORE the 2H reconstruction threshold, correcting D22 where the only global check waited until reconstruction
Every early cut is proved safe: it only removes objects that a real counterexample could never be.
C-D23-ARITHMETICProved (internal)
Branch A arithmetic realizability cuts PROVED-INTERNAL: exact positivity, per-degree coefficient bounds, Newton and Maclaurin inequalities, Newton-identity power-sum positivity, an auxiliary-modulus square-splitting sieve, and primitivity/multiplicity. Each is a proved necessary condition for E_j = e_j of 13 bounded integer squares; a genuine square-multiset passes all families
Classical inequalities among symmetric functions certify, before reconstruction, that a candidate cannot come from 13 integer squares.
C-D23-REFINEMENTProved (internal)
Branch B refinement cuts 14/28/42 PROVED-INTERNAL: by O-A a counterexample is improper on every refinement grid, so a state proper at level 14, 28 or 42 is soundly cut without integer reconstruction. The cheap mechanism: t=1/14 is a lonely time iff 14 divides no speed, carried as a small-modulus residue mod (14,28,42)
A state can be thrown out simply because it already has a lonely runner on the finer level-14 grid, no reconstruction needed.
C-D24-REACHABLEProved (internal)
D24 global mod-84 semantics PROVED-INTERNAL: represent reachable states as one common residue multiset modulo 84 = lcm(14,28,42), a single global clock never re-chosen per prime. The frozen exact cut: t=1/14 is a lonely time iff 14 divides no speed, so a bounded counterexample must have at least one V_i divisible by 14 (verified firing on the p=197 witness); the analogous test-time conditions at levels 28 and 42 are exact, not over-generalized to full level-l impropriety
One shared clock modulo 84 with an exact rule: any counterexample must have a runner whose speed is a multiple of 14, or the time 1/14 would be lonely.
C-D24-COUPLINGProved (internal)
D24 refined CRT coupling PROVED-INTERNAL: for each applicable prime p (coprime to 84, p>7), V_i mod 84 and V_i mod p combine by CRT into V_i mod 84p, and the refined local subproblem certifies impropriety on the nested grids {j/(l p)} returning REFINED-MATCH / REFINED-EMPTY-CERTIFIED / OPEN-INCOMPLETE with a replayable proof
The global clock and each prime are combined exactly, so the finer-grid check runs against one consistent picture.
C-D25-ADAPTIVEProved (internal)
D25 rational-time cut PROVED-INTERNAL: for a reduced time a/q, B(a,q) = { r mod q : min(a r mod q, q - a r mod q) < q/14 } (strict; the boundary is a lonely, not a bad, residue; integer-exact after clearing 14). A global counterexample is improper, so for every a/q it satisfies OR_i [ V_i mod q in B(a,q) ] (else t=a/q is lonely); the contrapositive cuts any branch lonely at that time. Each cut is a disjunction over ONE small modulus, so moduli stay separate and no giant LCM is materialized. B(1,14)={0} reproduces the D24 t=1/14 cut and the p=197 witness fires
A proved rule: for any rational time, a counterexample must have a runner near the origin, giving an exact clause on the speeds modulo just that time's denominator, no giant shared clock needed.
C-D25-MULTIMODProved (internal)
D25 multi-modulus consistency PROVED-INTERNAL: the active moduli are kept SEPARATE, each carrying V_i mod q, and only cross-modulus compatibility is enforced (V_i mod gcd(q1,q2) must agree), so the state represents ONE common speed tuple without ever materializing the least common multiple of the denominators
Every clock stays a separate small modulus, tied together only by their common factors, so the speeds stay one shared tuple and the search never collapses into a single giant modulus.
C-D26-DIRECT-CRTProved (internal)
D26 direct-CRT theorems PROVED and double-verified: a unique canonical labeled tuple exists (sort ascending breaking S_13 once, positive representative, primitive, duplicates kept) with sign, permutation and scale fixed ONCE globally; and each labeled coordinate V_i below B13 is pinned by direct CRT once the modulus product exceeds 2*B13 = 969 bits, versus the squared-coefficient threshold 2H = 1946 bits. The direct threshold is provably about half, cutting the certified prime product from about 205 to about 109 primes. Back-conversion re-symmetrizes to the same e_j(V^2) object the coefficient route uses
Direct coordinate CRT is proved and double-verified: each speed in the canonical labeled tuple is pinned once the modulus product exceeds about 969 bits, against about 1946 bits for the coefficient route, roughly half the certified primes.
C-D4-K13-P191Supported (internal)
Exact k=13 tight orbit count = 16,171
The tight configurations for 13 speeds collapse under symmetry to exactly 16,171 orbit classes, computed exactly, not extrapolated.
C-D5-UNIFORMSupported (internal)
Uniform prime transfer: tight closure at p=191 extends to all p>182
A single lattice-point argument covers every prime above 182 at once, so no per-prime campaign is needed on the tight side.
C-D13-SUPPORT3-INVERSE-SCOPEDSupported (internal)
Large connected triple correlation implies a bounded-height support-3 relation (profile at p=191)
A big three-way correlation is always backed by a short exact relation, measured at p=191, later made complete in D16.
C-D16-SUPPORT4-FRAMEWORKSupported (internal)
Primitive support-4 orbit identity + lattice + connected 4th cumulant, tau4 < 8/1000 at four primes, inventory + support-5 OPEN
The projective method extends to four-coordinate relations, exact at four small primes, full closure and support-5 remain open.
C-D20-BLOCKEDSupported (internal)
D20-BLOCKED (measured, not assumed): complete local-cover enumeration does not terminate within the resource caps for the inventory primes, so every campaign block is OPEN and the certified-closed product is zero. Honest cost-driven negative capability, like the D6 non-tight campaign; NOT a compatibility claim, NOT a counterexample
The direct route is blocked by computation cost, not by mathematics: nothing was proved or disproved about LRC(13).
C-D21-SEED-BLOCKEDSupported (internal)
Seed MATERIALIZATION BLOCKED-COMPUTE (measured): the two built routes that materialize the seed set both exceed the frozen caps. Distinct 13-multiset signatures grow 6 (p=23) -> 15511 (p=29); the Cartesian small-prime seed set is the CRT product to pass the threshold, at least 2^519; the meet-in-the-middle half-space is 1e9..1e17 at inventory primes. SCOPE (Contractor): this blocks the two explicit materialization methods, NOT every implicit approach. The product of local signature sets is not the mandatory state space, cross-prime constraints may eliminate most states before they are generated. Not a compatibility claim, not a counterexample
The two ways we tried to list every starting fingerprint are astronomically large, so those routes are cost-blocked. That does not mean every method is blocked, keeping the object symbolic may prune most states before they exist.
C-D22-CRT-NO-PRUNINGSupported (internal)
Cross-prime CRT compatibility ALONE prunes NOTHING (measured): distinct primes give independent moduli, so every pair of local signatures is CRT-consistent and the compatible set is the full product prod|Sigma_p|. If the only global check is deferred to the reconstruction threshold 2H, the implicit master grows as prod|Sigma_p| (>= 2^519) before any cut fires, the same wall as D21-S
Just matching fingerprints prime by prime removes nothing; a real global check has to come in earlier than the reconstruction step, or the count explodes again.
C-D26-NET-NEGATIVESupported (internal)
D26-PARTIAL (measured net-complexity): the exact ledger is decisive and negative. Maintaining one global labeling forces up to 13! (about 6.2 billion) label assignments per accumulation prime, roughly 2^3546 labeling entropy across the about 109-prime accumulation, far above both the 977-bit threshold saving and the 2^42 compute cap. CRT-consistency forces the labeling only after a coordinate pins, which needs the full accumulation. By the gate rule, a denominator that adds more unconstrained state than it removes is not progress, so the labeled campaign does NOT net-fit the caps. 723 of 723 corruption rejected. The reconstruction theorems stand; the campaign-fit closes negative. No BASE-SURVIVOR, no GLOBAL-WITNESS
The labeling cost dominates: each local cover is an unordered multiset, and assigning it to the 13 global labels gives a worst-case branching proxy near (13!)^109, beyond the frozen caps. The lower threshold does not offset this, so the fully labeled campaign does not close. LRC(13) remains OPEN.
C1External claim
LRC holds for k<=12 (upstream)
Known upstream results establish the conjecture up to 12 speeds, the project audits and reuses them.
C-D14-SUPPORT3-TAILSuperseded
Support-3 tail small, audited at three primes (bound 9/1000)
An early three-prime estimate suggested the support-3 tail is under 9/1000, later shown too small once the full universe was scanned.
C-D15-SUPPORT3-INVENTORYSuperseded
Support-3 tail < 1/100 over 109 primes (extremal family, max 0.009475 at p=281)
A broader 109-prime estimate over an extremal family gave 1/100, still incomplete, the full universe reaches 0.010377.
D-D18I-10-VERTEX-COVERSuperseded
Withdrawn as a global guide: the sampled minimum B5 = 3/98 over ~20000 vectors only reflected that covers are rare, not impossible; the exact p=197 witness reaches B5 = 0
A handful of certificates covered every sampled case, but that was a sampling artifact, not a proof, and an exact witness breaks it.
C-D18G-RANK-CUTRefuted
Bounded-height modular rank as the support-5 structural cut is refuted, rank saturates to full for every vector
Using relation rank to detect structure does not work, every vector already reaches full rank.
C-D18G-EXISTENCE-CUTRefuted
Bounded-height relation existence as the cut is refuted, every five-subset carries a short support-5 relation
Detecting structure by whether a short relation exists fails, short relations are everywhere.
C-D18G-MAGNITUDE-CUTRefuted
Per-direction magnitude concentration as the cut is refuted, the adverse fifth-order mass is diffuse
Peeling off the few largest directions does not separate structure, the mass is spread out.
C-D18H-FIXED-M5-CLOSURERefuted
The fixed signed degree-5 margin M5 is REFUTED, a real proper non-tight vector at p=197 has M5 = minus 20/49 < 0
A single fixed fifth-order rule cannot certify every case, an honest counterexample drives it negative.
C-D18H-SIGNED-INVERSERefuted
The signed inverse theorem is refuted as posed, the counterexample has large adverse mass yet is non-tight and adaptively certified
Large fifth-order mass does not force a known structured family, so that route also fails as stated.
D-D18H-ADAPTIVE-DEG5Refuted
REFUTED as a per-prime closure: the adaptive degree-5 dual stayed positive on the ~20000-vector sample, but the exact non-tight p=197 witness has adaptive B5 = 0, so it certifies nothing there
The best fifth-order certificate looked to work on every sampled case, but an exact witness drives it to zero, so the per-prime route does not close.
D-D18J-HISTOGRAM-ONLYRefuted
REFUTED as a universal description: the p0=0 cone is not histogram-only, an exact real 13-speed vector at p=197 realizes p0=0 with B5=0
The uncovered cone was thought to hold only abstract histograms, but a real speed vector reaches it, so the separation cannot exist.
C-D18J-VECTOR-SEPARATIONRefuted
REFUTED: real speed-vector moment profiles do NOT separate from the p0=0 cone, an exact p=197 vector realizes it, so no per-prime realizability cut exists
The hoped-for separation of real vectors from the uncovered cone is false, real improper vectors exist at single primes.