How it works

The question

Write $h$ for the vector of joint entropies of $n$ random variables: one entry $h(S)$ for each non-empty subset $S$, so $2^n-1$ of them. Every statement is linear in $h$, and after moving everything to one side it reads

\[v \cdot h + v_0 \ \ge\ 0 .\]

The elemental inequalities

\[H(X_i \mid X_{\text{rest}}) \ge 0, \qquad I(X_i ; X_j \mid X_K) \ge 0\]

generate every Shannon-type inequality — every inequality that follows from the basic properties of entropy alone. There are $n + \binom{n}{2} 2^{n-2}$ of them: 1800 for eight variables.

The statement is Shannon-type, given constraints $a_i \cdot h + b_i \ge 0$, exactly when it is a non-negative combination of those inequalities and the constraints. By Farkas' lemma exactly one of two things holds:

• true: there are multipliers $y \ge 0$ with $v = \sum y_i a_i$ and $\sum y_i b_i \le v_0$ — a Proof;
• not provable: there is an $h$ satisfying every elemental inequality and constraint but not the statement — a Counterexample.

Finding the answer

Adding a coordinate for the constant term turns this into cone membership: does the target $t = (v, v_0)$ lie in the cone generated by the columns $(a_i, b_i)$?

Xitip.jl projects the target onto that cone with non-negative least squares (the Lawson–Hanson active set method) in floating point. A zero residual gives the proof's multipliers; a non-zero residual is a counterexample, by the same lemma.

The answer is then verified exactly:

• a proof is recomputed as exact rationals on the inequalities it uses, and checked to be non-negative;
• a counterexample is rounded to small integers, shifted into the interior of the Shannon cone to absorb the rounding, projected exactly onto any equality constraints, and then checked against every inequality in exact arithmetic.

Only if verification fails does an exact rational simplex method decide. That fallback has never been observed to trigger over thousands of random problems in the test suite, but it keeps the result exact in every case; it produces no certificate, so certificates is then empty.

Passing method=:simplex to prove or explain uses the simplex method alone. It is an independent implementation, which the test suite uses to cross-check the fast path.

Why not the simplex method throughout

The obvious approach — hand the linear program to a simplex solver, as ITIP, Xitip and Citip do — is much slower here, because these programs are highly degenerate. For eight variables:

The provable row is the whole argument. The not-provable row is not: there the two are comparable, and which one wins depends on the statement. Over three not-provable eight-variable statements, least squares took 6 s, 11 s and 12 s where the simplex took 7.8 s, 3.8 s and 55 s — it wins one, loses one and is five times slower on the third.

So the simplex is the fallback not because it is always slower, but because it is sometimes catastrophically slower while least squares never was, and a prover is asked about statements believed true far more often than not. The seconds in the not-provable column are the exact rational projection that certifies a counterexample, not the least squares step.

An earlier version of this package used a floating point simplex method with Bland's rule; at eight variables it cycled and never finished. Exact arithmetic fixed the cycling, and the least squares formulation removed the blow-up on provable statements.

Performance

Time per call in a warm session, on an Apple Silicon laptop:

The statements measured are subadditivity, H(X1,...,Xn) <= H(X1) + ... + H(Xn), and its reverse, which is not provable — named so the numbers can be reproduced.

The eight-variable example on the Examples page, with fourteen constraints, takes about 0.1 s.

A statement that cannot be proven takes longer when constraints are involved, because the counterexample then has to be certified by an exact projection rather than by rounding: about 12 s for the eight-variable problem above with one of its constraints removed.

Cost grows with $2^n$: nine variables is noticeably slower and ten is impractical. The command line adds about two seconds for Julia's startup, so prefer one session for many statements.

Limitations

• Non-Shannon-type inequalities. A negative answer means "does not follow from the elemental inequalities" — the statement may still be true for a deeper reason, as the Zhang–Yeung inequality is.
• Counterexamples are polymatroids. Beyond three variables not every polymatroid is entropic, so a counterexample refutes provability, not necessarily the statement.
• Size. At most 30 variables by construction, about 9 in practice.
• No variable collapsing. Variables that only ever appear together are not merged, an optimization the original Xitip had.

Testing

The suite runs with

$ julia --project=. -e 'using Pkg; Pkg.test()'

and covers the parser, known Shannon and non-Shannon results, constraints, the certificate checks (including that wrong certificates are rejected), the command line, and the LaTeX output — which is compiled with pdflatex where a TeX installation is available, and checked for lines running past the margin.

Randomized tests cross-check the fast path against the simplex method, verify each proof independently by re-adding the multipliers times the inequalities they name, and check that anything proven holds for the entropies of randomly drawn probability distributions.