\(F(n,\alpha)/\log n\) to its reciprocal. Conversely,

If \(F(n,\alpha)\sim c_\alpha\log n\), evaluating along these two sequences

squeezes \(\log R_\alpha(k)/k\) to \(1/c_\alpha\). (a)

At \(\alpha=0\), an \(\alpha\)-bad set is precisely a clique or an

independent set, hence

Thus even the \(\alpha=0\) case of #563 is equivalent to existence of the

exponential growth base of the diagonal Ramsey numbers. The separately

listed Erdős problem #77 was checked

live through Bright Data on 2026-07-27 and is still OPEN; it asks for

exactly \(\lim_kR(k,k)^{1/k}\). (a)/(d)

This is the principal asymptotic wall: a proof of #563 as printed would, in

particular, settle the existence part of #77. It is not merely a need to

improve constants in the routine probabilistic argument.

2. Exact finite theorem: \(R_\alpha(4)\) for every \(\alpha\)

Theorem

For \(0\leq\alpha<1/2\),

The middle and high regimes are elementary-rigorous (a). The first

regime is rigorous modulo the classical theorem \(R(4,4)=18\) of Greenwood

and Gleason (b); the checker independently verifies their 17-vertex

lower-bound construction.

Regime \(0\leq\alpha<1/6\)

On four vertices there are six edges. Because \(6\alpha<1\), “more than

\(6\alpha\) edges of each colour” is equivalent to at least one edge of

each colour. Thus a good colouring is exactly one with no monochromatic

\(K_4\), and

Greenwood and Gleason proved the exact value in

[“Combinatorial Relations and Chromatic Graphs,” *Canadian Journal of

Mathematics* 7 (1955), 1–7](https://doi.org/10.4153/CJM-1955-001-4).

(b)

For the lower bound, their graph can be taken as the Paley graph on

\(\mathbb F_{17}\): join \(x,y\) when \(x-y\) is a nonzero quadratic

residue. The checker examines all \(\binom{17}{4}=2380\) four-sets and

finds between one and five edges in each, so neither colour has a \(K_4\).

(d)

Regime \(1/6\leq\alpha<1/3\)

Here \(1\leq6\alpha<2\), so a four-set is good exactly when it contains

\(2,3,\) or \(4\) edges of \(G\).

Nine-vertex construction. Let the vertices be the nine cells of a

\(3\times3\) board, adjacent when they share a row or a column (the rook

graph). For any four cells,

Four cells distributed over three rows force at least one row pair, and

similarly force at least one column pair, so \(e\geq2\). If a row contains

three cells, they occupy all three columns and the fourth cell makes the

column contribution exactly one, giving \(e=4\). If no row or column

contains three cells, each of the two sums in (7) is at most two. Thus

\(2\leq e\leq4\). (a)

No ten-vertex construction. Suppose every four-set in a graph \(G\)

has between two and four edges. Fix a vertex \(v\), and write

For every triple \(T\subseteq A\), the set \(T\cup\{v\}\) already has the

three edges from \(v\), so \(e_G(T)\leq1\). Hence \(G[A]\) has maximum

degree at most one: it is a matching plus isolated vertices. If

\(|A|\geq5\), four vertices can be selected spanning at most one matching

edge, contrary to the assumed lower bound two. Thus \(|A|\leq4\).

For every triple \(T\subseteq B\), the set \(T\cup\{v\}\) has no edges

from \(v\), so \(e_G(T)\geq2\). Equivalently,

\(\overline G[B]\) has maximum degree at most one. If \(|B|\geq5\), some

four vertices have at most one nonedge, hence at least five edges of

\(G\), contrary to the upper bound four. Thus \(|B|\leq4\). Therefore

Together with the rook graph, this proves \(R_\alpha(4)=10\). (a)

Regime \(1/3\leq\alpha<1/2\)

Now \(2\leq6\alpha<3\), so each colour must occur at least three times on

every four-set. Every four-set must therefore have exactly three edges of

\(G\).

The cycle \(C_5\) is a five-vertex construction: deleting any vertex leaves

a three-edge path. Conversely, in any graph with the property, every

five-set \(U\) has

so \(e(U)=5\). If six vertices existed, summing over their six five-sets

would give

an integer contradiction. Hence the maximum order is five and

\(R_\alpha(4)=6\). (a)

Consequences for the first nontrivial values of \(F\)

The same elementary argument gives

For the first regime this is \(R(3,3)=6\), with \(C_5\) as the

five-vertex construction; in the second regime two colour counts both

strictly larger than \(3\alpha\geq1\) would sum to at least four although a

triangle has only three edges. (a)

Equations (3), (6), and (8) give:

| \(\alpha\) | exact range determined by \(m=3,4\) |

|---|---|

| \(0\leq\alpha<1/6\) | \(F(n,\alpha)=3\) for \(3\leq n\leq5\); \(F(n,\alpha)=4\) for \(6\leq n\leq17\); \(F(n,\alpha)\geq5\) for \(n\geq18\) |

| \(1/6\leq\alpha<1/3\) | \(F(n,\alpha)=3\) for \(3\leq n\leq5\); \(F(n,\alpha)=4\) for \(6\leq n\leq9\); \(F(n,\alpha)\geq5\) for \(n\geq10\) |

| \(1/3\leq\alpha<1/2\) | \(F(n,\alpha)=4\) for \(3\leq n\leq5\); \(F(n,\alpha)\geq5\) for \(n\geq6\) |

The endpoints are important because the live statement uses the strict

word “more than.”

3. Complete exact computation through seven vertices

For fixed \(n,m\), define the integer

By the averaging lemma, an \(n\)-vertex colouring works at threshold \(m\)

if and only if

The standalone checker exhausts all labelled graphs for every

\(3\leq m\leq n\leq7\), taking one graph from each complementary pair.

The largest search is \(2^{20}=1,048,576\) representatives at \(n=7\).

It uses exact integer arithmetic and no graph package. A second naive

implementation, with no complement reduction or pruning, independently

recomputes all entries through \(n=6\). (d)

Each cell below is \(q(n,m)\), followed in parentheses by the density

\(q(n,m)/\binom m2\).

| \(n\backslash m\) | 3 | 4 | 5 | 6 | 7 |

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

| 3 | \(1\;(1/3)\) | — | — | — | — |

| 4 | \(1\;(1/3)\) | \(3\;(1/2)\) | — | — | — |

| 5 | \(1\;(1/3)\) | \(3\;(1/2)\) | \(5\;(1/2)\) | — | — |

| 6 | \(0\) | \(2\;(1/3)\) | \(4\;(2/5)\) | \(7\;(7/15)\) | — |

| 7 | \(0\) | \(2\;(1/3)\) | \(4\;(2/5)\) | \(7\;(7/15)\) | \(10\;(10/21)\) |

This gives the complete piecewise values: (d)

Values \(n+1\) are legitimate: if even the full vertex set cannot be

balanced strictly enough, \(m=n+1\) is the first vacuous threshold.

The checker prints a hexadecimal witness and its full edge set for every

entry, then directly checks the original “all sizes \(\geq m\)” condition.

4. A quantitative version of the easy random upper bound

Let

with \(0\log0=0\). Then for every fixed \(0\leq\alpha<1/2\),

This refines the order-of-magnitude upper bound listed on the live page.

(b), using the standard binomial Chernoff bound

To verify it, colour every edge independently and fairly. For a fixed

\(m\)-set, Chernoff and symmetry give

Hence the expected number of bad \(m\)-sets is at most

Put \(L=\log n\), \(a=2/D_\alpha\), and

Using \(\binom nm\leq(en/m)^m\), the logarithm of (14) is at most

Choose \(C>1+1/a-\log a\). The expectation tends to zero, so some

colouring has no bad \(m\)-set; the averaging lemma then excludes bad

larger sets as well. (b)

Balister, Bollobás, Sahasrabudhe, and Veremyev prove a much sharper

two-point concentration theorem for the largest quasi-clique in

“Dense Subgraphs in Random Graphs,” arXiv:1803.10349.

Specialising their theorem to \(p=1/2\), \(\gamma=1-\alpha\), and applying

it to both \(G\) and \(\overline G\) gives the same expression as (13), with

an explicit bounded term. This controls the random construction; it does

not supply the minimax lower bound or the missing limit in (4). (b)

5. Primary-source and literature audit

1. Crossref/Springer verify Paul Erdős,

[“Problems and Results on Graphs and Hypergraphs: Similarities and

Differences”](https://doi.org/10.1007/978-3-642-72905-8_2),

Mathematics of Ramsey Theory (1990), pp. 12–28. Google Books OCR for

p. 21 independently exposes the phrases “smallest integer” and “every

class contains more than,” matching the live strict definition. (b)

2. The page's hypergraph pointer is consistent with Conlon, Fox, and

Sudakov,

[“Large almost monochromatic subsets in hypergraphs,”

arXiv:0901.3912](https://arxiv.org/abs/0901.3912). Their theorem concerns

3-uniform hypergraphs and a \(\Theta(\sqrt{\log N})\)-scale

almost-monochromatic subset, not the existence of the graph limit in

(4). (b)

3. The modern diagonal-Ramsey papers improve upper bounds without proving

an exponential base. In particular, Gupta, Ndiaye, Norin, and Wei state

\(R(k,k)\leq(3.8)^{k+o(k)}\) in

arXiv:2407.19026; the live #77 page

still lists the limit itself as open. (b)/(d)

4. Exact-phrase searches for the displayed \(F(n,\alpha)\) formulation,

searches under “quasi-clique/quasi-independent set” and “induced

density Ramsey,” and a forward-citation scan of the 1990 chapter found

no primary paper claiming the limit in (4). This is a search miss, not

a proof that no relevant paper exists. The closest directly useful

result found was the random quasi-clique theorem above. (d)

The checker's optional --sources mode re-fetches the two DOI records,

Google Books p. 21 OCR, and the TeX source of arXiv:1803.10349,

arXiv:2407.19026, and arXiv:0901.3912, and asserts the exact phrases used

here.

6. Precise wall and what would be needed

The exact missing assertion is

Once (16) is proved, (3) gives the desired result with

\(c_\alpha=1/\lambda_\alpha\). At \(\alpha=0\), (16) is exactly the still

open diagonal Ramsey limit. (a)/(d)

A sufficient product lemma would be an almost-supermultiplicative estimate

of the shape

with a uniform error suitable for an approximate Fekete lemma. No such

fixed-\(\alpha\), additive-parameter inequality was found. (c)

The usual lexicographic product does not provide it. Already at

\(\alpha=0\), composing colourings only yields

whose clique-size parameter is multiplicative rather than additive. It

does not imply convergence of \(\log R_0(k)/k\). For \(\alpha>0\), the

density of a subset in a lexicographic product also depends on how its

vertices are distributed among blocks, so even the density parameter is

not preserved without loss. This identifies the exact place where the

standard product/Fekete machinery stalls. (a)

Finite computation cannot bridge this uniformity gap. The pure labelled

enumerator would need \(2^{27}=134{,}217{,}728\) complementary

representatives for \(n=8\), estimated from the measured run at roughly

0.2–0.4 core-hours, and \(2^{35}=34{,}359{,}738{,}368\) representatives

for \(n=9\), roughly 50–120 core-hours before allowing for the larger

subset family. Those runs were not attempted. Isomorph-free generation or

SAT can make individual finite cases much cheaper, but no finite table can

establish (16). (d)

7. Reproduction

Standalone checker:

SHA-256:

Commands actually run:

python3 -m py_compile runs/erdos563_wave6c_reverify.py
/usr/bin/time -f 'wall=%E cpu=%P maxrss=%MKB' \
  python3 runs/erdos563_wave6c_reverify.py --sources

Final output lines:

Naive all-graph cross-check passed through n=6.
R_alpha(4) ingredients: C5, 3x3 rook graph, local n<=9 obstruction, six-vertex obstruction, and Paley(17) all checked
ALL EXACT CHECKS PASSED in 5.50 seconds
PRIMARY-SOURCE TEXT/METADATA CHECKS PASSED
wall=0:06.69 cpu=84% maxrss=26460KB

8. Complete checker source

The full source is reproduced below and also exists as the standalone file

named above.

#!/usr/bin/env python3
"""From-scratch exact checks for Erdős problem #563.

For an n-vertex graph G and an m-set X, put

    balance_G(X) = min(e_G(X), C(m,2) - e_G(X)).

This script exhausts all labelled graphs (one graph from each complementary
pair) for 3 <= n <= 7 and computes

    q(n,m) = max_G min_{|X|=m} balance_G(X).

Thus the best possible minimum minority-colour density on every m-set is
q(n,m)/C(m,2).  Only the Python standard library and exact integer arithmetic
are used.  The 2^21 labelled graphs at n=7 make this a finite, reproducible
check rather than an asymptotic claim.
"""

from __future__ import annotations

import argparse
import gzip
import io
import json
import tarfile
import urllib.parse
import urllib.request
from dataclasses import dataclass
from fractions import Fraction
from itertools import combinations
from math import comb
from time import perf_counter


EXPECTED_Q = {
    3: {3: 1},
    4: {3: 1, 4: 3},
    5: {3: 1, 4: 3, 5: 5},
    6: {3: 0, 4: 2, 5: 4, 6: 7},
    7: {3: 0, 4: 2, 5: 4, 6: 7, 7: 10},
}


@dataclass(frozen=True)
class Extremum:
    n: int
    m: int
    q: int
    witness: int
    graphs_checked: int

    @property
    def density(self) -> Fraction:
        return Fraction(self.q, comb(self.m, 2))


def edge_index_data(n: int) -> tuple[list[tuple[int, int]], dict[tuple[int, int], int]]:
    edges = list(combinations(range(n), 2))
    return edges, {edge: index for index, edge in enumerate(edges)}


def induced_edge_masks(n: int, m: int) -> list[int]:
    """Return the edge-bit mask of every m-subset of [n]."""
    _edges, edge_index = edge_index_data(n)
    masks: list[int] = []
    for vertices in combinations(range(n), m):
        mask = 0
        for edge in combinations(vertices, 2):
            mask |= 1 << edge_index[edge]
        masks.append(mask)
    assert len(masks) == comb(n, m)
    assert all(mask.bit_count() == comb(m, 2) for mask in masks)
    return masks


def graph_score(graph: int, subset_edge_masks: list[int], edges_per_subset: int) -> int:
    """Minimum minority-colour edge count over the supplied equal-size subsets."""
    score = edges_per_subset // 2
    for subset_edges in subset_edge_masks:
        red = (graph & subset_edges).bit_count()
        score = min(score, red, edges_per_subset - red)
    return score


def exact_extremum(n: int, m: int) -> Extremum:
    """Exhaust complementary pairs of labelled n-vertex graphs exactly."""
    assert 3 <= m <= n <= 7
    edge_count = comb(n, 2)
    subset_masks = induced_edge_masks(n, m)
    subset_edge_count = comb(m, 2)

    # balance_G(X) is unchanged when every edge colour is swapped.  Exactly
    # one member of each complementary pair has the final edge bit equal to 0.
    graph_limit = 1 << (edge_count - 1)
    best = -1
    witness = -1

    for graph in range(graph_limit):
        # Once a subset has balance <= best this graph cannot improve best.
        score = subset_edge_count // 2
        for subset_edges in subset_masks:
            red = (graph & subset_edges).bit_count()
            balance = min(red, subset_edge_count - red)
            if balance <= best:
                score = balance
                break
            if balance < score:
                score = balance
        if score > best:
            # Recompute without the early-improvement shortcut before storing.
            score = graph_score(graph, subset_masks, subset_edge_count)
            if score > best:
                best = score
                witness = graph

    result = Extremum(n, m, best, witness, graph_limit)
    assert graph_score(witness, subset_masks, subset_edge_count) == best
    return result


def naive_extremum(n: int, m: int) -> int:
    """Second implementation: all graphs, no complement reduction or pruning."""
    subset_masks = induced_edge_masks(n, m)
    subset_edge_count = comb(m, 2)
    return max(
        graph_score(graph, subset_masks, subset_edge_count)
        for graph in range(1 << comb(n, 2))
    )


def witness_edges(n: int, graph: int) -> tuple[tuple[int, int], ...]:
    edges, _edge_index = edge_index_data(n)
    return tuple(edge for index, edge in enumerate(edges) if graph & (1 << index))


def graph_from_edges(n: int, selected: set[tuple[int, int]]) -> int:
    edges, edge_index = edge_index_data(n)
    normalized = {tuple(sorted(edge)) for edge in selected}
    assert normalized <= set(edges)
    return sum(1 << edge_index[edge] for edge in normalized)


def cycle_graph_5() -> int:
    return graph_from_edges(5, {tuple(sorted((v, (v + 1) % 5))) for v in range(5)})


def rook_graph_3_by_3() -> int:
    """The 9-vertex graph joining cells in a common row or common column."""
    selected: set[tuple[int, int]] = set()
    for u, v in combinations(range(9), 2):
        row_u, col_u = divmod(u, 3)
        row_v, col_v = divmod(v, 3)
        if row_u == row_v or col_u == col_v:
            selected.add((u, v))
    return graph_from_edges(9, selected)


def paley_graph_17() -> int:
    """The Greenwood--Gleason 17-vertex Ramsey graph."""
    squares = {x * x % 17 for x in range(1, 17)}
    selected = {
        (u, v)
        for u, v in combinations(range(17), 2)
        if (u - v) % 17 in squares
    }
    return graph_from_edges(17, selected)


def property_on_all_sizes(n: int, m: int, alpha: Fraction, graph: int) -> bool:
    """Directly check the live page's condition on every subset of size >= m."""
    for size in range(m, n + 1):
        total = comb(size, 2)
        for subset_edges in induced_edge_masks(n, size):
            red = (graph & subset_edges).bit_count()
            blue = total - red
            if not (red > alpha * total and blue > alpha * total):
                return False
    return True


def property_on_m_sets(n: int, m: int, alpha: Fraction, graph: int) -> bool:
    """Check only m-sets, the equivalent finite condition used in the search."""
    total = comb(m, 2)
    return all(
        min((graph & subset_edges).bit_count(), total - (graph & subset_edges).bit_count())
        > alpha * total
        for subset_edges in induced_edge_masks(n, m)
    )


def f_from_extrema(n: int, alpha: Fraction, row: dict[int, Extremum]) -> int:
    """Recover F(n,alpha); m=n+1 always works vacuously."""
    assert Fraction(0) <= alpha < Fraction(1, 2)
    for m in range(3, n + 1):
        if row[m].density > alpha:
            return m
    return n + 1


def check_subset_averaging_equivalence(max_n: int = 5) -> None:
    """Finite audit that checking m-sets suffices (the report proves it)."""
    for n in range(3, max_n + 1):
        edge_count = comb(n, 2)
        critical = {Fraction(0), Fraction(1, 2)}
        for size in range(3, n + 1):
            total = comb(size, 2)
            critical.update(Fraction(q, total) for q in range(total // 2 + 1))
        ordered = sorted(critical)
        alphas = {value for value in ordered if value < Fraction(1, 2)}
        alphas.update(
            (left + right) / 2
            for left, right in zip(ordered, ordered[1:])
            if left < Fraction(1, 2)
        )
        for graph in range(1 << edge_count):
            for m in range(3, n + 1):
                for alpha in alphas:
                    assert property_on_m_sets(n, m, alpha, graph) == property_on_all_sizes(
                        n, m, alpha, graph
                    )


def check_exact_r_alpha_4_constructions_and_obstructions() -> None:
    """Audit the ingredients of the exact piecewise value of R_alpha(4)."""
    # For 1/3 <= alpha < 1/2, C5 has exactly three edges on every four-set.
    c5 = cycle_graph_5()
    c5_counts = [
        (c5 & subset_edges).bit_count() for subset_edges in induced_edge_masks(5, 4)
    ]
    assert c5_counts == [3] * 5

    # For 1/6 <= alpha < 1/3, the 3-by-3 rook graph has 2..4 edges
    # on every four-set (and hence at least two edges of each colour).
    rook = rook_graph_3_by_3()
    rook_counts = [
        (rook & subset_edges).bit_count() for subset_edges in induced_edge_masks(9, 4)
    ]
    assert min(rook_counts) == 2
    assert max(rook_counts) == 4
    assert {2, 3, 4} == set(rook_counts)

    # The local upper-bound lemma used for n <= 9: every graph of maximum
    # degree at most one on at least five vertices has a four-set with <=1 edge.
    for graph in range(1 << comb(5, 2)):
        degrees = [0] * 5
        edges, _edge_index = edge_index_data(5)
        for index, (u, v) in enumerate(edges):
            if graph & (1 << index):
                degrees[u] += 1
                degrees[v] += 1
        if max(degrees) <= 1:
            assert min(
                (graph & subset_edges).bit_count()
                for subset_edges in induced_edge_masks(5, 4)
            ) <= 1

    # The high-alpha six-vertex obstruction can also be checked directly:
    # no graph has exactly three edges on every four-set.
    assert not any(
        all(
            (graph & subset_edges).bit_count() == 3
            for subset_edges in induced_edge_masks(6, 4)
        )
        for graph in range(1 << comb(6, 2))
    )

    # For 0 <= alpha < 1/6, the Paley graph on F_17 has neither a K4 nor
    # an independent four-set.  The matching upper bound R(4,4) <= 18 is
    # the named Greenwood--Gleason theorem, not a computational claim here.
    paley = paley_graph_17()
    paley_counts = [
        (paley & subset_edges).bit_count() for subset_edges in induced_edge_masks(17, 4)
    ]
    assert min(paley_counts) >= 1
    assert max(paley_counts) <= 5

    print(
        "R_alpha(4) ingredients: C5, 3x3 rook graph, local n<=9 "
        "obstruction, six-vertex obstruction, and Paley(17) all checked"
    )


def fetch(url: str) -> bytes:
    request = urllib.request.Request(
        url, headers={"User-Agent": "erdos563-wave6c-source-check/1.0"}
    )
    with urllib.request.urlopen(request, timeout=60) as response:
        return response.read()


def arxiv_source_text(arxiv_id: str) -> str:
    """Fetch and concatenate TeX/BibTeX files from an arXiv source bundle."""
    payload = fetch(f"https://export.arxiv.org/e-print/{arxiv_id}")
    try:
        with tarfile.open(fileobj=io.BytesIO(payload), mode="r:gz") as archive:
            chunks: list[str] = []
            for member in archive.getmembers():
                if member.isfile() and member.name.endswith((".tex", ".bbl")):
                    extracted = archive.extractfile(member)
                    assert extracted is not None
                    chunks.append(extracted.read().decode("utf-8", errors="replace"))
            assert chunks
            return "\n".join(chunks)
    except tarfile.ReadError:
        return gzip.decompress(payload).decode("utf-8", errors="replace")


def check_primary_sources() -> None:
    """Re-fetch machine-checkable metadata/text used in the literature audit."""
    crossref_expectations = (
        (
            "10.1007/978-3-642-72905-8_2",
            "Problems and Results on Graphs and Hypergraphs: "
            "Similarities and Differences",
            1990,
        ),
        (
            "10.4153/CJM-1955-001-4",
            "Combinatorial Relations and Chromatic Graphs",
            1955,
        ),
    )
    for doi, title, year in crossref_expectations:
        encoded_doi = urllib.parse.quote(doi, safe="")
        record = json.loads(
            fetch(f"https://api.crossref.org/works/{encoded_doi}").decode("utf-8")
        )["message"]
        assert record["title"][0] == title
        assert record["published"]["date-parts"][0][0] == year

    # Google Books exposes OCR search snippets from p. 21 of the original
    # chapter.  This verifies the strict "more than" definition at the source.
    params = urllib.parse.urlencode(
        {
            "jscmd": "SearchWithinVolume2",
            "q": "smallest integer",
            "vid": "kDPzCAAAQBAJ",
        }
    )
    search_data = json.loads(
        fetch(f"https://books.google.com/books?{params}").decode("latin-1")
    )
    page_21 = [
        item
        for item in search_data["search_results"]
        if item.get("page_id") == "PA21"
    ]
    assert len(page_21) == 1
    assert "every class contains more than" in page_21[0]["snippet_text"]

    random_quasicliques = arxiv_source_text("1803.10349")
    assert "Dense Subgraphs in Random Graphs" in random_quasicliques
    assert "concentrated on a set of two integers" in random_quasicliques
    assert r"\log n-\log\log n" in random_quasicliques

    diagonal_upper = arxiv_source_text("2407.19026")
    assert "Optimizing the CGMS upper bound on Ramsey numbers" in diagonal_upper
    assert r"R(k,k) \leq (3.8)^{k+o(k)}" in diagonal_upper

    hypergraph_generalization = arxiv_source_text("0901.3912")
    assert "Large almost monochromatic subsets in hypergraphs" in hypergraph_generalization
    assert r"s=c\sqrt{\log N}" in hypergraph_generalization

    print("PRIMARY-SOURCE TEXT/METADATA CHECKS PASSED")


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument(
        "--sources",
        action="store_true",
        help="also re-fetch and machine-check cited primary-source text/metadata",
    )
    args = parser.parse_args()
    started = perf_counter()
    table: dict[int, dict[int, Extremum]] = {}

    for n in range(3, 8):
        table[n] = {}
        for m in range(3, n + 1):
            result = exact_extremum(n, m)
            table[n][m] = result
            print(
                f"n={n} m={m}: q={result.q}, "
                f"density={result.density}, witness=0x{result.witness:x}, "
                f"complement-pair reps={result.graphs_checked}"
            )

    observed_q = {
        n: {m: result.q for m, result in row.items()} for n, row in table.items()
    }
    assert observed_q == EXPECTED_Q
    for n in range(3, 7):
        for m in range(3, n + 1):
            assert naive_extremum(n, m) == observed_q[n][m]
    print("Naive all-graph cross-check passed through n=6.")

    print("\nExact q(n,m) rows (m=3,...,n):")
    for n, row in table.items():
        print(f"n={n}: " + " ".join(str(row[m].q) for m in range(3, n + 1)))

    print("\nWitness edge sets:")
    for n, row in table.items():
        for m, result in row.items():
            print(f"(n,m)=({n},{m}): {witness_edges(n, result.witness)}")

    sample_alphas = (
        Fraction(0),
        Fraction(1, 10),
        Fraction(1, 6),
        Fraction(1, 4),
        Fraction(1, 3),
        Fraction(2, 5),
        Fraction(49, 100),
    )
    print("\nF(n,alpha) recovered from the exact extrema:")
    print("alpha\t" + "\t".join(f"n={n}" for n in table))
    for alpha in sample_alphas:
        values = [f_from_extrema(n, alpha, table[n]) for n in table]
        print(f"{alpha}\t" + "\t".join(map(str, values)))

    # Every maximizing witness must satisfy the original all-sizes condition
    # precisely for alpha below its certified m-set density.
    for n, row in table.items():
        for m, result in row.items():
            if result.q:
                alpha = Fraction(result.q, comb(m, 2)) - Fraction(1, 10_000)
                assert property_on_m_sets(n, m, alpha, result.witness)
                assert property_on_all_sizes(n, m, alpha, result.witness)

    check_exact_r_alpha_4_constructions_and_obstructions()

    # This audit is intentionally bounded at n=5; the mathematical equivalence
    # itself is proved for all n by averaging in the report.
    print("\nChecking m-set/all-larger-set equivalence through n=5...")
    check_subset_averaging_equivalence(max_n=5)

    elapsed = perf_counter() - started
    print(f"ALL EXACT CHECKS PASSED in {elapsed:.2f} seconds")
    if args.sources:
        check_primary_sources()


if __name__ == "__main__":
    main()

PARTIAL: Proved the exact piecewise formula R_alpha(4)=18,10,6, computed the complete n<=7 extremal table, and reduced the asymptotic question to existence of lim_k log R_alpha(k)/k, whose alpha=0 case is the open diagonal Ramsey limit.