A Dom-Path Longer Than the Jaco Graph Diameter Bound

Abstract

The finite linear Jaco graph on 33 vertices refutes Kok’s dom-path diameter conjecture.

Definition 1.1 (One-indexed Jaco vertices).

$$\forall n\in \mathrm{Nat},\mathrm{Vertex}\left(n\right)=\{i:\mathrm{Nat}\mid (1\le i)\wedge (i\le n)\}$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.Vertex (✓ std3).

Citation. Johan Kok (2025). Integer sequences with conjectured relation with certain graph parameters of the family of linear Jaco graphs. DOI: 10.48550/arXiv.2507.16500.

Commentary.

Vertex n is the subtype of natural indices from 1 through n. This preserves the paper’s labels v_1 through v_n rather than shifting them to zero.

Definition 1.2 (The finite linear Jaco graph).

$$\forall n\in \mathrm{Nat},\forall a\in \mathrm{Vertex}\left(n\right),\forall b\in \mathrm{Vertex}\left(n\right),(\mathrm{Adj}\left(\mathrm{jaco}\left(n\right),a,b\right))\iff (\mathrm{Adj}\left(\mathrm{val}\left(a\right),\mathrm{val}\left(b\right)\right))$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.jaco (✓ std3).

Citation. Johan Kok (2025). Integer sequences with conjectured relation with certain graph parameters of the family of linear Jaco graphs. DOI: 10.48550/arXiv.2507.16500.

Commentary.

The graph jaco n restricts the frozen infinite Jaco adjacency to the one-indexed vertices through n. Truncation removes only neighbors whose indices exceed n.

Definition 1.3 (Positions occupied by a vertex set).

$$\forall n\in \mathrm{Nat},\forall u\in \mathrm{Vertex}\left(n\right),\forall v\in \mathrm{Vertex}\left(n\right),\forall w\in \mathrm{Walk}\left(\mathrm{jaco}\left(n\right),u,v\right),\forall D\in \mathrm{Finset}\left(\mathrm{Vertex}\left(n\right)\right),\mathrm{positions}\left(w,D\right)=\{i:\mathrm{Fin}\left(\mathrm{length}\left(w\right)+1\right)\mid \mathrm{getVert}\left(w,i\right)\in D\}$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.positions (✓ std3).

Source. Repository-derived.

Commentary.

For a walk w and vertex set D, positions w D contains exactly the indices whose walk vertices lie in D. Its carrier has w.length + 1 elements.

Definition 1.4 (Dom-paths).

$$\forall n\in \mathrm{Nat},\forall h\in 1\le n,\forall w\in \mathrm{Walk}\left(\mathrm{jaco}\left(n\right),(1:\mathrm{Vertex}\left(n\right)),(n:\mathrm{Vertex}\left(n\right))\right),(\mathrm{IsDomPath}\left(n,h,w\right))\iff ((\mathrm{IsPath}\left(w\right))\wedge (\exists D\in \mathrm{Finset}\left(\mathrm{Vertex}\left(n\right)\right),(D\subseteq \mathrm{toFinset}\left(\mathrm{support}\left(w\right)\right))\wedge \left((\mathrm{IsNDominatingSet}\left(\mathrm{pathGraph}\left(\mathrm{length}\left(w\right)+1\right),\mathrm{dominationNumber}\left(\mathrm{pathGraph}\left(\mathrm{length}\left(w\right)+1\right)\right),\mathrm{positions}\left(w,D\right)\right))\wedge (\mathrm{IsNDominatingSet}\left(\mathrm{jaco}\left(n\right),\mathrm{dominationNumber}\left(\mathrm{jaco}\left(n\right)\right),D\right))\right)))$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.IsDomPath (✓ std3).

Citation. Johan Kok (2025). Integer sequences with conjectured relation with certain graph parameters of the family of linear Jaco graphs. DOI: 10.48550/arXiv.2507.16500.

Commentary.

Observation 2.7 (printed pages 6–7) reads verbatim: “For any finite linear Jaco graph Jn (x), n ≥ 2 there exists a pair of vertices i.e. v1 , vn for which a minimal (v1 , vn )-path (not necessarily a diam-path) i.e. Pd (Jn (x)) exists such that a γ-set of Pd (Jn (x)) is a γ-set of Jn (x). We call the path Pd (Jn (x)) the primary minimal dom-path.” A dom-path is a simple walk from v_1 to v_n with one set D of walk vertices. The positions of D form a minimum dominating set of the path graph, and the same D is a minimum dominating set of the finite Jaco graph.

Definition 1.5 (Kok’s Conjecture 2.9).

$$(claim)\iff (\forall n\in \mathrm{Nat},\forall h\in 1\le n,\exists w\in \mathrm{Walk}\left(\mathrm{jaco}\left(n\right),(1:\mathrm{Vertex}\left(n\right)),(n:\mathrm{Vertex}\left(n\right))\right),(\mathrm{IsDomPath}\left(n,h,w\right))\wedge (\mathrm{length}\left(w\right)\le \mathrm{diam}\left(\mathrm{jaco}\left(n\right)\right)+1))$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.claim (✓ std3).

Citation. Johan Kok (2025). Integer sequences with conjectured relation with certain graph parameters of the family of linear Jaco graphs. DOI: 10.48550/arXiv.2507.16500.

Commentary.

Conjecture 2.9 (printed page 7) reads verbatim: “For any linear Jaco graph Jn (x), n ≥ 1 the length of a diam-path and a primary minimal dom-path Pd satisfy |Pd | − |diam(Jn (x))| ≤ 1.” For every positive n, the conjectured bound requires some dom-path whose edge length is at most the Mathlib diameter of jaco n plus one. This existential statement is the weakest consequence independent of how the source selects its primary minimal dom-path.

Theorem 1.6 (Conjecture 2.9 is false).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.result (✓ std3). ∎

Resolves. Problems/kok-jaco-dom-path-diameter-refutation (refuted) by D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.result.

Source. Repository-derived.

Acknowledgement. Johan Kok (2025). Integer sequences with conjectured relation with certain graph parameters of the family of linear Jaco graphs. DOI: 10.48550/arXiv.2507.16500.

Commentary.

At n = 33, kernel-decided positive entries in powers of the adjacency matrix give a walk of length at most seven between every two vertices through Mathlib’s walk-counting identity. Four disjoint closed neighborhoods force every dominating set to contain at least four vertices, while a path graph on at most nine vertices has domination number at most three. A ten-vertex dom-path exists, so the contradiction is not caused by an empty notion.

References

• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.IsDomPath
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.Vertex
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.claim
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.jaco
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.positions
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/JacoDomPathDiameterRefutation.result
• Dependency: D5/S0/Certificates/JacoExponentialDominationRefutation
• Dependency: D5/S3/ConceptDynamics/GraphColoring/GraphCoverDomination