PaperlayerView exact revision on arXiv

Source-linked AI summary

Three Conjectures on Binary Channels for the Doubly Symmetric Binary Source

Georg Pichler

arXiv:2609.27991v1cs.ITmath.IT

TL;DR

The paper addresses whether binary symmetric channels suffice, after convexification, to match arbitrary binary-channel rate triples, and which channels attain the double-sided bottleneck extrema when p = 0. It reduces the problems to finite-dimensional inequalities and proves the conjectures, with all three theorems formally verified.

  • Problem

    The paper asks whether convexified rate triples from arbitrary binary channels match those from BSCs, and which channel pairs attain the double-sided bottleneck extrema at p = 0.

    Source: §1 · p. 2

  • Method

    It reduces channel extremal problems to finite-dimensional inequalities over bias-variable atoms, using Lagrangian and optimizer analyses.

    Source: §1 · p. 2, §2.4 · pp. 6–7

  • Results

    For every p, conv A = conv B; at p = 0, the binary-channel maximum and minimum are attained by Z/S pairs in opposite and same orientations, respectively.

    Source: §1 · p. 2, §2.1 · p. 4

  • Takeaways & Limitations

    All three theorems are formally verified in Lean 4, including computation-dependent steps in the proof of the maximum conjecture.

    Source: §6 · p. 28

    The minimum theorem is proved only for binary test channels; the case of larger output alphabets remains open.

    Source: §4.1 · p. 13, §6 · p. 28

Abstract

from arXiv · show

We settle three conjectures concerning a doubly symmetric binary source $(X,Y)$ with crossover $p$. Consider Markov chains $U - X - Y - V$ with $U,V$ binary, and let $\mathcal{A}$ be the set of rate triples $(I(U;V),I(U;X),I(Y;V))$ attainable with arbitrary binary channels $X\to U$, $Y\to V$, and $\mathcal{B}$ the subset attainable with binary symmetric channels. The averaged BSC conjecture, Conjecture 5.2 of Pichler, Piantanida and Matz (2022), asserts $\operatorname{conv}\mathcal{A}=\operatorname{conv}\mathcal{B}$. We prove this for every $p\in[0,1]$. Two conjectures of Dikshtein, Ordentlich and Shamai (2022) concern the double-sided information bottleneck at $p=0$, where $Y=X$ and the two channels see the same source: their Conjecture 1 identifies the exact maximum of $I(U;V)$ at prescribed rates $I(U;X)$ and $I(Y;V)$, and their Conjecture 2 the exact minimum. We prove both for binary $U,V$: the two extrema are attained by the same pair of Z/S-channels, in opposite orientation for the maximum and in the same orientation for the minimum. The proofs were found with substantial AI assistance, and all three theorems are formalised in Lean 4 with Mathlib, depending only on the standard axioms. The development is available at https://github.com/g-pichler/bsc-averaging . The proof of Conjecture 1 of Dikshtein, Ordentlich and Shamai (2022) contains three certified computations, a polynomial bound, an interval sweep and a polynomial positivity certificate, all of which are checked in Lean.

1. Introduction

The paper resolves three conjectures about pairs of binary channels on a doubly symmetric binary source. It reduces these extremal questions to finite-dimensional inequalities involving the atoms of two bias variables.

The averaged BSC conjecture

  • For every source crossover p, the convex hull of rate triples attainable with arbitrary binary channels equals the convex hull attainable with binary symmetric channels.Convexification is necessary: without it, the conjecture is false.Source: §1 · p. 2

The double-sided information bottleneck

  • At p = 0, the maximum and minimum of I(U; V) at prescribed rates are attained by Z/S-channels in opposite orientations and Z-channels in the same orientation, respectively.The results prove both conjectures for binary U and V.Source: §1 · pp. 2–3
  • The DSIB proof excludes interior BSC-pair optimizers using a saddle-point argument, then establishes optimality of the conjectured boundary pairs by duality.At least one channel in an optimum must be an S- or Z-channel.Source: §1 · pp. 2–3

Related methods

  • The paper’s specific methodological contributions include an even/odd Lagrangian decomposition, residual analysis for interior optimizers, a saddle inequality, and corner certificates.Earlier work supplies related Lagrangian and perturbation techniques [6, 9, 10].Source: §1 · p. 3

Formal verification

  • All three theorems are formalized in Lean 4 with Mathlib, and three computations in the proof of Conjecture 1 are certified in Lean.The proofs received substantial AI assistance, while the Lean kernel checks the development.Source: §1 · p. 3

2. Setting, representation and outline

The section defines the source and channel regions, introduces bias variables as coordinates for the mutual informations, and outlines reductions used to prove the three conjectures.

2.1. The source and the three conjectures

  • The source is defined by uniform X and Y = X ⊕ Z, with independent Z distributed as Bern(p); the regions constrain the rates and value of binary test channels.A(p) allows arbitrary binary channels, while B(p) restricts both to binary symmetric channels.Source: §2.1 · pp. 3–4
  • For every p, conv A = conv B; at p = 0, the two DSIB conjectures identify channel pairs attaining the maximum and minimum of I(U; V).The DSIB results are proved for binary U and V.Source: §2.1 · p. 4

2.2. The ±1 encoding and the biases

  • The ±1 encoding maps binary convolution to multiplication, and the two channel bias variables retain the three mutual informations used in the optimization.In particular, I(U; X) = I(S; X), I(Y; V) = I(Y; T), and I(U; V) = I(S; T).Source: §2.2 · pp. 4–5

2.3. The Fourier picture

  • The Fourier view identifies the channel biases as level-one Fourier coefficients; it explains why these coordinates are natural, but the proofs do not use that interpretation..Source: §2.3 · p. 6

2.4. Outline of the proofs

  • For the averaged BSC conjecture, maximizing a Lagrangian over channel pairs reduces to bounding the odd gain in its even/odd decomposition.The odd gain is controlled through supermodularity and one-variable bounds on artanh.Source: §2.4 · pp. 6–7
  • At p = 0, the DSIB extrema are the Z/S-channel maximum and Z-channel minimum; interior optimality conditions force BSC pairs, which a second-order saddle test excludes.Boundary cases reduce to linear functionals of the remaining bias law and are certified by pointwise dual bounds; three computations support the maximum proof.Source: §2.4 · p. 7

3. The averaged BSC conjecture

The proof reduces the averaged BSC conjecture to bounding a Lagrangian for arbitrary binary channels by the best BSC value. A two-point theorem establishes that bound, yielding the claimed convex-region inclusion.

3.1. The two-point Lagrangian

  • The two-point Lagrangian represents arbitrary non-degenerate binary channels using four positive parameters, while symmetric pairs recover the BSC value.The best BSC Lagrangian is defined as the supremum of g over a compact square.Source: §3.1 · p. 8

3.2. The two-point theorem

  • The two-point theorem bounds the Lagrangian by any upper bound on its four corner values, and in particular by the best BSC-pair value.The proof reduces arbitrary non-degenerate channels to four parameters; degenerate channels are bounded separately.Source: §3.2 · p. 8, §3.1 · p. 8

3.2.1. The even/odd split

  • Since f = fe + fo, Proposition 3.2’s integrand splits into g(S̄,T̄) + fo(δS̄T̄), with g built from even fe and even in each argument; remaining subsections reduce via supermodularity to a two-sided bound on artanh.Those subsections bound mixed second differences by strict supermodularity.Source: §3.2.1 · p. 9

3.2.2. Case 1: same-direction skews

  • When both skews point in the same direction, the odd gain is negative, so the Lagrangian is strictly below the corner-value maximum.This follows from strict supermodularity of −ω and the positive factors λ and κ.Source: §3.2.2 · p. 10

3.2.3. Case 2: opposite skews

  • For opposite skews, the odd gain is bounded by the corner-value slack, which keeps the Lagrangian at or below the corner maximum.The proof bounds Ω by λκδ|Δg| and then by the gap between Gmax and the weighted corner average.Source: §3.2.3 · pp. 10–11

3.2.4. Proof of Theorem 3.4

  • Equal skews make the mixed difference vanish; the two strict-skew cases cover all other orientations, establishing the two-point bound.The proof then sets M to the best BSC value to conclude L ≤ Lsym.Source: §3.2.4 · p. 11

3.3. From the two-point theorem to the conjecture

  • For every linear functional used to test inclusion, the supremum over arbitrary binary channels is at most the best BSC value, proving the conjecture for the stated crossover range.The proof treats 0 < p < 1/2 via the Lagrangian bound and says the remaining cases were settled earlier in the section.Source: §3.3 · p. 11, §3.2.4 · p. 11

4. The double-sided information bottleneck at p = 0

This section proves the exact maximum and minimum of I(U;V) for binary channels in the p = 0 double-sided information bottleneck at prescribed rates. It develops the optimizer argument and handles the saddle inequality and boundary cases needed to establish the extrema.

4.1. Setting and statements

  • At budgets RZ(a), RZ(d), the maximum I(U;V) is VZS(a,d), attained by (Za,Sd), while the minimum is VZZ(a,d), attained by (Za,Zd).Every budget in (0, log 2) has a unique parameter representation RZ(a), so both bounds cover that full range.Source: §4.1 · p. 13
  • The maximum theorem proves Conjecture 1 for arbitrary finite outputs using binary sufficiency [4, Prop. 3], whereas Conjecture 2 is proved only for binary outputs, with larger alphabets open.The cited proposition establishes binary sufficiency for the maximization, but does not apply to minimization.Source: §4.1 · p. 13

4.1.1. Structure of the proof

  • The proof obtains an optimizer by compactness, forces interior non-degenerate optimizers to be BSC pairs, rules out BSC constrained extrema, then handles optimizers with boundary atoms.These four steps reduce the extremal cases to degenerate channels or optimizers with an atom at ±1.Source: §4.1.1 · pp. 13–14

4.2. Steps (A) and (B): interior optimisers are symmetric

  • For either extremum, any non-degenerate optimizer whose atoms are all interior must be a BSC pair; the KKT condition yields a bitangency used in the proof.The KKT condition is ∇V = λ∇R for λ ≥ 0, and the resulting tangency matches a secant chord to the objective function at both atoms.Source: §4.2 · pp. 14, 15, 17
  • Antipodal atoms on both sides force the interior-optimizer pair to be BSCs.The argument first forces ξ1 = ξ2 = 0; Lemma 2.6 then identifies the pair as BSCs.Source: §4.2 · p. 17

4.4. The saddle inequality

  • Every BSC pair is a Lagrangian stationary point, and the saddle inequality makes its Hessian indefinite, enabling the constrained perturbation argument for non-optimality.The saddle inequality is proved by reducing the bound along αβ = x to its diagonal case and establishing a kernel inequality.Source: §4.3 · p. 19, §4.4 · p. 22

4.3. Step (C): a symmetric pair is not optimal

  • Under the stated rate conditions, a BSC pair neither maximizes nor minimizes the objective: perturbations yield feasible pairs with strictly larger or smaller value, respectively.For maximization, fe(s) ≤ Cu and fe(t) ≤ Cv; for minimization, fe(s) ≥ Cu and fe(t) ≥ Cv. The maximization argument uses the saddle inequality, while the minimization argument needs only L11 < 0.Source: §4.3 · pp. 19–20

4.4. The saddle inequality

  • Φ(ϑ)>0 is established for every ϑ: polynomial bounds cover ϑ≤0.45, an 88-cell exact-rational sweep covers [0.45,3], and an analytic bound covers ϑ>3.The polynomial certificate is checked in Lean, and each interval cell passes the sweep test in exact rational arithmetic.Source: §4.4 · p. 24

4.5. Step (D): the corner bound

  • For a non-degenerate V-channel with an atom at ±1, rate budgets below RZ(a), RZ(d) imply I(U;V)≤VZS(a,d), while budgets above imply I(U;V)≥VZZ(a,d).The bounds are tight for the corresponding Z/S bias laws, as established by the tightness lemma.Source: §4.5 · p. 26

4.6. Proof of Theorems 4.4 and 4.5

  • An optimiser exists; degenerate channels cannot attain the required minimum, boundary channels are handled by Theorem 4.19, and an interior BSC-pair optimiser is excluded.The interior case is ruled out because Proposition 4.10 shows a feasible BSC pair is not an optimiser.Source: §4.6 · p. 27

5. Formalisation

The formal statements encode the three theorems for binary channels, and the main results depend only on standard Lean axioms. The formalisation also records which reductions and optimiser properties remain outside its scope.

Formalisation

  • The main theorems depend only on propext, Classical.choice, and Quot.sound; kernel-evaluated checks and proof-producing tactics verify the cited computation steps.The interval sweep and coefficient check use decide +kernel, while the polynomial bound uses ring and norm_num.Source: §5 · p. 27

Formal statements

  • The self-contained statement file defines binary channels as 2 × 2 row-stochastic matrices and mutual information in nats.It writes out the joint laws for (U, X), (Y, V), and (U, V) under the Markov chain.Source: §5 · p. 27
  • The encoded theorems state the convex-hull equality and the two p = 0 extremal claims using explicit channel pairs and their rates.The formal statements express the budgets and bounds through rates and values of channel pairs rather than RZ, VZS, and VZZ.Source: §5 · pp. 27–28

Scope

  • The formal statements cover binary test channels; the minimisation result does not extend to larger output alphabets under the available cardinality bounds.The cardinality reduction connecting the maximisation theorem to the DSIB function, and the translation of Conjecture 2, are not formalised; neither theorem asserts uniqueness.Source: §5 · p. 28

6. Conclusion

The paper proves the averaged BSC conjecture and both DSIB conjectures for binary test channels, reducing the extremal problems to inequalities involving bias-variable atoms. It formally verifies the theorems, while identifying open cases and the limits of the current formal development.

Conclusion

  • The averaged BSC conjecture and both DSIB conjectures are proved for binary test channels through reductions to bias-atom inequalities and finite-dimensional certificates.The averaged BSC result uses the two-point bound; the DSIB results reduce to a saddle inequality and corner certificates.Source: §6 · p. 28

Open questions

  • Conjecture 3 of remains open; its asserted BSC behaviour is established by [4, Theorem 1] only asymptotically as p → 1.The conjecture concerns p above a threshold that depends on the rate budgets.Source: §6 · p. 28
  • For Conjecture 2, larger test-channel output alphabets remain uncovered, and formalising the cardinality reduction would connect Theorem 4.4 to the DSIB function.The available cardinality bounds do not cover the larger-alphabet minimisation case.Source: §6 · p. 28

Conclusion

  • Several proof steps use computations and certificates that are impractical to check by hand, making formal verification relevant to their reliability.The paper leaves open whether machine-assisted search combined with formal verification can contribute to related problems such as the Courtade–Kumar conjecture.Source: §6 · p. 28

A. Notation

The notation appendix sets out the source, channel and rate conventions, then collects the bias-variable representation and the quantities used in the extremal proofs. It also defines the Z/S channel pairs and certificate machinery used for the p = 0 bottleneck results.

Source, channels and regions

  • The DSBS has uniform X and Y = X ⊕ Z with Z ∼ Bern(p); A(p) and B(p) denote rate regions for arbitrary binary channels and BSCs, respectively.The rate triple is (R0, R1, R2), and binary entropy is measured in nats.Source: A. Notation · p. 31

Biases, likelihood ratios and Lagrangian

  • The two channels are represented by mean-zero bias variables S and T, while likelihood ratios have linear forms in those biases and the noise operator maps χ to δχ.The appendix also records the even and odd parts of the rate integrand and the BSC-pair corner-value Lagrangian.Source: A. Notation · pp. 31–32

The double-sided bottleneck at p = 0

  • The zero-crossover bottleneck uses Z- and S-channels with common rate RZ(a); the anti-aligned pair (Za, Sd) gives VZS, while (Za, Zd) gives VZZ.The aligned S/S pair has value VZZ, and the S/Z pair has value VZS by symmetry.Source: A. Notation · p. 32

Interior optima and symmetric pairs

  • Interior-optimum notation includes the KKT rate multiplier, chord defects, skew coordinates, and residuals that vanish at an optimiser.For symmetric pairs, the appendix defines atom perturbations and the second derivative of the Lagrangian; the saddle inequality is expressed through a mixture functional and kernel certificate.Source: A. Notation · pp. 32–33

Saddle and corner certificates

  • The corner-bound notation defines certificate multipliers and slack functions, with nonnegative slack for the maximum and nonpositive slack for the minimum.The saddle certificate uses a bihomogeneous polynomial with nonnegative coefficients and a Kronecker-substitution base of 264.Source: A. Notation · pp. 33–34

B. Certificate data

The certificate appendix describes how three generated objects are represented and checked rather than reproducing them in full.

Certificate data

  • The certificate data are supplied as generation recipes: 53-coefficient and 88-cell objects are not fully reproduced, and the bihomogeneous polynomial is never expanded.The coefficient comparison is presented in a form checkable by hand; separate appendices give the recipes and rational interval arithmetic.Source: B. Certificate data · p. 34

B.1. The polynomial of the first range

This section bounds the first range with polynomials derived from an exponential-series tail estimate. Lean verifies the resulting polynomial identity, and the coefficient table records rounded coefficients of Q.

B.1. The polynomial of the first range

  • A six-term exponential-series tail bound yields two-sided polynomial bounds after evaluation at ±ϑ and averaging.The bounds use E = 7/4320 ϑ^6.Source: §B.1 · p. 34
  • On [0, 0.45], non-negative lower bounds permit substitutions that reduce the comparison to a polynomial identity of degree at most 60.The identity is verified in Lean by the ring tactic.Source: §B.1 · p. 34
  • Table 1 lists Q coefficients rounded down to four decimal places for k < 21; for k ≥ 21, the rounded value is −0.0001.The coefficients, table, and numerical bound are generated from the Lean definition of Q.Source: §B.1 · p. 34, Table 1 · p. 35

B.2. Rational enclosures of Φ and Φ′

Verified rational interval arithmetic encloses the quantities needed to bound Φ and Φ′. Exponential and logarithm enclosures provide the cell-wide and midpoint inputs used in those bounds.

B.2. Rational enclosures of Φ and Φ′

  • Sound interval operations enclose expression values throughout each cell, with rational endpoints rounded outwards to multiples of 1/m.The enclosures use endpointwise sums and differences, corner products, and positive-interval reciprocals.Source: §B.2 · p. 35
  • For exp, argument reduction and a truncated series produce enclosures; log brackets are certified by enclosing their exponentials around Z.The exp method uses k = 4 and n = 10 terms; rational bracket witnesses are checked by the kernel.Source: §B.2 · p. 35
  • Cell-wide log brackets enclose Φ′ across each cell, while midpoint brackets are used to enclose Φ at the midpoint.The three terms of Φ′ are evaluated with interval arithmetic, and the midpoint evaluation combines the first two terms of Φ.Source: §B.2 · pp. 35–36

B.3. The sweep cells

The sweep partitions [0.45, 3] into cells and checks a Lipschitz-based test using rational enclosures. The listed cells and their generating script are part of the development.

B.3. The sweep cells

  • Each cell must pass the rational test L · (hi − lo) < Φ((hi + lo)/2), with L bounding |Φ′| over the cell.The test uses k = 4, n = 10, and m = 10^9.Source: §B.3 · p. 36
  • Eighty-eight cells cover [0.45, 3], with widths from 2/1000 to 149/1000.The generating script selects the largest width in multiples of 1/1000 for which the test succeeds, except at the final endpoint.Source: §B.3 · p. 36
  • The full cell list and its generating script are included in the development.Source: §B.3 · p. 36

B.4. The P´olya certificate

The Pólya certificate proves coefficient non-negativity without expanding Q into its 41405 monomials. Lean checks a Kronecker-point evaluation and base-B digit conditions using exact integer arithmetic.

B.4. The Pólya certificate

  • Q is represented by the product-form expression tree rather than an explicit expansion into 41405 monomials.The expression tree is shown by definitional unfolding to agree with the product form.Source: §B.4 · pp. 36–37
  • The tree is bihomogeneous of bidegree (12, 12), and its coefficient absolute-sum bound satisfies L < 2^63.The bound is constructed structurally from sums and products of subtree bounds.Source: §B.4 · p. 36
  • At the Kronecker point, distinct monomials occupy distinct base-B positions, so the value N encodes Q's coefficients as digits.The point uses B = 2^64; the exponent index is less than 135.Source: §B.4 · p. 36
  • The coefficient bound and checked digit conditions imply every coefficient of Q is non-negative.Lean checks the integer facts, including the lowest 371293 = 13^5 digits, with GMP arithmetic.Source: §B.4 · pp. 36–37

C. Lean names

The table maps numbered statements in the paper to their Lean declarations and lists auxiliary facts used in their proofs. The principal declarations include the averaged BSC theorem and the two DSIB conjectures.

C. Lean names

  • The table links the paper’s numbered statements to Lean declarations and collects section-level definitions and auxiliary proof facts.It identifies `averaged bsc maximise mutual information`, `DSIB.conjecture1 p0`, and `DSIB.conjecture2 p0` as statements displayed in Section 5.Source: C. Lean names · p. 37
  • `averagedBSCConjecture all` names the theorem establishing the averaged BSC conjecture.The development also records `regionB subset regionA` and intermediate declarations related to the conjecture.Source: C. Lean names · p. 37
  • The listed auxiliary declarations include Lagrangian bounds, corner bounds, and named positivity and certificate results used in the proof development.Examples include `lagrTwoPoint le of corner bounds closed`, `cornerBound`, `cornerBoundMin`, and `certificate tight`.Source: C. Lean names · pp. 37–38
  • The development names both DSIB conjectures as proved: `conjecture1 p0 holds` and `conjecture2 p0 holds`.The corresponding declarations are `DSIB.conjecture1 p0` and `DSIB.conjecture2 p0`.Source: C. Lean names · pp. 37–38
Loading 2609.27991v1…