Bounded-degree induced forests in the minimum-order counterexample to the Albertson–Berman conjecture
Abstract
For a graph G let a(G) be the maximum order of an induced forest of G, and for an integer d ≥ 2 let f_d(G) be the maximum order of an induced forest of maximum degree at most d. Albertson and Berman conjectured in 1979 that a(G) ≥ |V(G)|/2 for every planar G; the conjecture was disproved in August 2026, and Cames van Batenburg, Goedgebeur and Jooken showed that the minimum order of a counterexample is 29, exhibiting two graphs G₂₉ and G₂₉' of that order with a=14. We prove that f_d(G₂₉)=f_d(G₂₉')=14 for every d ≥ 2: on these two graphs the degree restriction costs nothing, because some maximum induced forest is already a union of paths. Consequently both graphs violate the conjecture f_d(G)>2dn/(4d+1) of Chappell and Pelsmajer for exactly the range d ≥ 7, and satisfy it for 2 ≤ d ≤ 6, so they leave the cases that are open untouched. The threshold is exact rather than an artefact: 29=4 · 7+1 and 14=2 · 7, so 2dn=(4d+1)f_d at d=7 and it is the strictness of the inequality that fails. The refutation for d ≥ 7 already follows from the published value a(G₂₉)=14, and lowers from 52 to 29 the smallest order at which a counterexample to that conjecture has been recorded; what the theorem adds is the converse half. Along the way we re-certify a(G₂₉)=a(G₂₉')=14 by a route that does not use the exhaustive gadget tables of the original argument: one hereditary density inequality together with four explicit 2-core certificates spanning 22 vertices in total. Planarity, which is the one ingredient we do not formalise, is isolated as an explicit hypothesis and supported by a spherical rotation-system certificate whose checker rejects all 46 656 rotation systems of K_(3,3). Every theorem below is machine-checked in Lean 4; the few counts that are not are flagged where they occur.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
2b0aaab120a22a1fc282f0c53ea914933c19a36c07d85b99978328547791c6dd
Claim ledger
Stated results
AB1known data2026-08-29
a(G29) = 14 for the 29-vertex minimum-order counterexample of arXiv:2608.23260v1 Figure 3: every induced forest has at most 14 vertices (the paper's gadget argument, kernel-bound), and an explicit 14-vertex one attains it – so 2*a(G29) = 28 < 29 and G29 violates the Albertson-Berman bound
AB2known data2026-08-29
a(G29') = 14 for the 29-vertex planar triangulation G29' (81 = 3*29-6 edges, G29 plus the diagonal 16-20 of its unique quadrilateral face): it is also a counterexample
AB3known2026-08-29
the Albertson-Berman conjecture is false, stated exactly: for any predicate Planar holding of G29, it is not the case that every graph satisfying Planar has an induced forest on at least half its vertices; and every induced forest of G29 covers strictly less than half of it (c_P <= 14/29)
AB4known data2026-08-29
the positive control: for the icosahedron I, a(I) = 6 = |V(I)|/2 and alpha(I) = 3 = |V(I)|/4, so I satisfies the Albertson-Berman bound with equality and the same machinery accepts it
AB5routine2026-08-29
negative controls: no induced forest of G29 on 15 vertices; a(G29) <= 13 is false; an explicit 14-vertex set that is not an induced forest; the four 2-core certificates are induced cycles; and the 8-vertex subset of the Q-gadget on which the density inequality alone fails, so cert1 is load-bearing
AB6routine2026-08-29
spherical rotation-system certificates: G29 has a rotation system with 53 faces (29-80+53 = 2) and G29' one with 54, all triangles (29-81+54 = 2); a single transposition inside one rotation list of G29 drops the Euler characteristic to 0; and none of the 46656 rotation systems of K_(3,3) is spherical
AB7candidate2026-08-29
f_d(G29) = f_d(G29') = 14 for every d >= 2, because some maximum induced forest of each is linear (three disjoint paths); hence both refute the Chappell-Pelsmajer conjecture f_d(G) > 2dn/(4d+1) for exactly the range d >= 7, on 29 vertices instead of the 52 the source uses, and both satisfy it for 2 <= d <= 6
AB8routine2026-08-29
G29 is a vertex-critical counterexample: for every vertex v there is a 14-vertex induced forest avoiding v, so a(G29 - v) = 14 = |V(G29 - v)|/2 and every one-vertex deletion satisfies the Albertson-Berman bound with equality; three explicit forests suffice for all 29 vertices
AB9routine2026-08-29
two decidable bridges for SimpleGraph.IsAcyclic on induced subgraphs, both kernel-clean: if G[T] is a forest then sum over v in T of |N(v) cap T| < 2|T|; and if every nonempty T subset of S has a vertex with at most one neighbour in T then G[S] is a forest
AB10measurement2026-08-29
the compute-first gate and the prices: independent C reproduction of a(G29) = a(G29') = 14, of the paper's gadget values, of a(I) = 6 and alpha(I) = 3, the counts of maximum induced forests, and the exhaustive K5 rotation-system check
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- For a graph G, let a(G) be the maximum number of vertices among all induced forests of G (equivalently a(G) = |V(G)| − fvs(G), the complement of the feedback vertex number). In 1979 Albertson and Berman conjectured
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7