__On graphs whose nodes are Black or White__

In this note we consider finite directed graphs. Each *edge* is considered to be directed from some *node*, called its *source*, to some *node*, called its *target*. The *in-degree* of a node is defined as the number of edges that have that node as their target; the *out-degree* of a node is defined as the number of edges for which that node is the source. Finally we postulate that each node is either black or white. We now observe

(0) the sum of the in-degrees of the black nodes

= {when in doubt, consult the appendix}

the number of edges with a black target

= {a source is white or black}

#`WB` + #`BB`

where #`WB` denotes the number of edges with a white source and a black target (and for #`BB`, etc, analogously). By colouring all nodes black, the first equality of (0) yields

(1) the sum of the in-degrees of all nodes equals the number of edges.

Interchanging source and target we get from (0)

(2) the sum of the out-degrees of the black nodes equals #`BW` + #`BB`

and from (1)

(3) the sum of the out-degrees of all nodes equals the number of edges.

Combining (0) and (2) we get

__Lemma__ If the sum of the out-degrees of the black nodes equals the sum of the in-degrees of the black nodes, then

#`WB` = #`BW`

__Remark__ From (1) and (3) we conclude

(4) the sum of the in-degrees equals the sum of the out-degrees

and hence an alternative formulation for the Lemma is

__Lemma'__ If the sum of the out-degrees of the white nodes equals the sum of the in-degrees of the white nodes, then

#`WB` = #`BW`

(End of Remark.)

The Lemma has the

__Corollary__ If each node's in-degree equals its out-degree, then #`WB` = #`BW`.

__Appendix__

With finite types `node` and `edge` we declare

`n` : `node`;

`e` : edge;

`s`,`t` : `edge` → `node (`for “source” and “target” respectively);

`in`,`out` : `node` → nat (for “in-degree” and “out-degree” respectively)

defined by ` in`.`n` = 〈∑`e` : `t`.`e` = `n` : 1〉

`out`.`n` = 〈∑`e` : `s`.`e` = `n` : 1〉;

`b`,`w` : `node` → bool (for “black” and “white” respectively)

satisfying `b`.`n` ≡ ¬ `w`.`n` .

For the derivation of (0) we observe

〈∑`n `: `b`.`n `: `in`.`n`〉

= {definition of `in`}

〈∑`n `: `b`.`n `: 〈∑`e `: `t`.`e` = `n `: 1〉〉

= {unnesting}

〈∑`n`,`e `: `b`.`n` ∧ `t`.`e` = `n` : 1〉

= {Leibniz}

〈∑`n`,`e `: `b`.(`t`.`e`) ∧ `t`.`e` = `n` : 1〉

= {nesting}

〈∑`e `: `b`.(`t`.`e`):〈∑`n `: `t`.`e `= `n `: 1〉〉

= {1-point rule}

〈∑`e `: `b`.(`t`.`e`) : 1〉

= {notational liberty}

#?`B`

At first sight, the above derivation of

〈∑`n `: `b`.`n `: `in`.`n`〉 = 〈∑`e `: `b`.(`t`.`e`) : 1〉

seems an overkill. I have tried all sorts of alternatives—counting marks in a 2-dimensional table, mathematical induction over the number of edges or the number of black nodes. All these methods could, of course, be made to work, but if you wanted to eliminate the handwaving, the argument became longer than the above that uses no more than the standard quantification manipulation. I had the privilege of discussing the alternatives with Maarten Boasson and Fred B. Schneider, who happened to visit UT simultaneously.