What remains

The primary source for Wróblewski's 1984 construction / Erdős #169

Read (Math. Comp. 43, 261–262, two pages in all). The proofs of Lemmas 1 and 2 are written out and machine-checked, so the dependence on those lemmas that the article listed among its limits is gone. Lean

The scale at which the Behrend-type construction starts to beat the self-similar continuation is 2^24.4, and the contribution from there on is 5.5×10⁻⁴, which is where almost the whole of the excess over the record is generated.

→ The Erdős conjecture on arithmetic progressions

The generator that "adds the point which increases α least" / Hadwiger–Nelson

No proxy variable exists. The form of the generator is settled (Δα ∈ {0,1}; Δα = 0 ⟺ the unit circle meets every maximum independent set; the candidate points are the intersections of unit circles about existing pairs), and it is closed as far as α = 2 requiring n ≤ 7, with the maximum 3.5 attained by the Moser spindle. paper

The route has a ceiling of its own — the best known density 0.22936 for a measurable set avoiding unit distances imposes an upper bound of 4.36 on the fractional chromatic number, so 5 cannot come out of this route. known

→ The Hadwiger–Nelson problem

A closed form for the constant C, and what the oscillation is / Collatz

The formula is written down. C = q²p/(ln2·(log₂3 − 4/3)) = 0.4215205965. Here q and p are the two factors of the Spitzer–Baxter series (the Wiener–Hopf factorisation) for the descending ladder. Only the overshoot factor oscillates; q is constant to thirteen digits. paper

The oscillation is identified too. It is a superposition of sawtooth modes indexed by the convergent denominators n of log₂3, with period T_n = (log₂3 − 4/3)/‖n·log₂3‖. The transfer operator has largest eigenvalue exactly 1/2, right eigenfunction 2^−x, and no spectral gap. The limit has a closed form; the value at each depth does not — that is the shape of this constant. paper

→ That constant is not yet a constant

The martingale line / Collatz

Closed. The +1/3 is not the obstacle: with n^s (0 < s < 1) the same computation gives a non-negative supermartingale, and the convergence theorem applies. That the sign bites only at s = 1 is an artefact of the coordinate, coming from the critical multiplier θ* = 1.

And the line itself is closed by the cycles of 3n−1. Supermartingale convergence gives a fixed point, while 3n−1 has cycles of length 2 and 7. The existence of the cycles is a proof that the process is not a supermartingale. A probabilistic argument that concludes Collatz would, by the same computation, conclude something false about 3n−1. paper

→ Only 3n+1 is exactly critical

Beyond the sign of 1/3 — where the asymmetry is decided / Collatz

On the side of the 3-adic limit measure it cannot be answered in principle (every quantity built from that side is invariant under the sign). The answer is on the 2-adic side. In the model e_k+1 − e_k = v_k+1 − g_k, where v is Terras's 2-adic drop and g_k = ⌊(k+1)·log₂3⌋ − ⌊k·log₂3⌋ ∈ {1,2} is the Sturmian word of slope log₂3, a descent needs v = 1 and g = 2 at once, while an ascent needs only one of the two. Hence the asymmetry is

The same inequality gives that three consecutive descents never occur (the forbidden word DDD). Moving the multiplier away from 3, the sign flips at Q* = 2^5/3. Lean · axiom log pending for the inequality and the forbidden word (Collatz1139.no_three_consecutive_descents, asymmetry_negative). The premises of the model — that v follows the Terras distribution and is independent of g — are known ingredients and measurement. known

→ What the sign of 1/3 decides

The route "replace the head of f(3)" / Erdős #169

It was not a different route. Replacing the head (the small numbers) is a restatement of improving the record itself. It is no longer listed as a separate route. known

→ The Erdős conjecture on arithmetic progressions

The AP-free condition for families whose contraction ratio differs by branch / Erdős #169

The condition can be written in the form of window separation (a condition looking only at the enclosing intervals), and it is machine-checked. Solving the window-separated Bellman equation reduces the number of levels from 100 to 84, and the reciprocal sum of a set containing no 3-term arithmetic progression rises to 3.0085385. That the set contains no 3-AP and that it exceeds the 1984 record of 3.00849 is a single theorem. LeanShiori959.erdos169_lower_record_939

What remains now is outside the frame of this construction. Use four or more windows, or a family of blocks other than Behrend. The room left inside the frame is, on a rough estimate, about 5×10⁻⁶.

The depth at which the limit of the constant C becomes visible / Collatz

The depth at which the value stays within ±0.01% is s ≈ 6–7×10⁵, with an envelope decaying like s^−1/2. paper But this number depends on how much length is looked at in one go — the component producing the oscillation has a period of about 4,000, and measuring with a window shorter than that makes the apparent depth come out two orders of magnitude shallower.

What remains now is on the side of the question. "Window width" is not part of the question, so the answer is not pinned to one number. To write a single number, the window width has to be fixed first.

The fifth Lovász exception / the Lovász conjecture

The place to search splits three ways. By the deficiency def = |V| − circumference (the perimeter gap): (I) def = 1 (hypohamiltonian), (II) truncations (def ≡ 0 mod 3), (III) def ≥ 2 and not a truncation. Box II is empty up to 3,840 vertices (a truncation T(H) has 3|V(H)| vertices, and T(H) is Hamiltonian whenever H is). Truncation freezes after one generation — T²(G) is never vertex-transitive. paper Box III has no example at all. The conjecture "no connected vertex-transitive graph has def = 2" contains the vertex-transitive case of Grünbaum's 1974 conjecture. known

Without vertex-transitivity, def = 2 does occur — among cubic bipartite graphs, three isomorphism classes on 30 vertices (45 edges each, girth 4). LeanShiori1161.G30_def2, Shiori1193.G30b_def2, G30c_def2. That none exists on 28 or fewer vertices is what was checked on this machine. computation

The number of Hamiltonian cycles of the generalised Petersen graph GP(n,3) is a multiple of n for every odd n ≥ 7. LeanShiori1202.gp3_dvd_hc_odd This quantity is invariant under automorphisms, so it cannot be used to prove non-Hamiltonicity.

What remains now is whether box III contains a vertex-transitive graph at all. Restricted to cubic graphs, everything up to 1,280 vertices has been exhaustively checked and the exceptions are the four known ones, so if there is one it is above that.

Hadwiger–Nelson — the goal is stated differently now / Hadwiger–Nelson

The goal "beat the Moser spindle's n/α = 3.5" has lost its meaning in the literature — that the fractional chromatic number of the plane is at least 4, and that finite unit-distance graphs with independence ratio below 1/4 exist (Dúcz–Varga, arXiv:2606.28157), are known. known What is left is the exact value of f(α), the largest number of vertices of a unit-distance graph with independence number at most α.

f(3) = 10 and 14 ≤ f(4) ≤ 15. The lower bounds are Moser ⊔ K₃ and Moser ⊔ Moser; the upper bounds are certificates that the 117 candidate graphs on 11 vertices and the 2,100 on 16 vertices are not realisable in the plane. LeanShiori1183.fGe_10_3, fGe_14_4, Shiori1178.hn11_no_realiz, Shiori1185.hn16_no_realiz, Shiori1189.hn10_no_realiz. That the enumeration of candidates is exhaustive is what was checked on this machine. computation

What remains now is the single cell n = 15, α = 4. If it closes, f(4) = 14; if it hits, a witness for f(4) = 15.