Yeah thanks, that version is indeed false, but I’ve been looking at a weakened version which might be true which I still like better than the sum version because it seems cleaner. I’ll write the conjecture up formally when I get the chance.
It’s funny how I’ve spent so many tokens (not much of my own time) on this problem even though I really don’t think it’s particularly important for the broader natural abstractions agenda relative to lots of other stuff, but it’s been a fun challenge, definitely one of the trickier formal math problems that’s been come across in this area.
This is above my head, but my Claude has a comment that might be useful to understanding why your conjecture is false.
Claude Opus 5
The exact-cap version is false. Here’s a witness.
Take the doubly symmetric binary source: X ~ Ber(1/2), Y = X ⊕ N with
N ~ Ber(q), 0 < q < 1⁄2. For the stochastic latent, flip an independent
coin and output X with probability λ, otherwise output ⊥. Then
I(X;Y|V) = (1−λ)·I(X;Y)
I(V;X|Y) = λ·h(q)
I(V;Y|X) = 0
Now look for a deterministic Γ with I(X;Y|Γ) ≤ I(X;Y|V). The constant Γ
gives exactly I(X;Y), so it’s excluded for every λ > 0. And every
nonconstant Γ costs at least h(q): join two atoms of the 2×2 support
whenever they share a row or a column, and that graph is a 4-cycle. A
cycle has no bridge, so any nonconstant partition cuts at least two
edges, each of weight h(q)/2. Γ = X attains it.
So the cheapest admissible Γ costs h(q) while the stochastic redundancy
is λ·h(q). The ratio is 1/λ, unbounded, and independent of q.
The failure is knife-edge, which I think is the useful part. Relax the
constraint to I(X;Y|Γ) ≤ I(X;Y|V) + η for any fixed η > 0 and the
constant Γ becomes admissible as soon as λ ≤ η/I(X;Y), so the supremum
is I(X;Y)/η and finite. The multiplicative form I(X;Y|Γ) ≤ C’·I(X;Y|V)
is untouched, and this family can’t refute it: its ratio is bounded by
C’/(C’−1).
The reason is convexity. A stochastic latent can time-share between
deterministic maps using an independent coin, so its achievable set of
(mixing, redundancy) pairs is convex. A partition can’t time-share. At
exactly equal mixing you’re comparing a convex region against a finite
set of points. So I’d read the sum form as doing real work rather than
being an artifact of the proof.
The natural strengthening that survives is the weighted family: for
λ > 0, compare min over Γ of [λ·I(X;Y|Γ) + H(Γ|X) + H(Γ|Y)] against
inf over V of [λ·I(X;Y|V) + I(V;X|Y) + I(V;Y|X)]. What’s proved now is
the λ = 1 slice, so that’s a genuine strengthening and it dodges the
obstruction above.
Two notes on #2, since GitHub didn’t show check runs on the head. I
replayed 34e3f898 in a clean checkout: source audit, all 8734 build
jobs, assert_no_sorry, and #print axioms pinned to exactly [propext,
Classical.choice, Quot.sound]. It verifies. Worth flagging that
T_le_698 is a T-endpoint, and generalized_stoch_to_det and LW_sum are
still exported at 1771, so the headline number and the public API
aren’t the same statement yet.
On extending past two observables, one caution: the analogous exact-cap
version fails the same way, and the machinery in #2 is specifically
two-factor (HGR maximal correlation, a bilinear form, two-factor
Hölder, a product marginal). It may extend, but I wouldn’t assume it’s
free.
Yeah thanks, that version is indeed false, but I’ve been looking at a weakened version which might be true which I still like better than the sum version because it seems cleaner. I’ll write the conjecture up formally when I get the chance.
It’s funny how I’ve spent so many tokens (not much of my own time) on this problem even though I really don’t think it’s particularly important for the broader natural abstractions agenda relative to lots of other stuff, but it’s been a fun challenge, definitely one of the trickier formal math problems that’s been come across in this area.