# Verification of the three regular Seymour vertex theorem The accepted mathematical scope is finite simple oriented graphs with indegree and outdegree three at every vertex. Exact second neighbors exclude the root and its first neighbors. Within this scope the manuscript proves the sharp three-fifths proportion, the surplus lower bound, the classification at the exact proportion, and simultaneous equality. ## Mathematical audit For a deficient root, the nine arcs leaving its three first neighbors force those neighbors to form a directed triangle and to send all six remaining arcs to two exact second neighbors. Indegree saturation places the successors of the latter outside both layers. Each first neighbor is therefore strictly good. A strictly good vertex receiving a bad predecessor also receives a strictly good predecessor on the forced triangle, leaving room for at most two bad predecessors. Counting these incidences yields 3|B| <= 2|P| and both inequalities. At the exact proportion, every inequality in this count is an equality. The strictly good vertices partition into directed triangles; every bad vertex has a unique source triangle and a different target triangle. This recovers a loopless two-in/two-out multigraph, including multiplicities. Conversely every permitted multigraph expands to a simple oriented three-regular graph with exactly two fifths of its vertices deficient. Direct neighborhood counts give F = t + 9s, where t is the number of multigraph vertices and s counts those with two distinct target vertices. Simultaneous equality forces doubled directed cycles of length at least two. The audit checked the exact-distance exclusions, the distinction between in/out regularity and total degree, digons at k=1, allowed parallel and opposite arcs in the auxiliary multigraph, the uniqueness of overlapping forced triangles, and the difference between rounded and unrounded bounds. There is no known mathematical gap in this stated scope. This is the originating researcher's detailed self-audit, not independent peer review. ## Finite regression evidence - The standalone classification checker exhausts 916 labelled loopless two-in/two-out multigraphs of orders two through five (1, 3, 42 and 870). It checks their expansions, intrinsic decoding, neighborhood counts, surplus formula and connectivity equivalence. - It also checks 300 larger multigraph expansions, 1,216 random relabellings in total, 2,400 nonuniform degree-preserving-switch samples of regular oriented graphs, and four invalid-input controls. - The sharp-family checker checks all D_k for 2 <= k <= 20, through order 100, and rejects k=1 because it introduces digons. - The broader research checker covers 28,116 graphs and retains four invalid-input controls. Its additional Eulerian identities and diagnostic examples are not claimed as extra manuscript theorems or source closures. All three checkers have matching normal and optimized Python outputs. The packaged copies are rerun from the package directory and compared byte-for-byte with the retained evidence. These tests are finite checks, not a proof assistant or an exhaustive enumeration of all regular graphs. ## Document checks and limits The six-page PDF compiled successfully with the built-in LaTeX compiler and Tectonic. Every rendered page was visually inspected. The package manifest records the PDF, source, report and reproducibility hashes. The original source asks for the mean inequality over arbitrary Eulerian oriented graphs. Mixed degrees at most three and the unrestricted case remain unresolved here. The exact-proportion theorem does not classify every graph attaining a rounded bound or the surplus bound alone. The degree-two mean theorem is credited to Mody's earlier work. The bounded literature review did not certify absolute novelty. No claim is made about a later question whose complete published wording was not retrieved. This is an AI-assisted, unrefereed preprint.