Erdoes #548 - working report - Erdős Problem a Day

Erdős problem 548 — wave9q report

Date: 2026-07-28 UTC

Artifacts:

Standalone verifier:

runs/erdos548_wave9q_reverify.py

This report: runs/erdos548_wave9q.md

0. Mandatory page and collision check

Live-origin warning

UNVERIFIED FROM THE LIVE ORIGIN BECAUSE THE SITE ITSELF WAS DOWN FOR MAINTENANCE. I used the requested Bright Data browser path before doing any mathematics. Independent browser navigations to both https://www.erdosproblems.com/548 and https://erdosproblems.com/548 rendered only:

Site down for planned maintenance... We'll be back soon!

The document title was Site down for planned maintenance. The browser route was available; the authoritative origin content was not.

I therefore did not reconstruct the statement from the problem number or from memory. The substitutes checked on 2026-07-28 were:

The newest indexed copy of the

problem page, crawled about one month ago, which says that the page was last edited on 2026-03-07.

The newest indexed

discussion thread, including its only comment.

The indexed forum landing page, crawled about four weeks ago. It lists thread

548's last post as six months ago and does not list 548 among solution claims.

The public teorth/erdosproblems

database at current HEAD 2e7e7a630f9814f3df562bc1b207d9ad41451a55 (2026-07-28 07:39:21 UTC). Its entry still says falsifiable, but its per-entry status date is only 2025-08-31, so this is corroboration rather than live authority.

The newest indexed page says:

status: **FALSIFIABLE — Open, but could be disproved with a finite

counterexample**;

prize: $100 (contrary to the older tracker metadata, which says no prize);
“Comment activity that has not yet been incorporated into the remarks”:

None / Partial Solution;

“There are no solutions, partial or complete, claimed in the comments”;
Likes, Interested in collaborating, Currently working on this problem,

looks difficult, looks tractable, could be formalisable, and working on formalising: all None.

Thus no current worker, solution-claim marker, solved status, or falsified status was visible in the newest accessible page state. The comment mentions the old Ajtai–Komlós–Simonovits–Szemerédi announcement, but the current literature describes it as a sufficiently-large-tree result whose proof has not been made available, not a proof of all finite cases. The page itself classifies the thread as containing no claimed solution. This did not trigger the stop condition. There remains a narrow unavoidable caveat: an origin-only change after the last index crawl could not be excluded during maintenance.

Verbatim statement from the newest accessible page copy

Let $n\geq k+1$. Every graph on $n$ vertices with at least $\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices.

The page gives the source labels #548: [Er64c][Er74c,p.78][Er78,p.30][Er93,p.345][Va99,3.55] and the tag graph theory.

Results and comments listed on the page

The indexed remarks say:

Erdős and Sós also conjectured that

\[ \max\left\{ \binom{2k-1}{2}+1,\, (k-1)n-(k-1)^2+\binom{k-1}{2}+1 \right\} \] edges force every forest with $k$ edges. Erdős–Gallai proved that this expression is the threshold for $k$ independent edges.

Erdős [Er78] called the star case trivial; Erdős–Gallai proved the path case.
An easy induction gives the weaker sufficient bound $n(k-1)+1$.
The conjecture holds when the host has girth at least five

(Brandt–Dobson), when its complement has girth at least five (Wang–Li–Liu), when it has no $C_4$ (Saclé–Woźniak), and when its complement has no $C_4$ (Yi–Li).

It implies problems 547 and 557 and appears in the graphs problem

collection.

The single comment by Alfaiz (2025-12-11) is a literature list, not a proof claim. It reports:

Haxell: $K_{2,s}$-free hosts for

$s=\lfloor k/18\rfloor$.

Balasubramanian–Dobson: improvement to $s<k/12+1$.
Dobson: complements with no $K_{2,4}$.
Sidorenko: a tree vertex with at least

$\lceil k/2\rceil-1$ leaf-neighbours.

Eaton–Tiner: improvement to

$\lceil k/2\rceil-2$, and the small tree orders through eight.

Tiner–Tomlin: tree order nine.
Zhou: host order equal to the tree order.
Slater–Teo–Yap: host order tree-order plus one.
Woźniak: a special diameter-four family and host order tree-order plus two.
Tiner: host order tree-order plus three.
Yuan–Zhang: host order tree-order plus four.
Fan–Hong–Liu: spiders.
Balasubramanian's thesis: $K_{2,s}$-free hosts when

$s\geq2$ and $k>12(s-1)$.

The historical announcement by

Ajtai–Komlós–Simonovits–Szemerédi, whose complete proof is unavailable.

These bullets reproduce what the accessible page lists; they are not all independently re-proved here.

1. Parameter normalization and literature audit

Write $r=k+1$ for the number of vertices in the guest tree. Most papers use $r$ where the page uses $k+1$, and formulate the hypothesis as average degree $>r-2$.

This shift matters. The paper titled “for $k=9$” proves the result for a tree on nine vertices, hence page parameter $k=8$, not page parameter $k=9$. For the concrete page-$k=9$ work below, the page threshold is $4n+1$, exactly equivalent to average degree $>8$. I do not silently identify the page's literal “at least $x+1$” wording with “greater than $x$” in parity cases where $x$ is a half-integer.

The following primary papers or primary publisher records were opened and checked:

[Bollobás and Eldridge, *Packings of graphs and applications to

computational complexity*, JCTB 25 (1978), 105–124](https://doi.org/10.1016/0095-8956(78)90030-8). Its Theorem 1 is the small-edge-sum packing theorem used below.

[Győri, Kostochka, McConvey, and Yager, *A list version of graph

packing*, arXiv:1501.02488](https://arxiv.org/abs/1501.02488). Theorem 4 restates the exact Bollobás–Eldridge theorem, including all seven exceptional pairs. Every graph in those pairs is disconnected, and the pairs have orders four through nine.

[Eaton and Tiner, *On the Erdős–Sós conjecture and graphs with large

minimum degree*, Ars Combin. 95 (2010), 373–382](https://digitalcommons.uri.edu/math_facpubs/115/). The publisher abstract explicitly states both the $\lceil r/2\rceil-2$ leaf-neighbour theorem and the theorem that average degree $>r-2$ plus minimum degree at least $r-4$ forces every $r$-vertex tree.

[Tiner and Tomlin, On the Erdős-Sós Conjecture for $k=9$,

Alabama J. Math. 45(1) (2022), 37–45](https://www.ajmonline.org/wp-content/uploads/2022/11/On-the-Erdos-Sos-Conjecture.pdf). Its abstract and Theorem 2.1 prove the nine-vertex-tree case. Its introduction states the host-order results through tree-order plus four and records the leaf-neighbour, spider, diameter-at-most-four, and double-broom theorems used in Section 4 below.

[Görlich and Żak, On Erdős-Sós Conjecture for Trees of Large Size,

EJC 23(1) (2016), P1.52](https://www.combinatorics.org/ojs/index.php/eljc/article/view/v23i1p52). For fixed $c$, it proves the conjecture for a host on $r+c$ vertices once $r$ is sufficiently large in terms of $c$.

[Pokrovskiy, Hyperstability in the Erdős-Sós Conjecture,

arXiv:2409.15191](https://arxiv.org/abs/2409.15191). Theorem 1.16 proves the exact conjecture for all sufficiently large bounded-degree trees; it does not cover the fixed ten-vertex cases.

[Davoodi, Piguet, Řada, and Sanhueza-Matamala, *The asymptotic version

of the Erdős-Sós conjecture and beyond*, arXiv:2603.17755](https://arxiv.org/abs/2603.17755), submitted 2026-03-18. Corollary 1.4 gives, for $k\geq qn$ and large $n$, an asymptotic result with average degree $>(1+\eta)k$, without a maximum-degree restriction on the tree. The introduction says the AKSS proof remains unavailable and records a 2025 announcement by Reed for the exact dense case.

I found no available paper proving all finite cases and no exact result covering every ten-vertex tree in arbitrary-order hosts. That is a search miss, not a claim of nonexistence. The historical containment result for a host of the same order is already attributed to Sauer–Spencer/Zhou in the literature, so no novelty is claimed for the closed form extracted next.

2. Exact extremal number when host and tree have the same order

For a fixed $r$-vertex tree $T$, let

\operatorname{ex}_r(T)= \max\{e(H): |V(H)|=r,\ T\nsubseteq H\}.

Theorem

For every tree $T$ on $r$ vertices:

\operatorname{ex}_r(T)= \begin{cases} \left\lfloor \dfrac{r(r-2)}2\right\rfloor, &T=K_{1,r-1},\\[6pt] \binom{r-1}{2}, &T\text{ is not a star}. \end{cases}

The star line is (a) elementary-rigorous. The non-star line is (b) rigorous modulo the named Bollobás–Eldridge packing theorem.

Proof for a non-star

The graph $K_{r-1}\cup K_1$ has $\binom{r-1}{2}$ edges and has no spanning connected subgraph, so it avoids $T$. This proves the lower bound.

Conversely, suppose

e(H)\geq \binom{r-1}{2}+1

and put $F=\overline H$. Then

e(F)\leq r-2,\qquad e(T)+e(F)\leq(r-1)+(r-2)=2r-3.

Because $T$ is not a star, $\Delta(T)\leq r-2$. Also $\Delta(F)\leq r-2$: a universal vertex of $F$ alone would require $r-1$ edges. The seven Bollobás–Eldridge exceptions do not apply because each graph in every exceptional pair is disconnected, whereas $T$ is connected. Therefore $T$ and $F$ pack. A packing is exactly a copy of $T$ in $\overline F=H$. This proves the upper bound.

There is no non-star tree below order four, and the same argument applies from order four onward.

Proof for a star

An $r$-vertex graph avoids $K_{1,r-1}$ exactly when $\Delta(H)\leq r-2$. The handshake lemma gives

e(H)\leq \left\lfloor\frac{r(r-2)}2\right\rfloor.

This is attained. If $r$ is even, delete a perfect matching from $K_r$. If $r$ is odd, delete a matching covering $r-1$ vertices and one additional edge incident with the uncovered vertex. In both cases every vertex loses at least one incident edge, and the remaining edge count is the displayed floor. This proves equality.

Translation to the page and the first open tree order

With $r=k+1$, the exact same-order values are

\operatorname{ex}_{k+1}(T)= \begin{cases} \left\lfloor\dfrac{(k+1)(k-1)}2\right\rfloor, &T=K_{1,k},\\[6pt] \binom{k}{2},&T\text{ non-star}. \end{cases}

In particular, for page parameter $k=9$, every non-star ten-vertex tree is already forced by 37 edges on ten vertices, and 36 is sharp. The star $K_{1,9}$ is forced by 41 edges, and 40 is sharp. Thus the page's 41-edge same-order threshold is sharp only because of the star; each of the other 105 tree types has the sharp threshold 37.

3. Independent finite audit at $r=10$

The standalone checker does not invoke the packing theorem. With Python 3.12.3 and nauty 2.8.8 it:

calls geng to enumerate all 106 unlabelled ten-vertex trees;
separately enumerates every unlabelled ten-vertex graph $F$ with at

most eight edges;

decodes graph6 itself and checks order, edge counts, connectedness, and

the unique star;

for each of 105 non-stars and each $F$, constructs and directly checks

a labelled copy of the tree edge-disjoint from $F$;

checks the two sharp lower constructions and all threshold arithmetic.

There are 705 complement graphs, distributed by edge count as

(1,1,2,5,11,26,66,165,428)\quad(q=0,\ldots,8).

Consequently the checker verifies

105\cdot705=74{,}025

explicit non-star packings. Passing from unlabelled representatives to arbitrary labelled pairs is valid because packing is invariant under isomorphism. A fixed seed and fixed permutation list make the run deterministic; every successful mask is checked directly, so randomness is not an assumption in the certificate.

The certificate digest is:

90e24be38a8a06cf566bdcf09ba1d6fa54e9e3eff83f7ca7324af69e6076d337

This census is (d) computational-only and is independent corroboration of the theorem, not the theorem's logical foundation.

Reproduce with:

python3 runs/erdos548_wave9q_reverify.py

The checker source SHA256 after the reported run is:

d2a4c207f0dcee3e63e4c64601fff510e2cdf7a95022ecf4de8b6855257d861e

Full verifier source

#!/usr/bin/env python3
"""
Independent finite verification for the n = k+1 = 10 result in the
Erdos problem 548 report.

Requirements:
    nauty's `geng` executable, normally installed as `nauty-geng` or `geng`.

The script does not use the Bollobas--Eldridge theorem.  It independently
enumerates:
  * every unlabelled tree on 10 vertices; and
  * every unlabelled graph F on 10 vertices with at most 8 edges,
and exhibits a labelled copy of each non-star tree disjoint from every F.
Equivalently, each such tree embeds in the complement of F.

Every positive certificate is checked directly as a bit-mask identity.
The fixed permutation list makes the output deterministic.
"""

from __future__ import annotations

import hashlib
import random
import shutil
import subprocess
import sys
from collections import Counter


N = 10
SEED = 548
PERMUTATION_COUNT = 2500
EXPECTED_F_COUNTS = {
    0: 1,
    1: 1,
    2: 2,
    3: 5,
    4: 11,
    5: 26,
    6: 66,
    7: 165,
    8: 428,
}


def fail(message: str) -> "NoReturn":
    raise AssertionError(message)


def find_geng() -> str:
    for name in ("nauty-geng", "geng"):
        path = shutil.which(name)
        if path:
            return path
    fail("nauty geng was not found (tried `nauty-geng` and `geng`)")


def run_geng(geng: str, *args: str) -> list[str]:
    proc = subprocess.run(
        [geng, "-q", *args],
        check=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        text=True,
    )
    lines = [line.strip() for line in proc.stdout.splitlines() if line.strip()]
    if not lines:
        fail(f"geng produced no graphs for arguments {args!r}")
    return lines


def edge_pairs(n: int) -> list[tuple[int, int]]:
    # graph6 emits the upper triangle column by column:
    # (0,1), (0,2), (1,2), (0,3), ...
    return [(i, j) for j in range(1, n) for i in range(j)]


PAIRS = edge_pairs(N)
PAIR_INDEX = {edge: index for index, edge in enumerate(PAIRS)}
COMPLETE_MASK = (1 << len(PAIRS)) - 1


def decode_graph6(line: str) -> int:
    raw = line.encode("ascii")
    if not raw or raw[0] - 63 != N:
        fail(f"expected a short graph6 graph of order {N}, got {line!r}")
    values = [byte - 63 for byte in raw[1:]]
    if any(value < 0 or value > 63 for value in values):
        fail(f"invalid graph6 character in {line!r}")
    bits: list[int] = []
    for value in values:
        bits.extend((value >> shift) & 1 for shift in range(5, -1, -1))
    if len(bits) < len(PAIRS):
        fail(f"truncated graph6 string {line!r}")
    mask = 0
    for index, bit in enumerate(bits[: len(PAIRS)]):
        mask |= bit << index
    return mask


def edge_count(mask: int) -> int:
    return mask.bit_count()


def degrees(mask: int) -> list[int]:
    answer = [0] * N
    for index, (u, v) in enumerate(PAIRS):
        if mask & (1 << index):
            answer[u] += 1
            answer[v] += 1
    return answer


def connected(mask: int) -> bool:
    reached = 1
    while True:
        old = reached
        for index, (u, v) in enumerate(PAIRS):
            if not mask & (1 << index):
                continue
            if reached & (1 << u):
                reached |= 1 << v
            if reached & (1 << v):
                reached |= 1 << u
        if reached == old:
            return reached == (1 << N) - 1


def adjacency(mask: int) -> list[set[int]]:
    answer = [set() for _ in range(N)]
    for index, (u, v) in enumerate(PAIRS):
        if mask & (1 << index):
            answer[u].add(v)
            answer[v].add(u)
    return answer


def tree_diameter(adj: list[set[int]]) -> int:
    answer = 0
    for source in range(N):
        distance = [-1] * N
        distance[source] = 0
        queue = [source]
        for u in queue:
            for v in adj[u]:
                if distance[v] == -1:
                    distance[v] = distance[u] + 1
                    queue.append(v)
        if -1 in distance:
            fail("diameter requested for a disconnected graph")
        answer = max(answer, max(distance))
    return answer


def unique_tree_path(
    adj: list[set[int]], source: int, target: int
) -> list[int]:
    parent = {source: -1}
    queue = [source]
    for u in queue:
        if u == target:
            break
        for v in adj[u]:
            if v not in parent:
                parent[v] = u
                queue.append(v)
    if target not in parent:
        fail("path requested in a disconnected graph")
    answer = []
    current = target
    while current != -1:
        answer.append(current)
        current = parent[current]
    return answer[::-1]


def is_double_broom(adj: list[set[int]]) -> bool:
    # There must be a path whose off-path vertices are leaves adjacent to
    # one of the two ends of the path.
    for source in range(N):
        for target in range(source + 1, N):
            path = set(unique_tree_path(adj, source, target))
            if all(
                len(adj[v]) == 1
                and next(iter(adj[v])) in (source, target)
                for v in range(N)
                if v not in path
            ):
                return True
    return False


def known_family_memberships(mask: int) -> set[str]:
    adj = adjacency(mask)
    degree = [len(neighbors) for neighbors in adj]
    leaf_neighbors = [
        sum(degree[v] == 1 for v in neighbors) for neighbors in adj
    ]
    answer = set()
    if tree_diameter(adj) <= 4:
        answer.add("diameter<=4")
    if max(leaf_neighbors) >= 3:
        answer.add("at_least_3_leaf_neighbors")
    if sum(value > 2 for value in degree) <= 1:
        answer.add("spider")
    if is_double_broom(adj):
        answer.add("double_broom")
    return answer


def permute_mask(mask: int, permutation: tuple[int, ...]) -> int:
    answer = 0
    for index, (u, v) in enumerate(PAIRS):
        if not mask & (1 << index):
            continue
        a, b = sorted((permutation[u], permutation[v]))
        answer |= 1 << PAIR_INDEX[(a, b)]
    return answer


def deterministic_permutations() -> list[tuple[int, ...]]:
    rng = random.Random(SEED)
    result = [tuple(range(N))]
    current = list(range(N))
    for _ in range(PERMUTATION_COUNT - 1):
        rng.shuffle(current)
        result.append(tuple(current))
    return result


def main() -> None:
    geng = find_geng()

    tree_lines = run_geng(geng, "-c", str(N), "9:9")
    tree_masks = [decode_graph6(line) for line in tree_lines]
    if len(tree_masks) != 106:
        fail(f"expected 106 unlabelled ten-vertex trees, got {len(tree_masks)}")
    if len(set(tree_masks)) != len(tree_masks):
        fail("geng emitted duplicate labelled graph6 strings for the tree list")
    for line, mask in zip(tree_lines, tree_masks):
        if edge_count(mask) != 9 or not connected(mask):
            fail(f"non-tree in purported tree enumeration: {line}")

    f_lines = run_geng(geng, str(N), "0:8")
    f_masks = [decode_graph6(line) for line in f_lines]
    distribution = Counter(map(edge_count, f_masks))
    if dict(sorted(distribution.items())) != EXPECTED_F_COUNTS:
        fail(
            "unexpected complement enumeration counts: "
            f"{dict(sorted(distribution.items()))}"
        )
    if len(f_masks) != sum(EXPECTED_F_COUNTS.values()) != 705:
        fail(f"expected 705 complement graphs, got {len(f_masks)}")

    stars = [
        index for index, mask in enumerate(tree_masks) if max(degrees(mask)) == 9
    ]
    if len(stars) != 1:
        fail(f"expected one star among the trees, found indices {stars}")
    star_index = stars[0]

    family_counts = Counter()
    residual_tree_lines = []
    for line, mask in zip(tree_lines, tree_masks):
        memberships = known_family_memberships(mask)
        family_counts.update(memberships)
        if not memberships:
            residual_tree_lines.append(line)
    expected_family_counts = {
        "diameter<=4": 26,
        "at_least_3_leaf_neighbors": 45,
        "spider": 26,
        "double_broom": 17,
    }
    if dict(family_counts) != expected_family_counts:
        fail(f"unexpected known-family counts: {dict(family_counts)}")
    if len(residual_tree_lines) != 41:
        fail(
            "expected 41 trees outside the four checked families, got "
            f"{len(residual_tree_lines)}"
        )

    permutations = deterministic_permutations()
    digest = hashlib.sha256()
    certificates = 0
    for tree_index, (tree_line, tree_mask) in enumerate(
        zip(tree_lines, tree_masks)
    ):
        if tree_index == star_index:
            continue
        copies = sorted(
            {permute_mask(tree_mask, permutation) for permutation in permutations}
        )
        for f_line, f_mask in zip(f_lines, f_masks):
            witness = next((copy for copy in copies if not copy & f_mask), None)
            if witness is None:
                fail(
                    "fixed certificate pool did not pack tree "
                    f"{tree_line!r} against complement {f_line!r}"
                )
            # Directly recheck everything represented by the certificate.
            if edge_count(witness) != 9:
                fail("permuted tree copy has the wrong number of edges")
            if witness & f_mask:
                fail("certificate tree copy intersects the complement")
            if witness & ~COMPLETE_MASK:
                fail("certificate uses a nonexistent edge")
            digest.update(
                f"{tree_line}|{f_line}|{witness:012x}\n".encode("ascii")
            )
            certificates += 1

    if certificates != 105 * 705:
        fail(f"expected 74,025 certificates, checked {certificates}")

    # Non-star lower construction: K_9 plus an isolated vertex.
    k9_mask = 0
    for index, (u, v) in enumerate(PAIRS):
        if u < 9 and v < 9:
            k9_mask |= 1 << index
    if edge_count(k9_mask) != 36 or connected(k9_mask):
        fail("K_9 plus an isolated vertex construction was encoded incorrectly")

    # Star lower construction: K_10 minus a perfect matching.
    matching_mask = 0
    for u in range(0, N, 2):
        v = u + 1
        matching_mask |= 1 << PAIR_INDEX[(u, v)]
    star_extremal_mask = COMPLETE_MASK ^ matching_mask
    if edge_count(star_extremal_mask) != 40:
        fail("star extremal construction should have 40 edges")
    if max(degrees(star_extremal_mask)) != 8:
        fail("star extremal construction should have maximum degree 8")

    # Arithmetic checks for the exact r=10 formulas.
    if 36 != (N - 1) * (N - 2) // 2:
        fail("non-star extremal formula arithmetic failed")
    if 40 != N * (N - 2) // 2:
        fail("star extremal formula arithmetic failed")
    # Every 41-edge graph on 10 vertices has degree sum 82, hence a
    # vertex of degree at least ceil(82/10)=9, the centre of K_{1,9}.
    if (2 * 41 + N - 1) // N != 9:
        fail("star forcing degree arithmetic failed")

    # In the first not-already-covered host order for a ten-vertex tree,
    # n=15, average degree >8 means at least 61 edges.  In a subgraph
    # minimal subject to that inequality, deleting a vertex of degree d
    # leaves at most 4(15-1) edges, so d >= 61-56 = 5.
    if 4 * 15 + 1 != 61 or 61 - 4 * 14 != 5:
        fail("n=15 minimal-counterexample arithmetic failed")

    print(f"PASS: geng executable: {geng}")
    print(
        "PASS: enumerated 106 unlabelled ten-vertex trees "
        "(105 non-stars and one star)"
    )
    print(
        "PASS: enumerated 705 unlabelled complements with 0..8 edges; "
        f"counts {dict(sorted(distribution.items()))}"
    )
    print(
        "PASS: directly checked 74,025 non-star packing certificates "
        f"from {PERMUTATION_COUNT} fixed-seed permutations per tree"
    )
    print(f"certificate SHA256: {digest.hexdigest()}")
    print(
        "PASS: extremal constructions have 36 edges (non-star) and "
        "40 edges (star); forcing thresholds are 37 and 41"
    )
    print(
        "PASS: ten-vertex family counts are "
        f"{expected_family_counts}; their union has 65 trees and leaves "
        "41 residual isomorphism classes"
    )
    print("residual graph6 identifiers:")
    print(" ".join(residual_tree_lines))
    print(
        "PASS: a minimal n=15 counterexample has 61 edges and "
        "minimum degree at least 5"
    )


if __name__ == "__main__":
    try:
        main()
    except (AssertionError, subprocess.CalledProcessError) as exc:
        print(f"FAIL: {exc}", file=sys.stderr)
        raise SystemExit(1)

4. Clean reduction for page parameter $k=9$

The exact conjecture for tree orders through nine does not include a tree on ten vertices. For a ten-vertex tree, however, the audited host-order results settle host orders $10,11,12,13,14$. Thus the first host order not covered by those results is $n=15$.

The checker also classifies all 106 unlabelled ten-vertex trees by four uniform theorems stated in Tiner–Tomlin:

| audited tree family | number of ten-vertex types | |---|---:| | diameter at most four | 26 | | some vertex has at least three leaf-neighbours | 45 | | spider (at most one vertex of degree $>2$) | 26 | | double-broom | 17 |

These classes overlap. Their union contains exactly 65 tree types, leaving 41 types. The count and membership tests are (d) computational-only; using the four named embedding theorems to discard the union is (b) rigorous modulo those theorems.

The 41 residual types, as graph6 identifiers emitted and re-read by the checker, are:

I???E?wh_ I???E?wHo I???F?[c_ I??CAAor? I??CAAoZ?
I??CAAoR_ I??CAAoRG I??CA?wx? I??CE?oj? I??CE?obG
I??CE?oRG I??CE?wX? I??CB@Or? I??CB@ObO I??CBBOBO
I??CB?WdO I??CBAWP_ I??CBAW`O I??CBAW@o I??CB@Wh?
I??CB@Wd? I??CB@W`O I??CB?[s? I??CB?[cO I??ED?WD_
I??ED?W`G I??ED?WPG I??ED?W@g I??E@_KI_ I??E@_KAo
I?AA@AOy? I?AA@BOJ? I?AA@AW[? I?AA@AWX? I?AAD@Oq?
I?AAD?oq? I?AAD?Ws? I?AAD?WoG I?AAD?WWG I?AA@_gw?
I?AA@_goO

This is an exact residual set after the four audited family theorems; it is not a claim that no other paper handles some of these shapes.

Now fix one residual tree $T$, and suppose a counterexample exists. Choose a $T$-free counterexample minimal first in order and then in edge count. Because the page-$k=9$ threshold is $4n+1$, elementary deletion gives:

e(G)=4n+1,\qquad e(G[U])\leq4|U|\quad\text{for every proper }U\subset V(G), \qquad \delta(G)\geq5.

Indeed, the first equality follows by deleting surplus edges. The induced subgraph inequality follows from minimality. Taking $U=V(G)\setminus\{v\}$ gives

d(v)\geq(4n+1)-4(n-1)=5.

Eaton–Tiner prove that average degree $>8$ and minimum degree at least $10-4=6$ force every ten-vertex tree. Hence a minimal counterexample must in fact satisfy

\boxed{\delta(G)=5.}

At the first possible order $n=15$, it has exactly 61 edges. Deleting a degree-five vertex leaves exactly $4(n-1)$ edges, the boundary average degree eight. The minimality calculation is (a) elementary-rigorous; the conclusion $\delta=5$ is (b) rigorous modulo Eaton–Tiner.

Therefore a counterexample at the first unresolved tree order must have all of the following:

one of the 41 displayed tree types;
$n\geq15$;
exactly $4n+1$ edges after taking a minimal subgraph;
minimum degree exactly five;
every proper induced subgraph $U$ has at most $4|U|$ edges.

5. Exact remaining wall

The packing argument is sharp at equal order and then stops for a precise reason. At $n=10$, a 37-edge host has complement size at most eight, so

e(T)+e(\overline G)\leq9+8=17=2(10)-3,

exactly the Bollobás–Eldridge range. At the first residual order $n=15$, a threshold host has 61 edges and its complement has 44, so padding $T$ with five isolated vertices gives edge sum

9+44=53\gg 2(15)-3=27.

The packing theorem has no leverage there.

The exact missing uniform lemma is:

For each of the 41 residual ten-vertex trees $T$, no $T$-free graph $G$ of any order $n\geq15$ can simultaneously satisfy $e(G)=4n+1$, $\delta(G)=5$, and $e(G[U])\leq4|U|$ for every proper $U\subset V(G)$.

Proving that statement, or finding one graph that violates it while avoiding its $T$, would settle page parameter $k=9$. Checking $n=15$ alone would not: a finiteness or order-reduction theorem is still required for all $n>15$.

A naive exact $n=15$ formulation has 105 host-edge variables. For a tree with trivial automorphism group it has as many as

\frac{15!}{5!}=10{,}897{,}286{,}400

distinct embedded-copy inequalities; the 41-shape upper total before automorphism reductions is $446{,}788{,}742{,}400$. Merely storing nine 32-bit edge indices per constraint would take about 392 GB per maximally asymmetric tree, before solver overhead. At an optimistic ten million copy generations per core-second, raw generation alone has a 12.4 core-hour upper-total workload; exact branch-and-cut and proof of infeasibility would realistically move this into at least the tens-to-hundreds of core-hours, with large uncertainty. More importantly, it would still leave unbounded $n$. I did not run that oversized computation on this VM.

The modern regularity/hyperstability results also stop at a named boundary: they require sufficiently large trees, bounded degree, asymptotic slack, or a dense proportional regime. None supplies the finite uniform lemma above for a fixed ten-vertex tree at the exact threshold.

6. Claim ledger

(a) elementary-rigorous: the star extremal formula, both sharp

constructions, the translation at $k=9$, and the minimal-counterexample deletion inequalities.

(b) rigorous modulo named theorem: the non-star extremal formula via

Bollobás–Eldridge; the host-order and tree-family reductions; the minimum-degree-six exclusion via Eaton–Tiner.

(c) plausible/structural-unverified: only historical novelty. No

novelty claim is made, and the maintenance-period origin status has the explicit caveat in Section 0.

(d) computational-only: the nauty census, 74,025 explicit packing

certificates, family counts, and the 41 graph6 identifiers.

PARTIAL: Exact same-order extremal numbers are proved for every tree (and independently checked for all 106 ten-vertex trees); page $k=9$ is reduced to 41 tree types and critical hosts with $n\ge15$, $e=4n+1$, and $\delta=5$, but the required uniform exclusion remains open.

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger