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

Erdős problem 626 — wave 6g

Date of live-page check and literature audit: 2026-07-27 UTC.

All logarithms below are natural logarithms. Changing the base does not affect the second question, but it does rescale the constant in the first.

Claim labels

(a) elementary-rigorous: proved below using only elementary facts.
(b) rigorous-modulo-named-theorem: the deduction is proved below, with

the stated published theorem used as an input.

(c) plausible/structural-unverified: a diagnosis or proposed route, not

a theorem.

(d) computational-only: certified by the supplied exhaustive program,

not promoted to a general theorem.

0. Mandatory live-page gate

I fetched https://www.erdosproblems.com/626 and its LaTeX endpoint through the Bright Data browser route because the direct datacenter route is Cloudflare-walled. This was a fresh check, not a use of the supplied stale YAML.

The live page showed:

status: OPEN;
claimed proofs: 0;
comments: 0;
“Currently working on this problem”: None;
“Interested in collaborating”: None;
likes: Alfaiz;
no “difficult”, “tractable”, “formalisable”, or “working on

formalisation” markers, and no formalised statement.

Thus the mandatory stop condition did not fire.

Verbatim current statement

Let $k\geq 4$ and $g_k(n)$ denote the largest $m$ such that there is a graph on $n$ vertices with chromatic number $k$ and girth $>m$ (i.e. contains no cycle of length $\leq m$). Does\[\lim_{n\to \infty}\frac{g_k(n)}{\log n}\]exist?
Conversely, if $h^{(m)}(n)$ is the maximal chromatic number of a graph on $n$ vertices with girth $>m$ then does\[\lim_{n\to \infty}\frac{\log h^{(m)}(n)}{\log n}\]exist, and what is its value?

Known results listed on the live page

The page states

\frac{1}{4\log k}\log n\leq g_k(n) \leq \frac{2}{\log(k-2)}\log n+1,

with the lower bound attributed to Kostochka [Ko88] and the upper bound to Erdős [Er59b]. It also says that Erdős proved

\lim_{n\to\infty}\frac{\log h^{(m)}(n)}{\log n}\gg\frac1m

and, for odd $m$,

\lim_{n\to\infty}\frac{\log h^{(m)}(n)}{\log n} \leq\frac{2}{m+1},

and conjectured the latter to be sharp. For even $m$, the page records Erdős's guess that the value should be in $[2/(m+2),2/m]$, and explicitly says that he could not prove this even for $m=4$. The displayed uses of “lim” here are reproduced as rendered; I do not interpret them as resolving the page's own existence question.

The page's bibliography entries are:

[Er59b] P. Erdős, Graph theory and probability, Canadian J. Math.

(1959), 34–38.

[Ko88] A. V. Kostochka, Upper bounds on the chromatic number of graphs,

Trudy Inst. Mat. (Novosibirsk) (1988), 204–226, 265.

Live page/history: <https://www.erdosproblems.com/history/626>. Primary copies checked: Erdős 1959 and Kostochka 1988 metadata/full-text entry.

1. Results obtained

There are four verifiable outputs.

(a) Both questions are exactly generalized-inverse questions for one

two-parameter extremal function $N_k(m)$. The desired limits exist if and only if the corresponding exponential/power growth rates of $N_k(m)$ exist. This identifies the precise missing uniformity lemma.

(b) Kim's Ramsey theorem gives the complete concrete case

\[ h^{(3)}(n)=\Theta\!\left(\sqrt{\frac n{\log n}}\right), \qquad \lim_{n\to\infty}\frac{\log h^{(3)}(n)}{\log n}=\frac12. \]

(b) Morgenstern's non-bipartite Ramanujan graphs, followed by a

from-scratch Hoffman argument, improve the live page's listed lower coefficient for $k=4$: \[ \liminf_{n\to\infty}\frac{g_4(n)}{\log n} \geq \frac{1}{6\log 2} =0.240449173480\ldots . \] The listed coefficient is $1/(8\log2)=0.180336880111\ldots$, so the improvement factor is exactly $4/3$. This is a deduction from published machinery, not a claim of novelty.

(d) A dependency-free exact checker reconstructs the

Exoo–Goedgebeur 66-vertex graph, proves its girth is exactly $6$, proves by exhaustive search that it is not 3-colourable, and exhibits a 4-colouring. Consequently $N_4(5)\leq66$.

Items 2–4 do not settle either general limit.

2. One extremal function controls both questions

Define

N_k(m)=\min\{|V(G)|:\ \chi(G)=k,\ \operatorname{girth}(G)>m\}.

In the notation of Exoo–Goedgebeur, $N_k(m)=n_{m+1}(k)$.

Exact inverse identities

Claim (a).

g_k(n)=\max\{m:N_k(m)\leq n\}, \tag{2.1}

and

h^{(m)}(n)=\max\{k:N_k(m)\leq n\}. \tag{2.2}

Proof. If an admissible graph has at most $n$ vertices, add isolated vertices. This preserves both chromatic number and all cycles, proving the forward directions in (2.1) and (2.2).

For the only slightly nontrivial reverse direction in (2.2), suppose a graph of order $n$, girth $>m$, and chromatic number $r\geq k$ is given. Delete vertices one at a time. Deleting one vertex decreases the chromatic number by at most one, since $\chi(G)\leq\chi(G-v)+1$. On the way from $r$ to $0$, an induced subgraph of chromatic number exactly $k$ therefore occurs. Induced subgraphs cannot create cycles. Hence $N_k(m)\leq n$. ∎

The same deletion observation proves that $N_k(m)$ is nondecreasing in both $k$ and $m$.

Generalized-inverse lemma

Claim (a). For fixed $k\geq4$, with positive finite constants,

\lim_{n\to\infty}\frac{g_k(n)}{\log n}=L_k \quad\Longleftrightarrow\quad \lim_{m\to\infty}\frac{\log N_k(m)}m=A_k, \qquad L_k=\frac1{A_k}. \tag{2.3}

For fixed $m$, again with positive finite constants,

\lim_{n\to\infty}\frac{\log h^{(m)}(n)}{\log n}=H_m \quad\Longleftrightarrow\quad \lim_{k\to\infty}\frac{\log N_k(m)}{\log k}=B_m, \qquad H_m=\frac1{B_m}. \tag{2.4}

Proof of (2.3). Put $a_m=\log N_k(m)$ and $G(n)=g_k(n)$. If $a_m/m\to A_k$, then for $m=G(n)$, (2.1) gives

a_m\leq\log n<a_{m+1}.

As $n\to\infty$, also $m\to\infty$, and squeezing gives $G(n)/\log n\to1/A_k$.

Conversely, evaluate a presumed limit $G(n)/\log n\to L_k$ at $n=N_k(m)$ and at $n=N_k(m)-1$. The first has $G(n)\geq m$; the second has $G(n)\leq m-1$. Since $N_k(m)\to\infty$ and $\log(N_k(m)-1)\sim\log N_k(m)$, these two inequalities squeeze $\log N_k(m)/m$ to $1/L_k$. ∎

For completeness, $N_k(m)\to\infty$ follows elementarily: take a vertex-critical $k$-chromatic induced subgraph, whose minimum degree is at least $k-1\geq3$, and expose its breadth-first tree to radius $\lfloor m/2\rfloor$. The absence of short cycles forces the usual Moore-tree number of distinct vertices, which tends to infinity with $m$. Also $N_k(m)\geq k$, so the sequence used in (2.4) tends to infinity with $k$.

Proof of (2.4). Put $b_k=\log N_k(m)$ and $H(n)=h^{(m)}(n)$. For $k=H(n)$, (2.2) says

b_k\leq\log n<b_{k+1}.

If $b_k/\log k\to B_m$, squeezing yields $\log H(n)/\log n\to1/B_m$. Conversely, use $n=N_k(m)$ and $n=N_k(m)-1$. At those orders $H(n)\geq k$ and $H(n)\leq k-1$, respectively, and the same squeeze gives $\log N_k(m)/\log k\to1/H_m$. ∎

Thus the first problem asks whether $N_k(m)$ has an exponential growth rate in $m$; the second asks whether it has a power-law exponent in $k$. This is an exact reduction, not merely an analogy.

3. The second question is completely determined for $m=3$

Here girth $>3$ means triangle-free. Jeong Han Kim proved

R(3,t)=\Theta(t^2/\log t).

Exoo and Goedgebeur explicitly record the standard consequence

n_4(k)=\Theta(k^2\log k).

Since $N_k(3)=n_4(k)$, (2.4), or direct inversion, yields:

Claim (b), modulo Kim's Ramsey theorem.

N_k(3)=\Theta(k^2\log k),\qquad h^{(3)}(n)=\Theta\!\left(\sqrt{\frac n{\log n}}\right), \tag{3.1}

and therefore

\boxed{\displaystyle \lim_{n\to\infty}\frac{\log h^{(3)}(n)}{\log n}=\frac12.} \tag{3.2}

The $\log k$ factor disappears after taking the log/log exponent, but is retained in (3.1).

Primary sources checked:

J. H. Kim,

The Ramsey number $R(3,t)$ has order of magnitude $t^2/\log t$, Random Structures & Algorithms 7 (1995), 173–207.

G. Exoo and J. Goedgebeur,

Bounds for the smallest $k$-chromatic graphs of given girth, DMTCS 21:3 (2019), paper 9.

4. A better published-machinery lower coefficient for $g_4$

External construction used

The following is the only non-elementary input in this section. Morgenstern's Theorem 5.13 supplies, for every power of two $q$, a family indexed by even extension degrees $d$ of Cayley graphs $X(q,d)$ on $\operatorname{PSL}(2,\mathbb F_{q^d})$ that are:

$(q+1)$-regular and Ramanujan;
non-bipartite in characteristic two;
of order

\[ M_d=q^d(q^{2d}-1); \]

of girth at least

\[ \frac23\log_q M_d. \]

The order formula uses $\operatorname{PSL}(2,\mathbb F_{q^d}) =\operatorname{PGL}(2,\mathbb F_{q^d})$ in characteristic two. The theorem is in:

M. Morgenstern,

Existence and Explicit Constructions of $q+1$ Regular Ramanujan Graphs for Every Prime Power $q$, JCTB 62 (1994), 44–62.

For an accessible precise restatement of the Ramanujan part, see Theorem 3.1 of Batra–Saxena–Shringi. For the characteristic-two non-bipartiteness and the $(2/3)\log_q|X|$ girth estimate, see the discussion of Morgenstern Theorem 5.13 in X. Dahan, Regular graphs of large girth and arbitrary degree, especially the paragraph beginning “for an even number $d$”.

Hoffman bound, proved here

Claim (a). If a $D$-regular graph has least adjacency eigenvalue $\tau<0$, then

\chi(G)\geq1+\frac{D}{-\tau}. \tag{4.1}

Proof. For a proper $r$-colouring, assign to each colour a vertex of a regular $(r-1)$-simplex: unit vectors whose pairwise inner products are $-1/(r-1)$. Let $x_j$ be the vector of the $j$-th coordinates assigned to all graph vertices. Summing the adjacency quadratic forms over coordinates gives

\sum_j x_j^TAx_j=-\frac{Dn}{r-1}, \qquad \sum_j\|x_j\|^2=n.

Rayleigh's inequality gives $-Dn/(r-1)\geq\tau n$, hence (4.1). ∎

For a non-bipartite $(q+1)$-regular Ramanujan graph, the eigenvalue $-(q+1)$ is absent and every nontrivial eigenvalue has absolute value at most $2\sqrt q$. Thus

\chi(X(q,d)) \geq 1+\frac{q+1}{2\sqrt q}. \tag{4.2}

Specialise to $q=16$

Now $X(16,d)$ is 17-regular, its least eigenvalue is at least $-8$, and (4.2) gives

\chi(X(16,d))\geq1+\frac{17}{8}=\frac{25}{8}>3.

Since chromatic number is integral, $\chi(X(16,d))\geq4$. By the vertex-deletion argument from Section 2, it contains an induced subgraph of chromatic number exactly $4$, with no shorter cycle. Add isolated vertices to obtain any larger desired order.

There is no subsequence gap hidden here. Consecutive allowed even extension degrees satisfy

\frac{M_{d+2}}{M_d} =q^2\frac{q^{2d+4}-1}{q^{2d}-1}=O_q(1).

For each sufficiently large $n$, choose the largest $M_d\leq n$. Then $\log M_d=\log n+O_q(1)$. Since a graph of girth $s$ witnesses $g_4(n)\geq s-1$, we obtain:

Claim (b), modulo Morgenstern's theorem.

\boxed{\displaystyle \liminf_{n\to\infty}\frac{g_4(n)}{\log n} \geq\frac{2}{3\log16} =\frac1{6\log2} =0.240449173480\ldots .} \tag{4.3}

The live-page coefficient at $k=4$ is

\frac1{4\log4}=\frac1{8\log2} =0.180336880111\ldots,

and the ratio is $4/3$. In the inverse formulation, (4.3) is equivalently the useful one-sided rate bound

\limsup_{m\to\infty}\frac{\log N_4(m)}m \leq\frac32\log16=6\log2, \tag{4.4}

improving the $8\log2$ supplied by inverting the page's listed lower coefficient.

General fixed $k$

Let $Q_k$ be the least power of two satisfying

1+\frac{Q_k+1}{2\sqrt{Q_k}}>k-1.

Exactly the same argument gives:

Claim (b), modulo Morgenstern's theorem.

\liminf_{n\to\infty}\frac{g_k(n)}{\log n} \geq\frac{2}{3\log Q_k}. \tag{4.5}

Since $\log Q_k=2\log k+O(1)$, the coefficient in (4.5) is $(1+o(1))/(3\log k)$, compared with the listed $1/(4\log k)$. The checker recomputes the exact choices and coefficients for $4\leq k\leq10$; no decimal was trusted by hand.

5. A fully checked finite witness

Exoo–Goedgebeur give the following $LCF(6,11)$ array. An entry $t$ in row $i$ means all edges

\{\,i+6j,\ i+6j+t\pmod {66}\,\},\qquad 0\leq j<11.

Their redundant array is:

0:   1    6   -23   -6   -1
1:   1    9    14   23   -1
2:   1   26    33  -10   -1
3:   1   18   -18  -14   -1
4:   1   10   -26   -9   -1
5:   1   18    33  -18   -1

The standalone checker below independently:

expands and deduplicates the edge orbits;
checks 66 vertices, 165 edges, and degree 5 at every vertex;
computes exact girth by BFS from every root;
runs exhaustive canonical DSATUR for three colours;
independently finds and checks a four-colouring.

Observed run:

vertices=66, edges=165, degrees={5}, girth=6
exact 3-color search: UNSAT (44708 search nodes)
exact 4-color search: SAT   (67 search nodes)
ALL CHECKS PASSED

Therefore:

Claim (d).

N_4(5)=n_6(4)\leq66,\qquad g_4(n)\geq5\ (n\geq66),\qquad h^{(5)}(66)\geq4. \tag{5.1}

This independently verifies the upper witness only. I did not repeat the paper's computational lower bound $n_6(4)\geq26$: the paper reports that its exhaustive enumeration of orders 19 through 25 used roughly 2.5 CPU-years on a cluster. That is far outside the requested few-CPU-minute budget. The witness verification here takes under one second on this VM.

6. Literature audit and non-results

I searched the exact functions and statement, the title/citations of the directly relevant $n_g(k)$ paper, and recent work on chromatic high-girth and $(r,g,\chi)$-graphs. I verified identifiers against primary paper or publisher pages rather than inferring from snippets.

The directly relevant post-page source located was Exoo–Goedgebeur (arXiv:1805.06713, published 2019). It studies finite $n_g(k)$, records Kim's triangle-free asymptotic, and supplies the 66-vertex witness. Its open problems do not prove either limit here. The 2025 paper Araujo-Pardo et al., On $(r,g,\chi)$-graphs and cages gives existence and finite cage constructions, not the missing asymptotic regularity. Exact-statement and citation searches through the audit date found no primary source claiming to resolve the two general limits. This is a search result, not a theorem that no such paper exists.

I also rejected the tempting “octonion” route (arXiv:1011.2642), which was subsequently reported incorrect, and did not use its advertised larger girth constant. The bound in Section 4 rests on Morgenstern's established theorem only.

7. Exact remaining wall

First limit

By (2.3), what is missing is exactly:

\text{prove that }\quad \frac{\log N_k(m)}m\quad\text{converges for every fixed }k\geq4. \tag{7.1}

A sufficient lemma would be an asymptotic submultiplicativity such as

\log N_k(m_1+m_2) \leq\log N_k(m_1)+\log N_k(m_2)+o(m_1+m_2). \tag{7.2}

Then Fekete-type machinery would finish the existence question.

Diagnosis (c). No standard graph operation found supplies (7.2): disjoint union takes the maximum chromatic number and does not increase girth; joins and blow-ups create triangles or 4-cycles; common graph products create short cycles or fail to preserve exact chromatic number; and covers/lifts can increase girth while lowering chromatic number. The missing object is therefore a bounded-overhead high-girth composition that preserves exact $k$-chromaticity, not another one-scale probabilistic bound.

Second limit

By (2.4), the exact missing statement is:

\text{prove that }\quad \frac{\log N_k(m)}{\log k}\quad\text{converges for every fixed }m. \tag{7.3}

Kim supplies (7.3) for $m=3$, with value $2$. For $m=4$, even the live page says Erdős could not prove his guessed interval for the reciprocal exponent. A finite table of $n_g(k)$ cannot provide the uniform $k\to\infty$ control required by (7.3), and the reported multi-CPU-year cost for just one small exact lower bound shows why extending the finite search is not a realistic route to the limit.

8. Reproduction

Standalone checker:

python3 runs/erdos626_wave6g_verify.py

It uses only the Python standard library. The full source follows so that this report remains self-contained.

#!/usr/bin/env python3
"""
Independent, dependency-free checks for runs/erdos626_wave6g.md.

This script checks the finite 66-vertex certificate from scratch and recomputes
all numerical constants used in the report.  It does not purport to prove the
external theorems of Kim or Morgenstern; it checks the deductions made from
their stated conclusions.
"""

from __future__ import annotations

from collections import deque
from math import isclose, log, sqrt


N = 66

# The LCF(6,11) array printed by Exoo--Goedgebeur.  Entry t on row i
# represents all edges {i+6j, i+6j+t (mod 66)}, 0 <= j < 11.
LCF_ROWS = (
    (1, 6, -23, -6, -1),
    (1, 9, 14, 23, -1),
    (1, 26, 33, -10, -1),
    (1, 18, -18, -14, -1),
    (1, 10, -26, -9, -1),
    (1, 18, 33, -18, -1),
)


def build_graph() -> tuple[set[tuple[int, int]], list[set[int]]]:
    """Expand the displayed LCF array, deduplicating undirected edges."""
    edges: set[tuple[int, int]] = set()
    for residue, offsets in enumerate(LCF_ROWS):
        for j in range(11):
            u = residue + 6 * j
            for offset in offsets:
                v = (u + offset) % N
                assert u != v
                edges.add((u, v) if u < v else (v, u))

    adjacency = [set() for _ in range(N)]
    for u, v in edges:
        adjacency[u].add(v)
        adjacency[v].add(u)
    return edges, adjacency


def exact_girth(adjacency: list[set[int]]) -> int | None:
    """
    Compute the exact undirected girth by BFS from every root.

    Every cycle has a root for which one of its edges joins two BFS branches;
    dist[u] + dist[v] + 1 therefore finds its length (and never understates
    the length of a genuine cycle).
    """
    n = len(adjacency)
    best = n + 1
    for root in range(n):
        distance = [-1] * n
        parent = [-1] * n
        distance[root] = 0
        queue = deque([root])
        while queue:
            u = queue.popleft()
            for v in adjacency[u]:
                if distance[v] < 0:
                    distance[v] = distance[u] + 1
                    parent[v] = u
                    queue.append(v)
                elif parent[u] != v:
                    best = min(best, distance[u] + distance[v] + 1)
    return None if best == n + 1 else best


def exact_k_coloring(
    adjacency: list[set[int]], k: int
) -> tuple[list[int] | None, int]:
    """
    Exact DSATUR backtracking.

    The search branches over every legal color of a maximum-saturation
    uncolored vertex.  Color names are introduced canonically (0,1,...), which
    quotients only global permutations of color names and loses no coloring.
    The returned node count makes it clear that an actual exhaustive search ran.
    """
    n = len(adjacency)
    colors = [-1] * n
    neighbor_color_masks = [0] * n
    nodes = 0

    def search(colored_count: int, colors_used: int) -> list[int] | None:
        nonlocal nodes
        nodes += 1
        if colored_count == n:
            return colors.copy()

        full_mask = (1 << k) - 1
        uncolored = [v for v in range(n) if colors[v] < 0]
        if any(neighbor_color_masks[v] == full_mask for v in uncolored):
            return None

        # Static degree is the conventional DSATUR tie-break.  Final -v makes
        # the run deterministic across Python versions.
        vertex = max(
            uncolored,
            key=lambda v: (
                neighbor_color_masks[v].bit_count(),
                len(adjacency[v]),
                -v,
            ),
        )
        forbidden = neighbor_color_masks[vertex]

        # Existing colors, plus at most the next new color.  Since the first
        # occurrence of colors can always be renamed by occurrence order, this
        # is an exhaustive symmetry reduction.
        for color in range(min(colors_used + 1, k)):
            bit = 1 << color
            if forbidden & bit:
                continue

            colors[vertex] = color
            changed: list[tuple[int, int]] = []
            for neighbor in adjacency[vertex]:
                if colors[neighbor] < 0:
                    old_mask = neighbor_color_masks[neighbor]
                    new_mask = old_mask | bit
                    if new_mask != old_mask:
                        changed.append((neighbor, old_mask))
                        neighbor_color_masks[neighbor] = new_mask

            answer = search(
                colored_count + 1,
                colors_used + (1 if color == colors_used else 0),
            )
            if answer is not None:
                return answer

            for neighbor, old_mask in changed:
                neighbor_color_masks[neighbor] = old_mask
            colors[vertex] = -1
        return None

    return search(0, 0), nodes


def assert_coloring(
    edges: set[tuple[int, int]], coloring: list[int], number_of_colors: int
) -> None:
    assert len(coloring) == N
    assert set(coloring) == set(range(number_of_colors))
    assert all(coloring[u] != coloring[v] for u, v in edges)


def least_power_of_two_for_k(k: int) -> int:
    """
    Least q=2^a for which the Ramanujan/Hoffman lower bound is > k-1:
        1 + (q+1)/(2 sqrt(q)) > k-1.
    """
    q = 2
    while 1.0 + (q + 1) / (2.0 * sqrt(q)) <= k - 1:
        q *= 2
    return q


def morgenstern_order(q: int, even_degree: int) -> int:
    """|PSL(2,F_{q^d})| in characteristic two."""
    assert q & (q - 1) == 0
    assert even_degree > 0 and even_degree % 2 == 0
    field_order = q**even_degree
    return field_order * (field_order**2 - 1)


def check_finite_certificate() -> None:
    edges, adjacency = build_graph()
    assert len(edges) == 165
    assert all(len(neighbors) == 5 for neighbors in adjacency)
    assert sum(map(len, adjacency)) == 2 * len(edges)

    girth = exact_girth(adjacency)
    assert girth == 6

    coloring3, nodes3 = exact_k_coloring(adjacency, 3)
    assert coloring3 is None

    coloring4, nodes4 = exact_k_coloring(adjacency, 4)
    assert coloring4 is not None
    assert_coloring(edges, coloring4, 4)

    print("finite witness:")
    print(f"  vertices={N}, edges={len(edges)}, degrees={{5}}, girth={girth}")
    print(f"  exact 3-color search: UNSAT ({nodes3} search nodes)")
    print(f"  exact 4-color search: SAT   ({nodes4} search nodes)")
    print(f"  4-coloring={coloring4}")


def check_ramanujan_deduction() -> None:
    q = 16
    degree = q + 1
    spectral_radius = 2 * sqrt(q)
    hoffman = 1 + degree / spectral_radius
    new_coefficient = 2 / (3 * log(q))
    old_coefficient = 1 / (4 * log(4))

    assert degree == 17
    assert spectral_radius == 8
    assert hoffman == 25 / 8
    assert hoffman > 3  # Hence the chromatic number is at least 4.
    assert isclose(new_coefficient, 1 / (6 * log(2)), rel_tol=1e-15)
    assert isclose(old_coefficient, 1 / (8 * log(2)), rel_tol=1e-15)
    assert isclose(new_coefficient / old_coefficient, 4 / 3, rel_tol=1e-15)

    # Consecutive available even extension degrees have bounded order ratio.
    # This is the elementary ingredient that turns an infinite construction
    # sequence into a liminf statement for every integer n after padding.
    order2 = morgenstern_order(q, 2)
    order4 = morgenstern_order(q, 4)
    order6 = morgenstern_order(q, 6)
    assert order4 // order2 > 0 and order6 // order4 > 0
    assert order4 / order2 < 2 * q**6
    assert order6 / order4 < 2 * q**6

    print("Morgenstern + Hoffman conditional arithmetic:")
    print(
        f"  q={q}, degree={degree}, nontrivial spectral bound="
        f"{spectral_radius:g}, Hoffman lower bound={hoffman:g}"
    )
    print(
        f"  new liminf coefficient={new_coefficient:.12f} "
        f"=1/(6 log 2)"
    )
    print(
        f"  page lower coefficient={old_coefficient:.12f} "
        f"=1/(8 log 2); ratio={new_coefficient / old_coefficient:.12f}"
    )
    print(
        "  consecutive even-degree order ratios "
        f"N4/N2={order4 / order2:.3f}, N6/N4={order6 / order4:.3f} "
        f"< 2*q^6={2 * q**6}"
    )


def check_general_q_table() -> None:
    print("general power-of-two choices:")
    print("  k   q_k    conditional coefficient    page coefficient    ratio")
    for k in range(4, 11):
        q = least_power_of_two_for_k(k)
        lower = 1 + (q + 1) / (2 * sqrt(q))
        assert lower > k - 1
        if q > 2:
            previous = q // 2
            assert 1 + (previous + 1) / (2 * sqrt(previous)) <= k - 1

        conditional = 2 / (3 * log(q))
        page = 1 / (4 * log(k))
        print(
            f"  {k:2d}  {q:4d}       {conditional:.12f}       "
            f"{page:.12f}    {conditional / page:.9f}"
        )


def main() -> None:
    check_finite_certificate()
    check_ramanujan_deduction()
    check_general_q_table()
    print("ALL CHECKS PASSED")


if __name__ == "__main__":
    main()

PARTIAL: reduced both limits exactly to growth rates of N_k(m), proved the m=3 exponent 1/2 modulo Kim, improved liminf g_4(n)/log n to 1/(6 log 2) modulo Morgenstern, and independently verified a 66-vertex girth-6 4-chromatic witness.

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