Proofs and counterexamples

prove answers true or false. explain answers with a Result, which carries the reason: a Proof for each part of a true statement (an equality has two, one per direction), or a single Counterexample.

Both kinds of certificate are verified in exact rational arithmetic before they are returned, so a printed proof is not a plausible-looking summary of a floating point computation: it is the object that was checked.

Proofs

A proof writes the statement as a non-negative combination of basic inequalities and constraints:

using Xitip

result = explain("H(X,Y,Z) <= H(X,Y) + H(Z)")

TRUE
Proof of  H(Z) + H(X,Y) - H(X,Y,Z) >= 0:
         1 * ( I(X;Z|Y) >= 0 )
         1 * ( I(Y;Z) >= 0 )

proof = only(result.certificates)
proof.terms

2-element Vector{Pair{Rational{BigInt}, String}}:
 1 => "I(X;Z|Y) >= 0"
 1 => "I(Y;Z) >= 0"

Step by step

print_proof shows the same proof as a chain of equalities. Each line splits one non-negative quantity off the expression; the bracket holds what is still to account for, and the last line has nothing left:

print_proof(result)

Proof of  E >= 0  where  E = H(Z) + H(X,Y) - H(X,Y,Z)  =  I(X,Y;Z)

  E  =  H(Z) + H(X,Y) - H(X,Y,Z)
     =  I(X;Z|Y)  +  [ H(Y) + H(Z) - H(Y,Z) ]
     =  I(X;Z|Y)  +  I(Y;Z)

  where every term is non-negative:
    I(X;Z|Y)  =  -H(Y) + H(X,Y) + H(Y,Z) - H(X,Y,Z)  >= 0
    I(Y;Z)    =  H(Y) + H(Z) - H(Y,Z)                >= 0

  so E is a sum of non-negative terms, hence E >= 0.

Reading it:

• E is the statement written as entropies, with everything moved to one side. Where E is a single information quantity, that name is shown as well — here I(X,Y;Z).
• Each chain line is an identity, not an assumption: the terms so far plus the bracket always equal E.
• The list below the chain gives the entropy form of every term, so each line can be checked by hand without expanding definitions.
• The last chain line is the conclusion: E is a sum of non-negative quantities.

A remainder that happens to be a single quantity is named, which is what turns H(Y) + H(Z) - H(Y,Z) into I(Y;Z) above. The shapes recognised are H(A), H(A|B), I(A;B) and I(A;B|C), including positive multiples of them.

Constraints in a proof

Constraints appear as C1, C2, ... in the chain, with their own text beside their entropy form:

print_proof(explain("I(X;Z) <= I(X;Y)", "X/Y/Z"))

Proof of  E >= 0  where  E = -H(Z) + H(Y) + H(X,Z) - H(X,Y)

  E  =  -H(Z) + H(Y) + H(X,Z) - H(X,Y)
     =  C1  +  [ -H(Z) + H(X,Z) + H(Z,Y) - H(X,Z,Y) ]
     =  C1  +  I(X;Y|Z)

  where every term is non-negative:
    C1        =  H(Y) - H(X,Y) - H(Z,Y) + H(X,Z,Y)   =  -I(X;Z|Y)  = 0   (from constraint 1, reversed: X/Y/Z)
    I(X;Y|Z)  =  -H(Z) + H(X,Z) + H(Z,Y) - H(X,Z,Y)                >= 0

  so E is a sum of non-negative terms, hence E >= 0.

A statement can imply several relations — a Markov chain implies one per link — so a term reads "from constraint 1" rather than "constraint 1". An equality constraint used in the other direction is marked "reversed".

A constraint is not non-negative for any obvious reason, so the list says why it is. Here C1 is minus a conditional mutual information, which is non-negative only because the Markov chain forces that information to zero:

C1 = H(X) - H(W,X) - H(X,Y) + H(W,X,Y)  =  -I(W;Y|X)  = 0

A constraint written as an inequality is simply >= 0, and an elemental inequality is non-negative by definition, so neither needs more.

LaTeX

latex writes a proof for a paper. By default it is the identity alone, which is usually what a paper wants:

latex(result)

\begin{align*}
  E &= H(Z) + H(X,Y) - H(X,Y,Z) \\
    &= I(X ; Z \mid Y) + I(Y ; Z) \;\ge\; 0
\end{align*}

steps=true gives the full chain, and expand=true adds the entropy form of every term (constraints are always listed, since the chain would otherwise refer to something invisible):

latex(result; steps=true, expand=true)

\begin{align*}
  E &= H(Z) + H(X,Y) - H(X,Y,Z) \\
    &= I(X ; Z \mid Y) + [ H(Y) + H(Z) - H(Y,Z) ] \\
    &= I(X ; Z \mid Y) + I(Y ; Z) \;\ge\; 0
\end{align*}
where
\begin{align*}
  I(X ; Z \mid Y) &= - H(Y) + H(X,Y) + H(Y,Z) - H(X,Y,Z) \;\ge\; 0 \\
  I(Y ; Z) &= H(Y) + H(Z) - H(Y,Z) \;\ge\; 0
\end{align*}

The output needs amsmath. Long expressions are wrapped to stay inside the page margin; the package's own test suite compiles the output with pdflatex where a TeX installation is available and fails on an overfull line.

latex_string returns the same text as a String.

Counterexamples

When a statement cannot be proven, the certificate is a counterexample: entropy values satisfying every basic inequality and every constraint, but not the statement.

explain("I(X;Y|Z) <= I(X;Y)")

NOT PROVABLE (false or non-Shannon-type)
No proof of  H(X) + H(Y) + H(Z) - H(X,Y) - H(X,Z) - H(Y,Z) + H(X,Y,Z) >= 0; it fails for the direction:
    H(X) = 6
    H(Y) = 6
    H(X,Y) = 11
    H(Z) = 6
    H(X,Z) = 11
    H(Y,Z) = 11
    H(X,Y,Z) = 13
  which satisfy every elemental inequality and constraint, but give -2 < 0.
  There the statement reads
    left side   I(X;Y|Z)  =  3
    right side  I(X;Y)    =  1
  so it asks for 3 <= 1, which is false.
  where
    I(X;Y|Z)  =  -H(Z) + H(X,Z) + H(Y,Z) - H(X,Y,Z)  =  -6 + 11 + 11 - 13  =  3
    I(X;Y)    =  H(X) + H(Y) - H(X,Y)                =  6 + 6 - 11         =  1
  Any positive multiple of these values fails in the same way.

The values are exact rationals, rounded to small numbers where possible, and can be read off the Counterexample:

counter = only(explain("H(X) <= H(Y)").certificates)
counter.entropies        # indexed by subset bitmask: 1 = X, 2 = Y, 3 = X,Y

3-element Vector{Rational{BigInt}}:
 5
 4
 7

The printed counterexample ends with the same reading: what each side of the statement comes to there, and how every quantity gets its value out of the entropies above it.

Reading the numbers

The values are entropies in bits, not probabilities: they are bounded by the logarithm of the alphabet size, not by 1. H(X) = 6 describes a variable with up to 64 equally likely values, and H(X,Y,Z) = 13 a triple with up to 8192.

direction = true marks the case where the values are not a point but a direction: the statement has no constant term, so every positive multiple of the values fails in the same way, and the small integers printed are just the most readable representative. Dividing by the largest of them is equally valid:

table = entropy_table(explain("I(X;Y|Z) <= I(X;Y)"))
peak = maximum(last, table)
[k => Float64(v // peak) for (k, v) in table]

7-element Vector{Pair{String, Float64}}:
     "H(X)" => 0.46153846153846156
     "H(Y)" => 0.46153846153846156
     "H(Z)" => 0.46153846153846156
   "H(X,Y)" => 0.8461538461538461
   "H(X,Z)" => 0.8461538461538461
   "H(Y,Z)" => 0.8461538461538461
 "H(X,Y,Z)" => 1.0

What matters is the relations between them. For the table above,

\[I(X;Y) = H(X) + H(Y) - H(X,Y), \qquad I(X;Y \mid Z) = H(X,Z) + H(Y,Z) - H(Z) - H(X,Y,Z),\]

and the second is the larger, which is why I(X;Y|Z) <= I(X;Y) fails. Conditioning really can raise mutual information, and it does so in an everyday distribution: let X and Y be independent fair bits and Z = X xor Y. Then

prove("I(X;Y|Z) <= I(X;Y)", "I(X;Y) = 0", "H(Z|X,Y) = 0", "H(X|Y,Z) = 0")

false

is still not provable, because those constraints describe exactly that distribution, where I(X;Y) = 0 while I(X;Y|Z) = 1 bit.

When it is not provable: what would make it true

A counterexample says the statement does not follow from the basic inequalities. It does not say the statement is useless — most information inequalities in practice hold under assumptions. sufficient_conditions looks for those assumptions.

sufficient_conditions("I(X;Y|Z) <= I(X;Y)")

Not provable as it stands:
    I(X;Y|Z) <= I(X;Y)

Provable if you assume any one of these:

  1. I(X;Y|Z) = 0
       X and Y are independent given Z, the Markov chain X/Z/Y

  2. I(X;Z|Y) = 0
       X and Z are independent given Y, the Markov chain X/Y/Z

  3. I(Y;Z|X) = 0
       Y and Z are independent given X, the Markov chain Y/X/Z

Conditioning can raise mutual information, so the statement is false in general. It becomes provable the moment any one of the three pairs is conditionally independent — two of those readings being the Markov chains X/Y/Z and Y/X/Z, which is the familiar fact that along a Markov chain conditioning cannot help.

The candidate assumptions are the elemental quantities, each forced to zero. That is a deliberate choice rather than a convenience: every elemental quantity reads as a condition one would state out loud — an independence, a conditional independence, or a functional dependence — so every answer is something you can say in words, and the constraint text printed beside it can be fed straight back in:

prove("I(X;Y|Z) <= I(X;Y)", "I(X;Z|Y) = 0")

true

Assumptions can be combined. Some statements need two:

sufficient_conditions("2H(X,Y,Z) <= H(X,Y) + H(Y,Z)"; maxsize = 2)

Not provable as it stands:
    2H(X,Y,Z) <= H(X,Y) + H(Y,Z)

Provable if you assume any one of these:

  1. H(X|Y,Z) = 0  and  H(Z|X,Y) = 0
       X is a function of Y, Z, written X:Y,Z
       Z is a function of X, Y, written Z:X,Y

and some have nothing that saves them:

sufficient_conditions("H(X) + H(Y) + H(Z) <= H(X,Y,Z)"; maxsize = 2)

Not provable as it stands:
    H(X) + H(Y) + H(Z) <= H(X,Y,Z)

No set of at most 2 assumptions out of 9 candidates makes it provable.

Only minimal sets are reported: once an assumption works on its own, no pair containing it is offered.

How the search is kept small

The number of candidates is the number of elemental inequalities, which grows quickly — 9 for three variables, 28 for four, 1800 for eight — and combining them squares that. Two things keep it in hand.

The first is the counterexample. If a quantity is already zero at the counterexample, assuming it is zero leaves that counterexample exactly where it was, so that assumption cannot possibly help. Only quantities that are strictly positive there are worth trying, and a combination is worth trying only when at least one of its members is. This is a sound rule, not a heuristic, and the test suite checks it against brute force over every candidate: the pruned search returns exactly the same answers.

The second is plain book-keeping: limit caps how many sets are reported and budget caps how many statements are proven, so a large problem returns something useful rather than running away. The printed result says when the search stopped early.

Each answer is verified the ordinary way — by proving the statement again with the assumption added — so a reported condition is one the prover accepts, not one the search believes.

Results without a certificate

If the exact simplex fallback had to decide (which the test suite has never observed over thousands of random problems), the verdict stands but certificates is empty:

explain("H(X,Y) <= H(X) + H(Y)"; method=:simplex)

TRUE
  (no certificate: decided by the simplex method)