Attack log — Caccetta–Häggkvist for directed triangles

2026-08-17 — start

• Folder empty except PROBLEM.md. House: write only here; no git; cite what we beat; no invented dent.
• Conjecture (Caccetta–Häggkvist 1978): every simple n-vertex digraph of minimum out-degree at least r has a directed cycle of length at most ⌈n/r⌉.
• First open case, and tonight's problem: whether δ⁺ ≥ n/3 forces a directed triangle.
• Tonight: a certified small-order obstruction, an improved numerical out-degree threshold with an independently checkable certificate, or a documented residue. Isolated random-graph statistics are not a dent.

Published record (fetched tonight)

AIM workshop summary: Sullivan, A Summary of Results and Problems Related to the Caccetta-Häggkvist Conjecture (14 Apr 2006), local compute/refs/sullivan-aim-caccetta.pdf. Egres page timed out.

HKN (and every later citation that needs a published number, including Grzesik–Volec IMRN 2023 Theorem 2.2) still states 0.3465n as the refereed unrestricted threshold. The 0.3388 figure is on the record as a personal communication only.

The cyclic construction (out-neighbours {1,…,⌊(n−1)/3⌋} on ℤ/n) is C₃-free and meets the conjectured threshold: so the exact finite statement is

every n-vertex oriented graph with δ⁺ ≥ ⌈n/3⌉ has a directed triangle.

HKN implies this whenever ⌈n/3⌉ ≥ 0.3465 n. Combined with Hoàng–Reed (r≤5) the first n where the exact statement is not implied is n=18, δ⁺=6 (0.3465·18 = 6.237). The 0.3388 communication still has 0.3388·18 = 6.098 > 6, so n=18 is open even if one grants that number. Same for n=21,24,27,…

Hamidoune already kills every Cayley counterexample, so a circulant search cannot produce an obstruction.

Plan

1. Fetch HKN, the AIM summary, Grzesik–Volec, Razborov; replay HKN's F₄ certificate independently from the published matrices and from a from-scratch flag count.
2. Re-optimise HKN's linear combination on the same F₄ inequalities; a verified c < 0.3465 is a dent against Combinatorica. Beating 0.3388 would need F₆ or a new inequality and is not assumed.
3. SAT-certify the exact statement at the first open order n=18 (and as far as the solver reaches). A DRAT/UNSAT proof, or a C₃-free 6-outregular oriented graph, is the product. The latter would disprove the conjecture; do not expect it.
4. If neither a better c nor a finished n=18 certificate appears, leave the residue. Do not call a partial search a bound.

Local PDFs and CH.mw: compute/refs/.

2026-08-17 — HKN certificate shape

HKN Theorem 3.3: every homomorphism Ψ of the flag algebra of triangle-free oriented graphs satisfies δα(Ψ) < 0.3465. Proof reduces to emptiness of a set R(c) ⊂ ℝ³² of 4-vertex type densities r = (Ψ(H₀),…,Ψ(H₃₁)) obeying

• r ≥ 0, ‖r‖₁ = 1
• AC(r) ≽ 0 (8×8 Cauchy–Schwarz on β-flags)
• b(BR − c AR)rᵀ ≥ 0 for all b (out-regularity)
• IndT(r) ≥ 0, IndV(r) ≥ 0 (order-3 induction, Shen-style)
• Fork(r) ≥ 0 (CSS + Jensen on forks)

They exhibit four vectors aᵢ ∈ ℝ⁸, one b ∈ ℝ¹⁴, and scalars cT, cV, d such that the linear form F(c,r) is a nonnegative combination of those inequalities, F is nonincreasing in c, and F(0.3465, r) has every coordinate strictly negative (worst −1.24639). Hence R(0.3465)=∅.

The aᵢ are two-decimal; the claimed F coefficients are called “exact”. Independent replay is compute/hkn_replay.py.

2026-08-17 — matrices rebuilt from scratch

flags4.py enumerates all 549 labeled C₃-free oriented graphs on 4 vertices, matches HKN’s 32 types H₀…H₃₁ (pairwise non-isomorphic), and rebuilds AC. Every entry of Table 1 matches exactly, no scale.

AR and BR match Table 2 after dividing the labeled count by 2 (HKN’s extras in a λ-flag are unordered). IndT and Fork match (4.14) and the fork identity exactly (ind_fork.py). IndV is twice (4.15) before the published factor 12 (type V has an extra automorphism). So the linear pieces of the HKN certificate are independently checked.

Plugging the printed two-decimal aᵢ into F does not reproduce (4.22). The display rounding of aᵢ is fatal; (4.22) was computed from higher-precision vectors that are not in the paper (the Maple worksheet stores them as encoded floats). We do not trust (4.22) as a certificate.

2026-08-17 — F₄ threshold of this system

optimize_bound.py (HiGHS LP on the linear multipliers, Q = Σ a aᵀ plus random PSD) and sdp_bound.py (CVXPY/SCS, feasibility Fₖ ≤ −1) agree: the HKN F₄ inequality system becomes empty at

c⋆ ≈ 0.346439.

HKN published 0.3465, a four-decimal rounding. The same system, with an explicit Q ≽ 0 and (b, cT, cV, d), certifies c = 0.34645 with worst coordinate F = −0.12343 (certs/f4_certificate.json). verify_certificate.py replays it against the rebuilt matrices.

This is a fifth-decimal tightening of Combinatorica, not a new method. It does not beat the 0.3388 personal communication. An F₅ lift (317 types, 14×14 λ-flag SOS plus the pulled-back F₄ block) did not improve the threshold (optimize_f5.py).

Linear-only R′(c) (no SOS) is nonempty down through 1/3 + ε and empty only around 0.38 — Bondy/Shen territory. The SOS is doing the work.

2026-08-17 — SAT encoding, two bugs, then a census

First CNF used a broken Sinz cardinality encoding. Kissat returned SAT for n=6, d=2; the model had min out-degree 1 and 2-cycles. Discarded. Replaced by binomial at-least / at-most (no auxiliaries).

verify_model.py reads only v-lines (the first version parsed numbers out of the kissat banner). After the fix:

All SAT models checked: out-regular, no 2-cycle, no C₃.

Without lex SB, n=12 d=4 (Hoàng–Reed) is already too hard: 180s, 1.8M conflicts, UNKNOWN. With lex order on out-neighbourhoods of N⁺(0) and of the complement:

• n=12 d=4: UNSAT, 2993 conflicts, 0.07s. DRAT verified (drat-trim).
• n=15 d=5: UNSAT, 137486 conflicts, 6.0s. DRAT verified.
• n=16 d=6: UNSAT, 35382 conflicts, 3.5s. DRAT verified. (HKN already implies this: 0.3465·16 < 6.)
• n=17 d=6: UNSAT, 654582 conflicts, 63s. DRAT verified. (HKN: 0.3465·17 < 6.)

n=18 d=6 is the first order not implied by Hoàng–Reed or HKN (0.3465·18 = 6.237 > 6; even 0.3388·18 = 6.098 > 6). Kissat still UNKNOWN at 20 min / 10.3M conflicts (certs/n18_residue.json).

Local search from the circulant plus one extra out-edge per vertex never produced a C₃-free (r+1)-regular graph on n≤24 (hunt_plus_one.py). Isolated, as required.

2026-08-17 — what would be a dent vs what we have

• Numerical: 0.34645 < 0.3465, independently checkable F₄ certificate. Tiny. Did not beat 0.3388.
• Small-order: DRAT-verified exact CH-triangle at n=12,15,16 (and n=17 pending proof). n=16 is the first n with ⌈n/3⌉=6. n=18 is the first n where this is not already a theorem. Residue if the n=18 run dies.

2026-08-27 — q1, first open order

Continue the 17 August campaign. Published unrestricted threshold is still HKN Combinatorica 0.3465: fetched arXiv:0908.2791v4 tonight; the abstract and Theorem 1.2 still state 0.3465n. Grzesik–Volec arXiv:2102.12830v2 (updated 2024-01-18) still quotes that number as the published out-degree bound and leaves 0.3388 as a personal communication. Cheng–Keevash arXiv:2402.16776 (2024) cites HKN 0.3465 as the triangle-case input. ProofAtlas's 2 August 2026 check still lists 0.3465 as the peer-reviewed unrestricted threshold. Do not treat 0.3388 as published.

The stored F₄ certificate at c=0.34645 still replays (worst F=−0.12343, min eig 9.5·10⁻⁹). The same (Q,b) ray stays strictly negative through c=0.34644447 (worst F=−0.0225) and goes positive at 0.34644. So this system does not give a clean fifth-decimal step below 0.34645; 0.34645 remains the frozen number. F₅ already failed to move the threshold. Beating 0.34645 needs a new inequality or F₆.

The leftover that counts is the exact statement at n=18, δ⁺=6. Code for this run is compute/q1/. Two changes to the SAT encoding:

1. Sinz sequential counters replace the binomial at-most/at-least. The 17 August CNF was p cnf 819 465269 mostly from C(17,7) per vertex.
2. Split on k=|N⁻(0)| and fix N⁻(0)={7,…,6+k} by relabelling. Each cube is a separate instance. k=11 is empty by counting: each v∈N⁺(0) would need 6 out-neighbours from 5 legal candidates.

A DRAT/UNSAT on every cube, or a verified C₃-free 6-outregular model, is the product. Incomplete SAT is residue.

2026-08-27 — cubes

Sequential-counter encoding recovers the 17 August census. DRAT-verified tonight with the new encoder: n=6 d=2, n=9 d=3, n=12 d=4, n=15 d=5, n=16 d=6, n=17 d=6 (18s; was 63s). Cube split on n=9 d=3 is all UNSAT; on n=9 d=2 some k are SAT with checked models. So the in-neighbourhood cut is not vacuously empty.

n=18 d=6 cubes, kissat 4.0.4:

| k=|N⁻(0)| | status | time | DRAT | | ---: | --- | ---: | --- | | 11 | UNSAT | 0.002s | VERIFIED, 8kB | | 10 | UNSAT | 0.002s | VERIFIED, 12kB | | 9 | UNSAT | 0.004s | VERIFIED, 24kB | | 8 | UNSAT | 0.003s | VERIFIED | | 7 | UNSAT | 0.012s | VERIFIED, 44kB | | 6 | UNSAT | 0.03s | VERIFIED, 39kB | | 5 | UNSAT | 1.1s | VERIFIED, 2.6MB | | 4 | UNSAT | 6s | (proof running) | | 3 | UNSAT | 24s | (proof running) | | 2 | UNSAT | 115s | VERIFIED, then dropped (245MB) | | 1 | UNKNOWN | 180s with proof log | leftover | | 0 | UNKNOWN | 180s with proof log | leftover |

k=0 and k=1 reran without proof logging (600s): k=1 UNSAT in 596s. Regenerated with proof: kissat 587s, DRAT VERIFIED, 1.207 GB (certs/keep/ch-18-6-k1-proof.json, sha256 73441d6e…). The proof is too large to store; replay is python3 solve.py --n 18 --d 6 --indeg0 1 --time 900 --proof. k=0 still UNKNOWN at 600s.

Second split t=|N⁺(1) ∩ U|:

• k=0, t=1..5: UNSAT, DRAT stored and replayed
• k=0, t=6: UNKNOWN at 900s (--stable)
• k=1, t=1..5: UNSAT, DRAT stored and replayed
• k=1, t=6: implied by the whole-k=1 DRAT

Third split of (k=0,t=6) on s=|N⁺(2) ∩ (N⁺(1) ∩ U)| timed out at 180s for s=0,1,2,3. That leftover is unused.

Pigeonhole. A 6-outregular oriented graph on 18 vertices has 108 arcs, so some vertex has in-degree ≥ 6. Relabel that vertex as 0, its out-neighbours as 1..6, its in-neighbours as 7..6+k, and sort each block to meet the lex cut. The exact statement at n=18 therefore reduces to cubes k=6..11.

Those six cubes are UNSAT with stored, replayed DRATs (certs/keep/ch-18-6-k{6..11}.{cnf,drat}). So every 18-vertex oriented graph with δ⁺ ≥ 6 has a directed triangle.

This is a dent against the finite hole, not against HKN 0.3465 (that number already misses n=18). Did not beat 0.34645. Did not treat 0.3388 as published. The k=0 search is leftover bookkeeping, not a bound.

2026-08-27 — q2, next exact holes

Continue from the n=18 pigeonhole. Code is compute/q2/. Published unrestricted threshold is still HKN Combinatorica 0.3465: fetched arXiv:0908.2791v4 tonight (abstract and Theorem 1.2 still 0.3465n; no later version). Grzesik–Volec arXiv:2102.12830v2 still does not replace the unrestricted triangle number. Cheng–Keevash arXiv:2402.16776v4 (21 Aug 2024) quotes HKN 0.3465 as the triangle-case input and proves a path-length statement, not a new c. No arXiv hit after 2024 states a published unrestricted c < 0.3465 with a public certificate. Do not treat 0.3388 as published. The stored F₄ certificate at 0.34645 is not to be moved unless a new inequality appears.

After n=18, the first remaining exact order is n=21, δ⁺=7 (0.3465·21 = 7.2765 > 7; even 0.3388·21 = 7.1148 > 7). Then n=24, and a few near-threshold orders such as n=26 (0.3465·26 = 9.009 > 9). A 7-outregular oriented graph on 21 vertices has 147 arcs, so some in-degree is at least 7. Same encoder as q1: cubes k=|N⁻(0)|. Counting on N⁺(0) empties k=13. The statement reduces to k=7..12.

A DRAT/UNSAT on every needed cube, or a verified C₃-free 7-outregular model, is the product. Incomplete SAT is residue. Isolated random-graph statistics are not a bound.

2026-08-27 — cubes through n=36

Same encoder as q1. High-k cubes first, kissat 4.0.4, DRAT checked against a CNF regenerated from encode.py (not against leftover scratch files).

Soundness: n=21 d=6 k=6 is SAT in 0.15s with a checked C₃-free 6-outregular model. n=24 d=7 k=7 is SAT in 7s, same check. So the encoder is not vacuously UNSAT at these orders.

Every needed cube k≥d at the remaining holes through n=36 is UNSAT. Each proof is tens to a few hundred kilobytes and finishes in well under a second:

Independent replay: python3 verify_keep.py (95 cubes, 0 failures).

So every oriented graph on one of those n with δ⁺ ≥ ⌈n/3⌉ has a directed triangle. This is a dent against those finite holes, not against HKN 0.3465. Did not beat 0.34645. Did not treat 0.3388 as published.

The first remaining hole is n=38, δ⁺=13 (0.3465·38 = 13.167 > 13). Then 39, 41, 42, … . Those were not run.

2026-08-27 — q3, first leftover hole n=38

Continue from the q2 certificates through n=36. Code is compute/q3/. Published unrestricted threshold is still HKN Combinatorica 0.3465: fetched arXiv:0908.2791v4 tonight (abstract and Theorem 1.2 still 0.3465n; no later version). Grzesik–Volec arXiv:2102.12830v2 still does not replace the unrestricted triangle number. Cheng–Keevash arXiv:2402.16776v4 quotes HKN 0.3465 as the triangle-case input. Mezher–Daamouch arXiv:2405.17797 is a restricted-class second-neighbourhood note, not a new unrestricted c. No arXiv hit after 2024 states a published unrestricted c < 0.3465 with a public certificate. Do not treat 0.3388 as published. The stored F₄ certificate at 0.34645 is not to be moved unless a new inequality appears.

After n=36, the first remaining exact order is n=38, δ⁺=13 (0.3465·38 = 13.167 > 13; even 0.3388·38 = 12.8744 < 13, so granting the personal communication would already imply n=38 — we do not grant it). Then 39, 41, 42, 44, 45, … . A 13-outregular oriented graph on 38 vertices has 494 arcs, so some in-degree is at least 13. Same encoder as q1/q2: cubes k=|N⁻(0)|. Counting on N⁺(0) empties k=24. The statement reduces to k=13..23.

Replay q2 first: cd compute/q2 && ./run_all.sh. A DRAT/UNSAT on every needed cube at n=38 (and as many later holes as finish), or a verified C₃-free 13-outregular model, is the product. Incomplete SAT is residue. Isolated random-graph statistics are not a bound. A new F₄/F₆ certificate with some c < 0.34645 would be a numerical dent; the same (Q,b) ray does not give one.

2026-08-27 — cubes through n=72

q2 replay first: F₄ still 0.34645 (worst F=−0.12343); 95 stored pigeonhole DRATs, 0 failures.

Same encoder as q1/q2. High-k cubes first, kissat 4.0.4, DRAT checked against a CNF regenerated from encode.py.

Soundness: n=21 d=6 k=6 is SAT in 0.15s with a checked C₃-free 6-outregular model. The n=38 circulant (d=12) is C₃-free and 12-outregular; after placing N⁺(0) and N⁻(0), every arc-variable clause of both the non-SB and the lex-SB cube is satisfied (certs/keep/soundness_n38_d12.json). Kissat searching for that SAT model timed out at 60s; the explicit circulant is the check. The encoder is not vacuously UNSAT at these orders.

Every needed cube k≥d at the remaining holes through n=72 is UNSAT. Each proof is tens of milliseconds to a couple of seconds:

Independent replay: python3 verify_keep.py (534 cubes). Orders closed tonight: 38, 39, 41, 42, 44, 45, 47, 48, 50–72. The n≡1 (mod 3) values 40, 43, 46, 49 are already implied by HKN 0.3465 and were not cubes.

So every oriented graph on one of those n with δ⁺ ≥ ⌈n/3⌉ has a directed triangle. This is a dent against those finite holes, not against HKN 0.3465. Did not beat 0.34645.

A second F₄ Cauchy–Schwarz block on the order-2 non-edge type was tried (sos_nonedge.py). The old c=0.34645 still certifies (t=−0.77); at c=0.346 the best t is +73. The extra SOS did not move the threshold. F₄ residue, not a numerical dent.

The first remaining hole is n=73, δ⁺=25. The conjecture 1/3 is open. Did not treat 0.3388 as published.

2026-08-27 — q4, first leftover hole n=73

Continue from the q3 certificates through n=72. Code is compute/q4/. Published unrestricted threshold is still HKN Combinatorica 0.3465. Do not treat 0.3388 as published. The stored F₄ certificate at 0.34645 is not to be moved unless a new inequality appears.

After n=72, the first remaining exact order is n=73, δ⁺=25 (0.3465·73 = 25.2945 > 25). A 25-outregular oriented graph on 73 vertices has 1825 arcs, so some in-degree is at least 25. Same encoder as q1/q2/q3: cubes k=|N⁻(0)|. Counting on N⁺(0) empties k=47. The statement reduces to k=25..46.

A DRAT/UNSAT on every needed cube at n=73 (and as many later holes as finish), or a verified C₃-free 25-outregular model, is the product. Incomplete SAT is residue. Isolated random-graph statistics are not a bound. A new F₄/F₆ certificate with some c < 0.34645 would be a numerical dent.

2026-08-27 — why leftover cubes are easy

The k≥d cubes are easy for two different reasons. High k is a count. Each a∈N⁺(0) omits exactly σ=n−2−d−k vertices of (N⁺(0)\{a}) ∪ U. Avoiding 2-cycles in N⁺(0) needs at least C(d,2) A-omissions, so σ≥(d−1)/2. Equality (d odd) forces a C₃-free tournament on A, hence a transitive tournament, whose out-degrees cannot all meet s_a≥d−|U|. Replay: python3 compute/q4/count_obstruction.py --self-test. On n=73 that empties k=34..46. The same count on n=73..120 empties 792 of 1464 needed cubes and leaves at least nine survivors at every order (certs/keep/covering_73_120.json).

The survivors (n=73: k=25..33) are not a linear obstruction: the [0,1] relaxation with exact degree, 2-cycle, and triangle inequalities is feasible on A∪U, and combinatorial unit propagation does not close. They are SAT-easy because of lex SB. With SB, n=73 k=25 is UNSAT in 1.08s / 5244 conflicts (p cnf 379710 901442). Without SB the same cube is UNKNOWN at 20s / 138k conflicts. Preprocess alone (--decisions=0) does not finish the k=d cube. So a short written proof of every leftover n≥73 cube is still missing; the covering count is only the high-k half. Did not write certs/keep/ch-*.drat. Did not treat 0.3388 as published. This note does not move the numerical threshold.

2026-08-27 — independent F₄ dump at c=0.3464

Recomputed the 32 F-coordinates of certs/keep/f4_or_new_certificate.json without importing verify_q4_certificate.py. AC slices from hkn_replay.ac_slices; 4Ψ(κ) rebuilt from flags4.enumerate_labeled and matched HKN (4.7); fork penalty 12(3c−1)²/0.8616. Script: dump_f_coords.py. Output: certs/keep/f_coords_0.3464.json. min eig(Q) = 6.192452827718651e-10; worst F = −0.4190333660408214 at r₃₀; all 32 coordinates < −0.05. Did not start SAT. Did not beat the stored 0.3464 certificate; this is a replay of that file.

2026-08-27 — cubes through n=108

q3 leftover through n=72 still stands. Same encoder as q1/q2/q3. High-k cubes first, kissat 4.0.4, DRAT checked against a CNF regenerated from encode.py. Raw kissat proofs at n≈84+ grow past GitHub’s 100 MB cap; those files were replaced by drat-trim core lemmas that still replay.

Soundness: n=21 d=6 k=6 is SAT in 0.15s with a checked C₃-free 6-outregular model. The n=73 circulant (d=24) is C₃-free and 24-outregular; after placing N⁺(0) and N⁻(0), every arc-variable clause of the cube is satisfied (certs/keep/soundness_n73_d24.json). The encoder is not vacuously UNSAT at these orders.

Every needed cube k≥d at the remaining leftover holes through n=108 is UNSAT. 1026 stored DRATs. Independent replay: python3 verify_range.py --n-min 73 --n-max 108 in three batches (516+244+266), 0 failures. The slowest stored cube is about 27s (n=108).

So every oriented graph on one of those n with δ⁺ ≥ ⌈n/3⌉ has a directed triangle. This is a dent against those finite holes. After n=72 every leftover n is consecutive (the n≡1 (mod 3) window implied by HKN 0.3465 ended near n=50).

2026-08-27 — F₄ with the CKLS fork

The stored parent certificate at c=0.34645 still replays (worst F=−0.12343). A new Farkas ray on the same 32 types, with the published CKLS 2015 constant β<0.8616γ in place of CSS β≤γ, certifies c=0.34640. Replay: python3 verify_q4_certificate.py certs/keep/f4_or_new_certificate.json --margin 0.05 (worst F=−0.4190333660 at r₃₀, min eig(Q)=6.19·10⁻¹⁰). Hunt log: t at 0.34645 is −38.5; at 0.34640 is −0.419; at 0.346 / 0.340 / 0.3388 the best t stays positive. Did not beat 0.3388. HKN already said tightening Lemma 3.5 only gives a tiny decrease; this is that fifth-decimal move, now with a public certificate.

The first remaining hole is n=109, δ⁺=37. The conjecture 1/3 is open. Did not treat 0.3388 as published.

2026-08-27 — wrap: inventory, n=109 residue, merge main

Re-fetched HKN v4 (arXiv:0908.2791, Theorem 1.2 still 0.3465n; no v5) and CKLS (arXiv:0909.2468, Theorem 2.5: β<0.8616γ). Keep/ has exactly the 1026 needed cubes for leftover n=73..108, no extras, none ≥90 MB. n=109 was started (high-k cubes k=38..70 came back UNSAT) and interrupted before the k=d end; those files were not stored. Residue, not a lower bound. First remaining hole still n=109.

Merged origin/main into this branch. README Problems/ledger now keep the later claims (ionization 1.1057, CCR 1.44655, Landau 0.22525, Jacobian deg 125, kissing leftover, Hilbert 16(b), …) together with leftover CH through n=108 and F₄ c=0.34640.

2026-08-27 — leftover cubes n=109–112

Same encoder as q1–q4. High-k first, kissat 4.0.4, DRAT against a regenerated CNF. New proofs live in compute/q5/certs/keep/ (q4 stays the n=73–108 store).

Every needed cube at leftover n=109 through n=114 is UNSAT. 213 stored DRATs, all under 8 MB after drat-trim -l cores. Independent replay: python3 verify_range.py --n-min 109 --n-max 114 in five batches (69+36+35+36+37), 0 failures.

Dent against those finite leftover holes. n=115 was started and is not fully stored. Residue, not a bound.

F₄ hunt below 0.34640 is residue. The stored ray at 0.34640 still replays (worst F=−0.419 at r₃₀). The same (Q,b,cT,cV,d) at 0.34639 is already positive (worst F≈+8.44; HiGHS refit t≈+7.21). Warm Qs and extras at css_beta=0.8616 and 1/(1+0.16065) stay positive at 0.34639 / 0.34638 / 0.34635. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=115, δ⁺=39. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=115

Same encoder as q1–q5. New proofs live in compute/q6/certs/keep/ (q5 stays the n=109–114 store).

Leftover n=115 is closed: d=39, cubes k=39..74, 36 stored DRATs, all under 11 MB after drat-trim -l (k=40 is 10.2 MB). Independent replay: python3 verify_range.py --n-min 115 --n-max 115 reports 36 checked, 0 failures.

Dent against that finite leftover hole. n=116 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=116, δ⁺=39. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=116

Same encoder as q1–q6. New proofs live in compute/q7/certs/keep/ (q6 stays the n=115 store).

Leftover n=116 is closed: d=39, cubes k=39..75, 37 stored DRATs, all under 8 MB. Independent replay: python3 verify_range.py --n-min 116 --n-max 116 reports 37 checked, 0 failures.

Dent against that finite leftover hole. n=117 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=117, δ⁺=39. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=117

Same encoder as q1–q7. New proofs live in compute/q8/certs/keep/ (q7 stays the n=116 store).

Leftover n=117 is closed: d=39, cubes k=39..76, 38 stored DRATs, all under 10 MB after drat-trim -l (k=40 is 9.2 MB). Independent replay: python3 verify_range.py --n-min 117 --n-max 117 reports 38 checked, 0 failures.

Dent against that finite leftover hole. n=118 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=118, δ⁺=40. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=118

Same encoder as q1–q8. New proofs live in compute/q9/certs/keep/ (q8 stays the n=117 store).

Leftover n=118 is closed: d=40, cubes k=40..76, 37 stored DRATs, all under 8 MB after drat-trim -l (k=74 is 7.5 MB). Independent replay: python3 verify_range.py --n-min 118 --n-max 118 reports 37 checked, 0 failures.

Dent against that finite leftover hole. n=119 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=119, δ⁺=40. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=119

Same encoder as q1–q9. New proofs live in compute/q10/certs/keep/ (q9 stays the n=118 store).

Leftover n=119 is closed: d=40, cubes k=40..77, 38 stored DRATs, all under 8 MB after drat-trim -l (k=75 is 7.6 MB). Independent replay: python3 verify_range.py --n-min 119 --n-max 119 reports 38 checked, 0 failures.

Dent against that finite leftover hole. n=120 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=120, δ⁺=40. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=120

Same encoder as q1–q10. New proofs live in compute/q11/certs/keep/ (q10 stays the n=119 store).

Leftover n=120 is closed: d=40, cubes k=40..78, 39 stored DRATs after drat-trim -l (k=40 is 25.2 MB; k=44 is 16.1 MB). Independent replay: python3 verify_range.py --n-min 120 --n-max 120 reports 39 checked, 0 failures.

Dent against that finite leftover hole. n=121 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=121, δ⁺=41. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=121

Same encoder as q1–q11. New proofs live in compute/q12/certs/keep/ (q11 stays the n=120 store).

Leftover n=121 is closed: d=41, cubes k=41..78, 38 stored DRATs after drat-trim -l (k=41 is 9.0 MB; k=42 is 8.3 MB). Independent replay: python3 verify_range.py --n-min 121 --n-max 121 reports 38 checked, 0 failures.

Dent against that finite leftover hole. n=122 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=122, δ⁺=41. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=122

Same encoder as q1–q12. New proofs live in compute/q13/certs/keep/ (q12 stays the n=121 store).

Leftover n=122 is closed: d=41, cubes k=41..79, 39 stored DRATs after drat-trim -l (k=45 is 7.0 MB). Independent replay: python3 verify_range.py --n-min 122 --n-max 122 reports 39 checked, 0 failures.

Dent against that finite leftover hole. n=123 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=123, δ⁺=41. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=123

Same encoder as q1–q13. New proofs live in compute/q14/certs/keep/ (q13 stays the n=122 store).

Leftover n=123 is closed: d=41, cubes k=41..80, 40 stored DRATs after drat-trim -l (k=41 is 12.0 MB; k=44 is 11.1 MB). Independent replay: python3 verify_range.py --n-min 123 --n-max 123 reports 40 checked, 0 failures.

Dent against that finite leftover hole. n=124 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=124, δ⁺=42. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=124

Same encoder as q1–q14. New proofs live in compute/q15/certs/keep/ (q14 stays the n=123 store).

Leftover n=124 is closed: d=42, cubes k=42..80, 39 stored DRATs after drat-trim -l (k=44 is 11.1 MB). Independent replay: python3 verify_range.py --n-min 124 --n-max 124 reports 39 checked, 0 failures.

Dent against that finite leftover hole. n=125 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=125, δ⁺=42. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=125

Same encoder as q1–q15. New proofs live in compute/q16/certs/keep/ (q15 stays the n=124 store).

Leftover n=125 is closed: d=42, cubes k=42..81, 40 stored DRATs after drat-trim -l (k=44 is 9.0 MB). Independent replay: python3 verify_range.py --n-min 125 --n-max 125 reports 40 checked, 0 failures.

Dent against that finite leftover hole. n=126 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=126, δ⁺=42. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=126

Same encoder as q1–q16. New proofs live in compute/q17/certs/keep/ (q16 stays the n=125 store).

Leftover n=126 is closed: d=42, cubes k=42..82, 41 stored DRATs after drat-trim -l (k=45 is 6.0 MB). Independent replay: python3 verify_range.py --n-min 126 --n-max 126 reports 41 checked, 0 failures.

Dent against that finite leftover hole. n=127 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=127, δ⁺=43. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=127

Same encoder as q1–q17. New proofs live in compute/q18/certs/keep/ (q17 stays the n=126 store).

Leftover n=127 is closed: d=43, cubes k=43..82, 40 stored DRATs after drat-trim -l (k=47 is 11.6 MB). Independent replay: python3 verify_range.py --n-min 127 --n-max 127 reports 40 checked, 0 failures.

Dent against that finite leftover hole. n=128 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=128, δ⁺=43. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=128

Same encoder as q1–q18. New proofs live in compute/q19/certs/keep/ (q18 stays the n=127 store).

Leftover n=128 is closed: d=43, cubes k=43..83, 41 stored DRATs after drat-trim -l (k=43 is 12.5 MB). Independent replay: python3 verify_range.py --n-min 128 --n-max 128 reports 41 checked, 0 failures.

Dent against that finite leftover hole. n=129 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=129, δ⁺=43. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=129

Same encoder as q1–q19. New proofs live in compute/q20/certs/keep/ (q19 stays the n=128 store).

Leftover n=129 is closed: d=43, cubes k=43..84, 42 stored DRATs after drat-trim -l (k=44 is 7.4 MB). Independent replay: python3 verify_range.py --n-min 129 --n-max 129 reports 42 checked, 0 failures.

Dent against that finite leftover hole. n=130 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=130, δ⁺=44. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=130

Same encoder as q1–q20. New proofs live in compute/q21/certs/keep/ (q20 stays the n=129 store).

Leftover n=130 is closed: d=44, cubes k=44..84, 41 stored DRATs after drat-trim -l (k=48 is 15.6 MB). Independent replay: python3 verify_range.py --n-min 130 --n-max 130 reports 41 checked, 0 failures.

Dent against that finite leftover hole. n=131 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=131, δ⁺=44. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=131

Same encoder as q1–q21. New proofs live in compute/q22/certs/keep/ (q21 stays the n=130 store).

Leftover n=131 is closed: d=44, cubes k=44..85, 42 stored DRATs after drat-trim -l (k=46 is 12.7 MB). Independent replay: python3 verify_range.py --n-min 131 --n-max 131 reports 42 checked, 0 failures.

Dent against that finite leftover hole. n=132 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=132, δ⁺=44. Conjecture 1/3 open.

2026-08-27 — leftover cubes from n=132

Same encoder as q1–q22. New proofs live in compute/q23/certs/keep/ (q22 stays the n=131 store).

Leftover n=132 is closed: d=44, cubes k=44..86, 43 stored DRATs after drat-trim -l (k=44 is 11.9 MB). Independent replay: python3 verify_range.py --n-min 132 --n-max 132 reports 43 checked, 0 failures.

Dent against that finite leftover hole. n=133 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=133, δ⁺=45. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=133

Same encoder as q1–q23. New proofs live in compute/q24/certs/keep/ (q23 stays the n=132 store).

Leftover n=133 is closed: d=45, cubes k=45..86, 42 stored DRATs after drat-trim -l (k=45 is 10.8 MB). Independent replay: python3 verify_range.py --n-min 133 --n-max 133 reports 42 checked, 0 failures.

Dent against that finite leftover hole. n=134 is started and is not fully stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=134, δ⁺=45. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=134

Same encoder as q1–q24. New proofs live in compute/q25/certs/keep/ (q24 stays the n=133 store).

Leftover n=134 is closed: d=45, cubes k=45..87, 43 stored DRATs after drat-trim -l (k=46 is 15.5 MB). Independent replay: python3 verify_range.py --n-min 134 --n-max 134 reports 43 checked, 0 failures.

Dent against that finite leftover hole. n=135 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=135, δ⁺=45. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=135

Same encoder as q1–q25. New proofs live in compute/q26/certs/keep/ (q25 stays the n=134 store).

Leftover n=135 is closed: d=45, cubes k=45..88, 44 stored DRATs after drat-trim -l (k=49 is 17.1 MB). Independent replay: python3 verify_range.py --n-min 135 --n-max 135 reports 44 checked, 0 failures.

Dent against that finite leftover hole. n=136 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=136, δ⁺=46. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=136

Same encoder as q1–q26. New proofs live in compute/q27/certs/keep/ (q26 stays the n=135 store).

Leftover n=136 is closed: d=46, cubes k=46..88, 43 stored DRATs after drat-trim -l (k=50 is 13.0 MB). Independent replay: python3 verify_range.py --n-min 136 --n-max 136 reports 43 checked, 0 failures.

Dent against that finite leftover hole. n=137 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=137, δ⁺=46. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=137

Same encoder as q1–q27. New proofs live in compute/q28/certs/keep/ (q27 stays the n=136 store).

Leftover n=137 is closed: d=46, cubes k=46..89, 44 stored DRATs after drat-trim -l (k=46 is 13.0 MB). Independent replay: python3 verify_range.py --n-min 137 --n-max 137 reports 44 checked, 0 failures.

Dent against that finite leftover hole. n=138 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=138, δ⁺=46. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=138

Same encoder as q1–q28. New proofs live in compute/q29/certs/keep/ (q28 stays the n=137 store).

Leftover n=138 is closed: d=46, cubes k=46..90, 45 stored DRATs after drat-trim -l (k=48 is 16.4 MB). Independent replay: python3 verify_range.py --n-min 138 --n-max 138 reports 45 checked, 0 failures.

Dent against that finite leftover hole. n=139 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=139, δ⁺=47. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=139

Same encoder as q1–q29. New proofs live in compute/q30/certs/keep/ (q29 stays the n=138 store).

Leftover n=139 is closed: d=47, cubes k=47..90, 44 stored DRATs after drat-trim -l (k=49 is 18.5 MB). Independent replay: python3 verify_range.py --n-min 139 --n-max 139 reports 44 checked, 0 failures.

Dent against that finite leftover hole. n=140 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=140, δ⁺=47. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=140

Same encoder as q1–q30. New proofs live in compute/q31/certs/keep/ (q30 stays the n=139 store).

Leftover n=140 is closed: d=47, cubes k=47..91, 45 stored DRATs after drat-trim -l (k=50 is 22 MB). Independent replay: python3 verify_range.py --n-min 140 --n-max 140 reports 45 checked, 0 failures.

Dent against that finite leftover hole. n=141 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=141, δ⁺=47. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=141

Same encoder as q1–q31. New proofs live in compute/q32/certs/keep/ (q31 stays the n=140 store).

Leftover n=141 is closed: d=47, cubes k=47..92, 46 stored DRATs after drat-trim -l (k=48 is 19 MB). Independent replay: python3 verify_range.py --n-min 141 --n-max 141 reports 46 checked, 0 failures.

Dent against that finite leftover hole. n=142 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=142, δ⁺=48. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=142

Same encoder as q1–q32. New proofs live in compute/q33/certs/keep/ (q32 stays the n=141 store).

Leftover n=142 is closed: d=48, cubes k=48..92, 45 stored DRATs after drat-trim -l (k=49 is 27 MB). Independent replay: python3 verify_range.py --n-min 142 --n-max 142 reports 45 checked, 0 failures.

Dent against that finite leftover hole. n=143 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=143, δ⁺=48. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=143

Same encoder as q1–q33. New proofs live in compute/q34/certs/keep/ (q33 stays the n=142 store).

Leftover n=143 is closed: d=48, cubes k=48..93, 46 stored DRATs after drat-trim -l (k=54 is 18.5 MB). Independent replay: python3 verify_range.py --n-min 143 --n-max 143 reports 46 checked, 0 failures.

Dent against that finite leftover hole. n=144 is closed in the same folder (next paragraph). n=145 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

2026-08-28 — leftover cubes from n=144

Same encoder as q1–q33. Proofs for this order also live in compute/q34/certs/keep/.

Leftover n=144 is closed: d=48, cubes k=48..94, 47 stored DRATs after drat-trim -l (k=54 is 23.9 MB). Independent replay: python3 verify_range.py --n-min 144 --n-max 144 reports 47 checked, 0 failures.

Dent against that finite leftover hole. n=145 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=145, δ⁺=49. Conjecture 1/3 open.

2026-08-28 — leftover cubes from n=145

Same encoder as q1–q34. New proofs live in compute/q35/certs/keep/ (q34 stays the n=143–144 store).

Leftover n=145 is closed: d=49, cubes k=49..94, 46 stored DRATs after drat-trim -l (k=51 is 15.0 MB). Independent replay: python3 verify_range.py --n-min 145 --n-max 145 reports 46 checked, 0 failures.

Dent against that finite leftover hole. n=146 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=146, δ⁺=49. Conjecture 1/3 open.

2026-08-29 — leftover cubes from n=146

Same encoder as q1–q35. New proofs live in compute/q36/certs/keep/ (q35 stays the n=145 store).

Leftover n=146 is closed: d=49, cubes k=49..95, 47 stored DRATs after drat-trim -l (k=50 is 24.2 MB). Independent replay: python3 verify_range.py --n-min 146 --n-max 146 reports 47 checked, 0 failures.

Dent against that finite leftover hole. n=147 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=147, δ⁺=49. Conjecture 1/3 open.

2026-08-29 — leftover cubes from n=147

Same encoder as q1–q36. New proofs live in compute/q37/certs/keep/ (q36 stays the n=146 store).

Leftover n=147 is closed: d=49, cubes k=49..96, 48 stored DRATs after drat-trim -l (k=50 is 16.9 MB). Independent replay: python3 verify_range.py --n-min 147 --n-max 147 reports 48 checked, 0 failures.

Dent against that finite leftover hole. n=148 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=148, δ⁺=50. Conjecture 1/3 open.

2026-08-29 — leftover cubes from n=148

Same encoder as q1–q37. New proofs live in compute/q38/certs/keep/ (q37 stays the n=147 store).

Leftover n=148 is closed: d=50, cubes k=50..96, 47 stored DRATs after drat-trim -l (k=52 is 27.6 MB). Independent replay: python3 verify_range.py --n-min 148 --n-max 148 reports 47 checked, 0 failures.

Dent against that finite leftover hole. n=149 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=149, δ⁺=50. Conjecture 1/3 open.

2026-08-29 — leftover cubes from n=149 (q39 start)

Same encoder as q1–q38. New proofs will live in compute/q39/certs/keep/ (q38 stays the n=148 store).

Independent cube bounds at leftover n=149: ⌈149/3⌉=50, so d=50. HKN 0.3465·149=51.6285 and the stored F₄ 0.34640·149=51.6136 both sit above 50, so the order is leftover. Even the 0.3388 personal communication still has 0.3388·149=50.4812>50. A 50-outregular graph on 149 vertices has 7450 arcs, so some in-degree is at least 50. Each v∈N⁺(0) needs 50 outs from (N⁺(0){v})∪U, size 147−k, hence k≤97. Absolute max k=98 is empty by that N⁺ cut. Needed cubes: k=50..97 (48). The 2-cycle covering count on A empties k≥73; SAT work is k=50..72. That is the same arithmetic as n=148, recomputed here, not copied as a prescription.

F₄ stays 0.34640. Did not beat 0.3388. n=149 not stored yet. Residue until the 48 DRATs exist and an independent verify_range reports 0 failures.

2026-08-29 — leftover cubes from n=149

Same encoder as q1–q38. New proofs live in compute/q39/certs/keep/ (q38 stays the n=148 store).

Leftover n=149 is closed: d=50, cubes k=50..97, 48 stored DRATs after drat-trim -l (k=51 is 28.3 MB). Independent replay: python3 verify_range.py --n-min 149 --n-max 149 reports 48 checked, 0 failures.

Dent against that finite leftover hole. n=150 is not stored. Residue, not a bound.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=150, δ⁺=50. Conjecture 1/3 open.

2026-08-29 — leftover cubes from n=150 (q40 start)

Same encoder as q1–q39. New proofs will live in compute/q40/certs/keep/ (q39 stays the n=149 store).

Independent cube bounds at leftover n=150: ⌈150/3⌉=50, so d=50. HKN 0.3465·150=51.975 and the stored F₄ 0.34640·150=51.96 both sit above 50, so the order is leftover. Even the 0.3388 personal communication still has 0.3388·150=50.82>50. A 50-outregular graph on 150 vertices has 7500 arcs, so some in-degree is at least 50. Each v∈N⁺(0) needs 50 outs from (N⁺(0){v})∪U, size 148−k, hence k≤98. Absolute max k=99 is empty by that N⁺ cut. Needed cubes: k=50..98 (49). The 2-cycle covering count on A empties k≥74 (σ=n−2−d−k=98−k; survive when σ≥⌊(d−1)/2⌋+1=25, i.e. k≤73). SAT work is k=50..73. That is the same arithmetic as n=149, recomputed here, not copied as a prescription.

F₄ stays 0.34640. Did not beat 0.3388. n=150 not stored yet. Residue until the 49 DRATs exist and an independent verify_range reports 0 failures. Stored leftover SAT is residue, not a bound. A dent is only a verified move of F₄ below 0.3388, or a new exact-CH theorem.

2026-08-29 — leftover cubes from n=150

Same encoder as q1–q39. New proofs live in compute/q40/certs/keep/ (q39 stays the n=149 store).

Leftover n=150 is closed: d=50, cubes k=50..98, 49 stored DRATs after drat-trim -l (k=52 is 37.9 MB). Independent replay: python3 verify_range.py --n-min 150 --n-max 150 reports 49 checked, 0 failures.

Stored leftover SAT is residue, not a bound. n=151 is not stored. A dent is only a verified move of F₄ below 0.3388, or a new exact-CH theorem.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=151, δ⁺=51. Conjecture 1/3 open.

2026-08-29 — leftover cubes from n=151 (q41 start)

Same encoder as q1–q40. New proofs will live in compute/q41/certs/keep/ (q40 stays the n=150 store).

Independent cube bounds at leftover n=151: ⌈151/3⌉=51, so d=51. HKN 0.3465·151=52.3215 and the stored F₄ 0.34640·151=52.3064 both sit above 51, so the order is leftover. Even the 0.3388 personal communication still has 0.3388·151=51.1588>51. A 51-outregular graph on 151 vertices has 7701 arcs, so some in-degree is at least 51. Each v∈N⁺(0) needs 51 outs from (N⁺(0){v})∪U, size 149−k, hence k≤98. Absolute max k=99 is empty by that N⁺ cut. Needed cubes: k=51..98 (48). The 2-cycle covering count on A empties k≥73 (σ=n−2−d−k=98−k; survive when σ≥⌊(d−1)/2⌋+1=26, i.e. k≤72). SAT work is k=51..72. That arithmetic is recomputed here, not copied as a prescription.

F₄ stays 0.34640. Did not beat 0.3388. n=151 not stored yet. Residue until the 48 DRATs exist and an independent verify_range reports 0 failures. Stored leftover SAT is residue, not a bound. A dent is only a verified move of F₄ below 0.3388, or a new exact-CH theorem.

2026-08-29 — leftover cubes from n=151

Same encoder as q1–q40. New proofs live in compute/q41/certs/keep/ (q40 stays the n=150 store).

Leftover n=151 is closed: d=51, cubes k=51..98, 48 stored DRATs after drat-trim -l (k=52 is 35.3 MB). Independent replay: python3 verify_range.py --n-min 151 --n-max 151 reports 48 checked, 0 failures.

Stored leftover SAT is residue, not a bound. n=152 is not stored. A dent is only a verified move of F₄ below 0.3388, or a new exact-CH theorem.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=152, δ⁺=51. Conjecture 1/3 open.

2026-08-29 — leftover cubes from n=152 (q42 start)

Same encoder as q1–q41. New proofs will live in compute/q42/certs/keep/ (q41 stays the n=151 store).

Independent cube bounds at leftover n=152: ⌈152/3⌉=51, so d=51. HKN 0.3465·152=52.668 and the stored F₄ 0.34640·152=52.6528 both sit above 51, so the order is leftover. Even the 0.3388 personal communication still has 0.3388·152=51.4976>51. A 51-outregular graph on 152 vertices has 7752 arcs, so some in-degree is at least 51. Each v∈N⁺(0) needs 51 outs from (N⁺(0){v})∪U, size 150−k, hence k≤99. Absolute max k=100 is empty by that N⁺ cut. Needed cubes: k=51..99 (49). The 2-cycle covering count on A empties k≥74 (σ=n−2−d−k=99−k; survive when σ≥⌊(d−1)/2⌋+1=26, i.e. k≤73). SAT work is k=51..73. That arithmetic is recomputed here, not copied as a prescription.

F₄ stays 0.34640. Did not beat 0.3388. n=152 not stored yet. Residue until the 49 DRATs exist and an independent verify_range reports 0 failures. Stored leftover SAT is residue, not a bound. A dent is only a verified move of F₄ below 0.3388, or a new exact-CH theorem.

2026-08-29 — leftover cubes from n=152

Same encoder as q1–q41. New proofs live in compute/q42/certs/keep/ (q41 stays the n=151 store).

Leftover n=152 is closed: d=51, cubes k=51..99, 49 stored DRATs after drat-trim -l (k=51 is 31.8 MB). Independent replay: python3 verify_range.py --n-min 152 --n-max 152 reports 49 checked, 0 failures.

Stored leftover SAT is residue, not a bound. n=153 is not stored. A dent is only a verified move of F₄ below 0.3388, or a new exact-CH theorem.

F₄ stays 0.34640. The stored CKLS-fork ray still replays. Did not overwrite q4/certs/keep/f4_or_new_certificate.json. Did not beat 0.3388.

First remaining hole n=153, δ⁺=51. Conjecture 1/3 open.