Three-colored tournaments and monochromatic reachability

For any type $V$, a digraph on $V$ is a binary relation $D$ assigning a proposition $D(u,v)$ to each ordered pair of vertices. An arc coloring on $V$ is a function assigning to every ordered pair $(u,v)$ one of the three colors in $\mathrm{Fin}(3)$.

For a digraph $D$ on $V$, $\mathrm{IsTournament}(D)$ asserts that no vertex has a loop, and that for every pair of distinct vertices $u,v$, at least one of $D(u,v)$ and $D(v,u)$ holds while they do not both hold. Thus exactly one directed arc is present between every pair of distinct vertices.

For a digraph $D$ and coloring $\mathrm{color}$, $\mathrm{HasRainbowDirectedTriangle}(D,\mathrm{color})$ asserts that there exist vertices $a,b,c$ such that $a\ne b$, $b\ne c$, and $c\ne a$, with directed arcs $a\to b$, $b\to c$, and $c\to a$, and with the three colors $\mathrm{color}(a,b)$, $\mathrm{color}(b,c)$, and $\mathrm{color}(c,a)$ pairwise distinct.

$\mathrm{MonochromaticallyReaches}(D,\mathrm{color},s,t)$ asserts that there exists a color $k\in\mathrm{Fin}(3)$ and a directed path from $s$ to $t$ consisting of zero or more steps, every step $x\to y$ satisfying $D(x,y)$ and having $\mathrm{color}(x,y)=k$. Because zero steps are allowed, every vertex reaches itself monochromatically for any available color.

$\mathrm{IsMonochromaticSource}(D,\mathrm{color},s)$ asserts that for every vertex $t\in V$, the vertex $s$ monochromatically reaches $t$ in the preceding sense. The color and path may be chosen separately for each target $t$.