Erdős problem 551 — wave 5z

Run date: 2026-07-26 UTC.

Mathematical claim labels used below:

• [a] elementary-rigorous: proved in this report from definitions and elementary facts.
• [b] rigorous-modulo-named-theorem: the deduction is rigorous conditional on the accurately cited theorem.
• [c] plausible/structural-unverified: a possible route or literature-search conclusion, not a theorem.
• [d] computational-only: established by the standalone computation, without being promoted to a theorem.

Page and bibliographic transcriptions are source facts rather than mathematical claims.

0. Mandatory live-page check

I used the Bright Data anti-bot Chromium path required by the prompt. The browser connected successfully to Bright Data, but each attempt to load the problem, its non-www redirect, and its discussion thread returned Cloudflare HTTP 522, origin connection timed out. The final retry at approximately 2026-07-26 23:41 UTC again had title erdosproblems.com | 522: Connection timed out. Direct curl returned the Cloudflare challenge and was not used as page evidence.

I therefore could not truthfully certify the origin's state at the exact run time. I used the most recent indexed copies instead:

• problem 551, indexed with an access date of 2026-06-16;
• discussion thread 551, indexed with an access date of 2026-05-09 and still returned by the web retrieval backend;
• the site's canonical database repository, fetched live at commit e5145a87748092babd7b4f990c493c0ab46edf10, dated 2026-07-26 19:08:01 UTC. Its entry for 551 still says status: decidable and informal_status: decidable (the entry's own last_update field is 2025-08-31).

Thus the page content below is the freshest retrievable snapshot, not a falsely labelled live-origin read. A worker or claim posted after the last indexed snapshot cannot be excluded while the origin is down.

Verbatim statement

> Prove that\[R(C_k,K_n)=(k-1)(n-1)+1\]for $k\geq n\geq 3$ (except when $n=k=3$).

The page status is DECIDABLE — Resolved up to a finite check, not PROVED, DISPROVED, or FALSIFIED. It attributes the question to Erdős, Faudree, Rousseau, and Schelp and lists:

• Bondy–Erdős for \(k>n^2-2\);
• Nikiforov for \(k\ge 4n+2\);
• Keevash–Long–Skokan for \(k\ge C\log n/\log\log n\) for some absolute \(C\), hence all sufficiently large \(n\);
• the associated questions asking for the first valid \(k\) at fixed \(n\), and for \(\min_k R(C_k,K_n)\).

The indexed discussion has exactly one comment:

> Technically the problem has been reduced to a decidable (finitary) problem, but is still open.

It is by Terence Tao, 2025-09-01. The coordination fields in that snapshot are:

Likes this problem                         None
Interested in collaborating               None
Currently working on this problem         None
This problem looks difficult              None
This problem looks tractable              None
The results could be formalisable         None
Working on formalising the results        None

No claimed proof or solution is present in the retrieved problem or thread, and the live canonical YAML still has the decidable status. On that evidence the mandatory stop condition was not triggered, subject to the explicit origin-outage caveat above.

1. Primary-source literature audit

I downloaded and text-checked the following sources. The hashes make the audit reproducible.

| Source | Checked claim | SHA-256 of checked PDF |

|---|---|---|

| Erdős–Faudree–Rousseau–Schelp, J. Graph Theory 2 (1978), 53–64 | Original cycle–complete problem and related questions. | 375bdd8f88a6dd1c054452ef4a1cd63da9f81a4864f0d31b797f950e7523fb3e |

| Bondy–Erdős, JCT B 14 (1973), 46–5480005-X) | Earlier long-cycle range. | a0261f0bf99bf32bbcf0e39904c7342ae6807ba99530d2a49d4d2c28b08ab6cb |

| Nikiforov, Combin. Probab. Comput. 14 (2005), 349–370; arXiv:math/0404501 | The accepted \(k\ge4n+2\) theorem; Case 4.1 was audited line by line below. | 7b2f94cc407ad2683ff38d1d31e432d0022349838a47a8df88e96f6de09cb1f4 |

| Keevash–Long–Skokan, IMRN 2021, 275–300; arXiv:1807.06376 | \(k\ge C\log n/\log\log n\) for an absolute \(C\). Their concluding remarks explicitly say that they did not compute \(C\); “less than 20” is only suggested as obtainable with more work. | 0459c5f2cdc64796db985e8e876a58b3c1caea0e860e161939df60f9b169acf9 |

| Chen–Cheng–Zhang, European J. Combin. 29 (2008), 1337–1352 (preprint) | \(R(C_k,K_7)=6k-5\) for every \(k\ge7\). | Primary preprint inspected. |

| Baniabedalruhman, JJMS 16(4) (2023), 703–718 | \(R(C_k,K_8)=7k-6\) for \(10\le k\le15\). | 1ede5655c02ef75577f60d296a2aead24f52c157c08cade7449e3757070b13c7 |

| Radziszowski, Small Ramsey Numbers, DS1.18, revision 2026-04-24 | Current survey check: all \(K_m\) cases for \(m\le7\), \(R(C_8,K_8)\), \(R(C_9,K_8)\), and the \(10\le k\le15\) range are recorded; the general \(K_8\) row remains conjectural. | 9519a676ee381f02f03269c22e3f101162b2fdcc9d432e4103cb1192fdff91bc |

The \(K_8\) boundary papers additionally checked were Jaradat–Alzaleq for \(R(C_8,K_8)=50\) and Bataineh–Jaradat–Al-Zaleq, DOI 10.5402/2011/926191, for \(R(C_9,K_8)=57\).

Searches on 2026-07-26 for exact strings R(C16,K8), R(C_16,K_8), later \(K_8\) cycle ranges, and corrections/errata to Nikiforov found no primary source settling \(C_{16}\) versus \(K_8\), and no erratum to the arithmetic issue in Section 4 below. [c] This is an honest search miss, not a proof that no such source exists.

2. Exact published frontier and the first finite kernel

[b] Combining the \(K_8\) results through \(k=15\) with Nikiforov's accepted \(k\ge4n+2\) theorem gives the following fully explicit \(n=8\) row:

| Cycle length \(k\) | Value/status located |

|---:|---|

| 8 | \(R(C_8,K_8)=50\) |

| 9 | \(R(C_9,K_8)=57\) |

| 10 | 64 |

| 11 | 71 |

| 12 | 78 |

| 13 | 85 |

| 14 | 92 |

| 15 | 99 |

| 16 through 33 | not settled by the located/current-survey sources |

| \(k\ge34\) | \(R(C_k,K_8)=7k-6\) |

Thus [b] the first pair not settled by those sources is

The standard lower construction is \(7K_{15}\) on 105 vertices. [a] Every cycle lies in a 15-vertex component and every independent set takes at most one vertex from each of the seven components, so it has no \(C_{16}\) and has independence number exactly 7. The standalone script reconstructs and checks this graph.

Consequently [a], conditional only on the definition of the Ramsey number, the first case is exactly:

> Rule out a graph \(G\) on 106 vertices with no \(C_{16}\) and \(\alpha(G)\le7\).

For \(n\ge9\), [b] Nikiforov restricts a possible exception to \(n\le k\le4n+1\), while Keevash–Long–Skokan says only finitely many \(n\) can contribute at all. Their paper does not give a numerical \(C\), so it does not print a finite global list. Extracting a valid explicit \(C\) from their hierarchy of constants is one exact remaining uniformity task; treating the informal “less than 20” remark as a proved constant would be invalid.

3. New from-scratch structural reduction for \(R(C_{16},K_8)\)

Here and below, \(N_G(S)=\bigcup_{v\in S}N_G(v)\).

3.1 Independent-set expansion

[b] Proposition. If a counterexample \(G\) on 106 vertices exists, then every independent set \(S\), \(1\le |S|=s\le7\), satisfies

Proof. Put \(H=G-(S\cup N_G(S))\). An independent set of size \(8-s\) in \(H\), together with \(S\), would have size 8. The solved smaller-clique cases give

for \(1\le8-s\le7\). Since \(H\) is \(C_{16}\)-free,

Therefore

In particular [b] \(\delta(G)\ge15\). The complete checked table is:

| \(s\) | smaller clique \(K_{8-s}\) | maximum \(|H|\) | minimum \(|N_G(S)|\) |

|---:|---:|---:|---:|

| 1 | 7 | 90 | 15 |

| 2 | 6 | 75 | 29 |

| 3 | 5 | 60 | 43 |

| 4 | 4 | 45 | 57 |

| 5 | 3 | 30 | 71 |

| 6 | 2 | 15 | 85 |

| 7 | 1 | 0 | 99 |

3.2 Two-connectivity

[b] Proposition. Every such \(G\) is 2-connected.

Proof. If \(G\) is disconnected with component independence numbers \(a_i\), then \(\sum a_i=\alpha(G)\le7\). There are at least two nonempty components, so every \(a_i\le6\). The solved smaller cases imply

Thus \(|G|\le15\sum a_i\le105\), a contradiction.

Now suppose \(v\) is a cut vertex. Group the components of \(G-v\) into two nonempty anticomplete induced subgraphs \(A,B\), and put \(a=\alpha(A)\), \(b=\alpha(B)\). Then \(a,b\le6\), \(a+b\le7\), and

Equality holds throughout: \(a+b=7\), \(|A|=15a\), and \(|B|=15b\). The \(C_{16}\)-free graph \(G[A\cup\{v\}]\) has \(15a+1=R(C_{16},K_{a+1})\) vertices, so it has an independent set of size \(a+1\). Since \(\alpha(A)=a\), that set contains \(v\) and \(a\) non-neighbours of \(v\) in \(A\). Similarly there are \(b\) such vertices in \(B\). Together with \(v\) they form an independent set of size \(1+a+b=8\), a contradiction. \(\square\)

3.3 Clique and local-path exclusions

[a] Proposition. Such a \(G\) has no \(K_{15}\), so \(\omega(G)\le14\).

Proof. Let \(U\cong K_{15}\). Minimum degree 15 gives every \(u_i\in U\) an external neighbour \(x_i\). No external vertex can be adjacent to two vertices of \(U\): it would close a Hamilton path through all 15 clique vertices into a \(C_{16}\). Thus the \(x_i\) are distinct. If \(x_ix_j\) were an edge for \(i\ne j\), a path from \(u_i\) to \(u_j\) using 14 of the clique vertices, together with \(x_i,x_j\), would be a \(C_{16}\). Hence any eight of the \(x_i\) are independent, again impossible. \(\square\)

[a] For every vertex \(v\), \(G[N(v)]\) has no \(P_{15}\), because \(v\) closes such a path into a \(C_{16}\).

[b] Chvátal's tree–complete Ramsey theorem gives

Since \(G[N(v)]\) contains neither \(P_{15}\) nor an independent set of size 8, \(d(v)\le98\). The first unresolved case has therefore been reduced to the following exact kernel:

together with \(|N(S)|\ge14|S|+1\) for every independent \(S\).

This does not solve the case, but it is a reusable, fully checked reduction derived only from already solved smaller clique parameters.

4. A verifiable arithmetic gap in the published \(4n+2\) proof

This section audits a proof, not the truth of Nikiforov's theorem.

Nikiforov shifts variables and proves \(R(K_{r+1},C_{p+1})=pr+1\) under \(p\ge4r+5\). In Case 4.1 he sets

and establishes

The paper then prints the consecutive bounds

[a] The middle inequality is equivalent to

whereas the established premise is only \(r_1+r_2\le r+1\). The factor of two cannot be removed arithmetically.

[a] Concrete witness to the failed numerical implication. Take the first inductive value \(r=6\), its boundary \(p=4r+5=29\), and values \(r_1=2,r_2=5\), which satisfy both \(r_1\le(r+1)/2\) and \(r_1+r_2\le r+1\). (Unlike \(r_1=1,r_2=6\), this allocation is also compatible with the possibility \(\alpha(B-z)=r_1-1\) and the global bound \(\alpha(G)\le r\).) The two displayed relaxed bounds are

and

Thus the printed step asserts \(37\le30\). These numerical values need not arise from an actual counterexample graph; they prove exactly that the stated premises do not imply the displayed inequality.

The precise structural lemma that would repair this route is

The available estimate \(l_1\le2r_2+1\) would imply it only from the unproved stronger relation \(2(r_1+r_2)\le r+1\).

[a] If one uses only the bounds actually stated in Case 4.1, the worst lower endpoint is at most

This is \(\le p+1\) first when \(p\ge5r+12\); at \(p=5r+11\) it is still \(p+2\). This repairs only that arithmetic line under a weaker parameter range. It is not a verification of the whole proof under the weaker range.

[b] Nikiforov's \(k\ge4n+2\) theorem remains an accepted named result, repeatedly cited by Keevash–Long–Skokan and the 2026 Radziszowski survey. [c] I found no erratum or alternate repair. Therefore I use the theorem for the literature frontier, but I do not claim a new cutoff by modifying this proof. Any such modification first needs either the missing \(l_1+2r_1\) lemma or a different treatment of Case 4.1.

5. Exact computational wall

For the 106-vertex kernel, a direct edge-variable SAT encoding has

Boolean variables. [a] Explicitly forbidding all independent 8-sets requires

clauses. The number of undirected labelled 16-cycles is

Even an unrealistically packed four-byte-per-literal representation would use 9,650,546,848,800 bytes for the independent-set clauses and

bytes for the cycle clauses. [d] At \(10^9\) enumerated cycles per second, merely listing the latter takes about \(7.64\times10^{13}\) single-core years. These are exact encoding counts, not a lower bound on clever algorithms.

A meaningful exact computation would therefore need a lazy SAT/constraint-generation solver with:

1. an exact independent-8 separator (a \(K_8\) finder in the complement);

2. an exact \(C_{16}\) separator;

3. symmetry breaking and the expansion/2-connectivity kernel above;

4. a replayable UNSAT proof or, if satisfiable, an adjacency-list certificate checked independently.

[c] No defensible core-hour estimate exists before a lazy-separation pilot: its iteration count is not controlled by the explicit clause counts. The fully expanded approach has the quantitative cost above and is not runnable on this box; a specialized complete solver, rather than more raw enumeration, is the required computation.

6. Standalone re-verification

File: runs/erdos551_wave5z_reverify.py

SHA-256:

bfcdab1b29317c8a6f12de062cc4e3a1640445d08a56e741f2a52d4bf6349021

Run:

python3 runs/erdos551_wave5z_reverify.py

Measured on this VM:

lower construction: 7 K_15, order=105, alpha=7, C_16-free
q=8 unresolved literature frontier: ell=16..33
independent-set expansion rows (s, 8-s, |H|max, |N(S)|min):
  (1, 7, 90, 15)
  (2, 6, 75, 29)
  (3, 5, 60, 43)
  (4, 4, 45, 57)
  (5, 3, 30, 71)
  (6, 2, 15, 85)
  (7, 1, 0, 99)
first-case kernel: N=106, 2-connected, 15<=delta<=Delta<=98, omega<=14
Nikiforov Case 4.1 arithmetic witness: {'r': 6, 'p': 29, 'first_relaxed_bound': 37, 'claimed_next_bound': 30, 'gap': 7, 'safe_p_using_only_stated_bounds': 42}
naive encoding: {'edge_variables': 5565, 'independent_8_clauses': 301579589025, 'undirected_16_cycle_clauses': 2411044134482636127622667520000, 'packed_independent_clause_bytes': 9650546848800, 'packed_cycle_clause_bytes': 154306824606888712167850721280000, 'cycle_enumeration_years_at_1e9_per_second': 76401378256985.19}
ALL CHECKS PASSED

Runtime was 0.03 seconds with 12,564 KiB maximum RSS.

The complete checker source follows.

#!/usr/bin/env python3
"""Offline arithmetic/structural checks for runs/erdos551_wave5z.md.

This script does not assume or prove the open Ramsey conjecture.  Its imported
mathematical inputs are stated explicitly below.  Everything downstream of
those inputs is checked with Python's standard library.

Imported named results:
  (I1) R(C_ell, K_m) = (ell-1)(m-1)+1 for ell=16 and 1 <= m <= 7.
  (I2) R(C_ell, K_8) = 7(ell-1)+1 for 8 <= ell <= 15.
  (I3) Nikiforov's accepted theorem covers ell >= 4m+2.
"""

from __future__ import annotations

from fractions import Fraction
from math import comb, factorial


ELL = 16
Q = 8
TARGET_N = (ELL - 1) * (Q - 1) + 1


def ramsey_conjectured(ell: int, clique_order: int) -> int:
    return (ell - 1) * (clique_order - 1) + 1


def connected_components(adjacency: list[set[int]]) -> list[list[int]]:
    unseen = set(range(len(adjacency)))
    answer: list[list[int]] = []
    while unseen:
        root = min(unseen)
        unseen.remove(root)
        stack = [root]
        component: list[int] = []
        while stack:
            vertex = stack.pop()
            component.append(vertex)
            new = adjacency[vertex] & unseen
            unseen.difference_update(new)
            stack.extend(new)
        answer.append(sorted(component))
    return sorted(answer, key=lambda component: component[0])


def build_cluster_lower_bound(
    number_of_clusters: int, cluster_size: int
) -> list[set[int]]:
    order = number_of_clusters * cluster_size
    adjacency = [set() for _ in range(order)]
    for cluster in range(number_of_clusters):
        vertices = range(cluster * cluster_size, (cluster + 1) * cluster_size)
        for u in vertices:
            for v in vertices:
                if u != v:
                    adjacency[u].add(v)
    return adjacency


def check_lower_bound_construction() -> None:
    """Check 7 K_15 on 105 vertices without a generic exponential search."""
    adjacency = build_cluster_lower_bound(7, 15)
    assert len(adjacency) == TARGET_N - 1 == 105
    components = connected_components(adjacency)
    assert [len(component) for component in components] == [15] * 7

    for component in components:
        component_set = set(component)
        for vertex in component:
            assert adjacency[vertex] == component_set - {vertex}

    assert max(map(len, components)) < ELL

    witness = [component[0] for component in components]
    assert len(witness) == 7
    assert all(v not in adjacency[u] for i, u in enumerate(witness) for v in witness[i + 1 :])
    alpha = len(components)
    assert alpha == 7 < Q


def check_q8_frontier() -> list[int]:
    """Check the arithmetic frontier implied by imported results I2 and I3."""
    solved_small = list(range(8, 16))
    nikiforov_start = 4 * Q + 2
    unresolved = list(range(max(solved_small) + 1, nikiforov_start))
    assert nikiforov_start == 34
    assert unresolved == list(range(16, 34))
    assert len(unresolved) == 18
    assert ramsey_conjectured(16, 8) == 106
    assert ramsey_conjectured(33, 8) == 225
    return unresolved


def check_first_case_expansion() -> list[tuple[int, int, int, int]]:
    rows: list[tuple[int, int, int, int]] = []
    for s in range(1, 8):
        smaller_clique = Q - s
        h_max = ramsey_conjectured(ELL, smaller_clique) - 1
        neighborhood_min = TARGET_N - s - h_max
        assert h_max == 15 * (7 - s)
        assert neighborhood_min == 14 * s + 1
        rows.append((s, smaller_clique, h_max, neighborhood_min))
    assert rows[0][-1] == ELL - 1 == 15
    return rows


def check_connectivity_reduction() -> None:
    disconnected_caps = []
    cutvertex_equality_cases = []
    for a in range(1, 7):
        for b in range(1, 7):
            if a + b <= 7:
                disconnected_caps.append(15 * (a + b))
                cut_cap = 1 + 15 * (a + b)
                if cut_cap == TARGET_N:
                    cutvertex_equality_cases.append((a, b))
                    assert 1 + a + b == 8

    assert disconnected_caps
    assert max(disconnected_caps) == 105 < TARGET_N
    assert cutvertex_equality_cases == [
        (1, 6),
        (2, 5),
        (3, 4),
        (4, 3),
        (5, 2),
        (6, 1),
    ]


def clique_path(
    clique_vertices: list[int], start: int, end: int, number_used: int
) -> list[int]:
    assert start != end
    assert start in clique_vertices and end in clique_vertices
    middle = [v for v in clique_vertices if v not in {start, end}]
    path = [start] + middle[: number_used - 2] + [end]
    assert len(path) == number_used
    assert len(set(path)) == number_used
    return path


def check_no_k15_argument() -> None:
    clique = list(range(15))
    outside_x, outside_y = 15, 16

    path15 = clique_path(clique, 0, 1, 15)
    cycle_from_common_neighbor = [outside_x] + path15
    assert len(cycle_from_common_neighbor) == ELL
    assert len(set(cycle_from_common_neighbor)) == ELL

    path14 = clique_path(clique, 0, 1, 14)
    cycle_from_adjacent_private_neighbors = [outside_x] + path14 + [outside_y]
    assert len(cycle_from_adjacent_private_neighbors) == ELL
    assert len(set(cycle_from_adjacent_private_neighbors)) == ELL


def check_local_path_and_degree_bound() -> None:
    center = 15
    path_vertices = list(range(15))
    resulting_cycle = [center] + path_vertices
    assert len(resulting_cycle) == ELL
    assert len(set(resulting_cycle)) == ELL

    r_path15_k8 = (15 - 1) * (8 - 1) + 1
    assert r_path15_k8 == 99
    maximum_degree = r_path15_k8 - 1
    assert maximum_degree == 98


def nikiforov_relaxed_bounds(
    p: int, r: int, r1: int, r2: int
) -> tuple[Fraction, Fraction]:
    first = (
        Fraction(p + 2 * r1 + 2 * r2 + 5)
        - Fraction(p - r - 1, 2)
    )
    second = Fraction(p + r + 6) - Fraction(p - r - 1, 2)
    return first, second


def nikiforov_exact_worst_endpoint(p: int, r: int) -> int:
    return p + 2 * r + 7 - ((p - r) // 2)


def check_nikiforov_case_4_1_arithmetic() -> dict[str, int]:
    r = 6
    p = 4 * r + 5
    r1, r2 = 2, r - 1
    d = p - r

    assert p == 29 and d == 23
    assert r1 <= (r + 1) / 2
    assert r1 + r2 <= r + 1

    first, second = nikiforov_relaxed_bounds(p, r, r1, r2)
    assert first == 37
    assert second == p + 1 == 30
    assert first > second
    assert first - second == r + 1
    assert not (2 * (r1 + r2) <= r + 1)

    for test_r in range(6, 101):
        test_p = 4 * test_r + 5
        test_first, test_second = nikiforov_relaxed_bounds(
            test_p, test_r, 2, test_r - 1
        )
        assert test_first - test_second == test_r + 1

        repaired_p = 5 * test_r + 12
        assert nikiforov_exact_worst_endpoint(repaired_p, test_r) <= repaired_p + 1
        previous_p = repaired_p - 1
        assert nikiforov_exact_worst_endpoint(previous_p, test_r) > previous_p + 1

    return {
        "r": r,
        "p": p,
        "first_relaxed_bound": int(first),
        "claimed_next_bound": int(second),
        "gap": int(first - second),
        "safe_p_using_only_stated_bounds": 5 * r + 12,
    }


def check_naive_encoding_size() -> dict[str, int | float]:
    edge_variables = comb(TARGET_N, 2)
    independent_8_subsets = comb(TARGET_N, 8)
    undirected_16_cycles = (
        factorial(TARGET_N)
        // factorial(TARGET_N - ELL)
        // (2 * ELL)
    )

    assert edge_variables == 5_565
    assert independent_8_subsets == 301_579_589_025
    assert (
        undirected_16_cycles
        == 2_411_044_134_482_636_127_622_667_520_000
    )

    independent_clause_bytes = independent_8_subsets * 8 * 4
    cycle_clause_bytes = undirected_16_cycles * ELL * 4
    seconds_at_billion_cycles_per_second = undirected_16_cycles / 1_000_000_000
    years_at_billion_cycles_per_second = (
        seconds_at_billion_cycles_per_second / (365.25 * 24 * 60 * 60)
    )

    assert independent_clause_bytes == 9_650_546_848_800
    assert (
        cycle_clause_bytes
        == 154_306_824_606_888_712_167_850_721_280_000
    )

    return {
        "edge_variables": edge_variables,
        "independent_8_clauses": independent_8_subsets,
        "undirected_16_cycle_clauses": undirected_16_cycles,
        "packed_independent_clause_bytes": independent_clause_bytes,
        "packed_cycle_clause_bytes": cycle_clause_bytes,
        "cycle_enumeration_years_at_1e9_per_second": years_at_billion_cycles_per_second,
    }


def main() -> None:
    assert TARGET_N == 106
    check_lower_bound_construction()
    unresolved = check_q8_frontier()
    expansion = check_first_case_expansion()
    check_connectivity_reduction()
    check_no_k15_argument()
    check_local_path_and_degree_bound()
    proof_gap = check_nikiforov_case_4_1_arithmetic()
    encoding = check_naive_encoding_size()

    print("lower construction: 7 K_15, order=105, alpha=7, C_16-free")
    print(f"q=8 unresolved literature frontier: ell={unresolved[0]}..{unresolved[-1]}")
    print("independent-set expansion rows (s, 8-s, |H|max, |N(S)|min):")
    for row in expansion:
        print(" ", row)
    print("first-case kernel: N=106, 2-connected, 15<=delta<=Delta<=98, omega<=14")
    print("Nikiforov Case 4.1 arithmetic witness:", proof_gap)
    print("naive encoding:", encoding)
    print("ALL CHECKS PASSED")


if __name__ == "__main__":
    main()

PARTIAL: The first located open case is reduced to an explicit 106-vertex 2-connected kernel with verified expansion/degree/clique constraints, and Nikiforov Case 4.1 has a reproducible factor-two proof gap; neither the case nor problem 551 is resolved.