Graphs with five harmonic boundary vertices, subcubic graphs with six, and minimum-boundary two-trees

Dev D. Goyal

Graphs with five harmonic boundary vertices, subcubic graphs with six, and minimum-boundary two-trees

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Classify the connected graphs with exactly five Steinerberger boundary vertices
Posed in: Chiem, Dudarov, Lee, Lee and Liu, A characterization of graphs with at most four boundary vertices, J. Combin. 15 (2024), Problem 6.1; boundary defined by Steinerberger, Discrete Appl. Math. 338 (2023)
Status: Solved with a computer-assisted proof: 227 reduced graphs; subcubic six-boundary graphs and minimum-boundary two-trees also classified
Result: A connected graph has exactly five boundary vertices if and only if it is a bridge subdivision of one of 227 reduced graphs; two-connected graphs with at most five boundary vertices have diameter at most two.

Abstract

Every two-connected graph with at most five Steinerberger boundary vertices has diameter at most two, and a connected graph has exactly five boundary vertices if and only if it is a bridge subdivision of one of 227 reduced graphs of order at most fourteen; this answers Problem 6.1 of Chiem, Dudarov, Lee, Lee and Liu. The proof reduces boundary metrics of every diameter, through the three cones of five-point metrics and a cap preserving local configurations, to an exact certificate that leaves fifteen metrics, excluded by hand. Connected graphs of maximum degree three with exactly six boundary vertices are the bridge subdivisions of 201 reduced graphs. For n ≥ 6 every two-tree on n vertices has at least ⌈n/2⌉ + 2 boundary vertices, with three extremal two-trees at each even n ≥ 8 and, at odd n ≥ 9, a period-eight quartic quasi-polynomial number of them, asymptotic to n⁴/192.

Details

Year: 2026
Discipline: Mathematics
Area: Graph theory
Subject: Graph theory and graph polynomials
Result type: Computer-assisted complete classification with exact certificates and partial Lean proofs
Formal proof: Standalone Lean package
Family: harmonic-boundary-five
Keywords: graph boundary, Steinerberger boundary, harmonic boundary vertices, graph classification, subcubic graphs, two-trees, five-point metrics

Statement and scope

Formal scope. Lean 4.35.0 proves, for finite simple graphs with certified shortest-path distances and the original strict boundary inequality, that a nonboundary degree-three vertex whose deletion leaves the graph connected forces six boundary vertices; the one-point gluing and block-accounting identities; the 14-vertex sharpness example; all 835 integer infeasibility systems of the local certificate; the bipartite subcubic boundary characterization; a sharp rooted metric truncation theorem; and the grammar weight bounds and polynomial identities for two-trees. A strict audit covers all 15,771 project declarations. The cone coverage, capping reduction, diameter-three argument, subcubic interior reduction, block decomposition, grammar correspondence and catalogue enumerations are conventional proofs and exact computations, replayed by the package checkers and by independent enumerations.

Lean 4.35.0 proves at graph level that a nonboundary degree-three vertex whose deletion leaves the graph connected forces six boundary vertices, together with the gluing and accounting identities, the 14-vertex sharpness example, all 835 infeasibility systems of the local certificate, the bipartite subcubic boundary theorem, a sharp rooted metric truncation theorem and the two-tree grammar bounds; a strict audit covers all 15,771 project declarations. The cone and capping reduction, the subcubic interior reduction and the catalogue enumerations are conventional proofs and exact computations, rechecked by independent enumerations.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 729 KB
PDF on GitHub: papers/mathematics/harmonic-boundary-five/manuscript.pdf
LaTeX source: papers/mathematics/harmonic-boundary-five/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/harmonic-boundary-five/

Lean project

papers/mathematics/harmonic-boundary-five/lean/ 57 Lean files

Lakefile

papers/mathematics/harmonic-boundary-five/lean/lakefile.toml

Toolchain

leanprover/lean4:v4.35.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/harmonic-boundary-five/VERIFICATION.md, which gives their context and working directory.

Lean

bash scripts/verify.sh /tmp/harmonic-boundary-five-verification

README: papers/mathematics/harmonic-boundary-five/README.md
Verification guide: papers/mathematics/harmonic-boundary-five/verification/README.md
Verification record: papers/mathematics/harmonic-boundary-five/VERIFICATION.md
Authorship: papers/mathematics/harmonic-boundary-five/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. Chiem, Dudarov, Lee, Lee and Liu, A characterization of graphs with at most four boundary vertices, 2024. · Steinerberger, The boundary of a graph and its isoperimetric inequality, 2023. · Koolen, Lesser and Moulton, Optimal realizations of generic five-point metrics, 2009.

Source. The boundary is due to Steinerberger (The boundary of a graph and its isoperimetric inequality, Discrete Appl. Math. 338 (2023)). The five-boundary classification is Problem 6.1 of Chiem, Dudarov, Lee, Lee and Liu (A characterization of graphs with at most four boundary vertices, J. Combin. 15 (2024), arXiv:2209.04438), who classified the graphs with at most four boundary vertices. The profile frame is due to Müller, Pór and Sereni and the five-point metric cones to Koolen, Lesser and Moulton. The subcubic six-boundary and two-tree results extend the question. Historical priority is not certified.

Questions and answers

Which graphs have exactly five boundary vertices?

A connected graph has exactly five Steinerberger boundary vertices if and only if it is obtained by subdividing bridges of one of 227 reduced graphs, which have at most fourteen vertices. Eighteen of them are two-connected, of order five or six, and every two-connected graph with at most five boundary vertices has diameter at most two. This answers Problem 6.1 of Chiem, Dudarov, Lee, Lee and Liu.

What is the boundary of a graph in this sense?

Steinerberger calls a vertex x a boundary vertex if some vertex y is strictly farther from x than the average distance from y to the neighbours of x. Chiem, Dudarov, Lee, Lee and Liu classified the graphs with at most four such vertices.

How many boundary vertices must a two-tree have?

For n ≥ 6 every two-tree on n vertices has at least ⌈n/2⌉ + 2 boundary vertices. Equality holds for three two-trees at each even n ≥ 8, and for a number of two-trees at odd n ≥ 9 given by an explicit quartic quasi-polynomial of period eight, asymptotic to n⁴/192.

Is the classification formally verified?

Partly. Lean proves the degree-three obstruction at graph level, the 835 local infeasibility systems of the certificate and several further components. The metric-cone reduction, the capping argument and the catalogue enumerations are conventional proofs and exact computations, rechecked by independent programs.

Cite

Citation file papers/mathematics/harmonic-boundary-five/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026harmonicboundaryfive,
  author = {Goyal, Dev D.},
  title = {Graphs with Five Harmonic Boundary Vertices, Subcubic Graphs with Six, and Minimum-Boundary Two-Trees},
  year = {2026},
  month = nov,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/harmonic-boundary-five}
}