Logarithmic influence bounds and variance counterexamples for Boolean decision-tree covariance

Dev D. Goyal

Logarithmic influence bounds and variance counterexamples for Boolean decision-tree covariance

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Wan–Wright–Wu log₂ k variance bound for read-k decision-tree covariance
Posed in: Wan, Wright and Wu, ITCS 2014, Section 2.4; called a conjecture by Shalev, arXiv:1806.03646v2, Section 6.2
Status: Disproved
Result: Read-k decision trees with no repeated coordinate on a path have tree covariance at most I(f) log₂ k, sharp for k = 2^d, while exact read-3 trees refute the proposed bound Var(f) log₂ k.

Abstract

For a finite Boolean decision tree under uniform independent bits, the sum of absolute child covariances, weighted by node reach probabilities, is at most the sum of each coordinate influence times the base-two logarithm of its global query-node count. Counts zero and one receive weight zero. No coordinate repeats on a root-to-leaf path. A read-k tree therefore has absolute covariance at most I(f) log₂ k. The known dummy-prefix construction attains equality for powers of two. A four-variable witness and a nine-variable witness refute the coefficient-one logarithmic variance proposal. Every query in the latter witness is relevant. The formalization contains no Fourier-entropy theorem.

Details

Year: 2026
Discipline: Theoretical computer science
Area: Boolean functions and decision trees
Subject: Boolean functions and decision trees
Result type: Finite covariance bounds and variance counterexamples
Formal proof: Standalone Lean package
Family: readk-covariance
Keywords: decision trees, Boolean functions, covariance inequalities, influences, read-k formulas

Statement and scope

Result summary. For finite Boolean decision trees with no repeated coordinate on a root-to-leaf path, a logarithmic influence bound controls signed and absolute tree covariance. A known family attains equality at powers of two. Exact read-3 examples disprove the proposed coefficient-one variance replacement, including an example in which every query is relevant. No Fourier entropy theorem is formalized.

Formal scope. The standalone package uses Lean 4.19.0. Its 29 axiom reports are separate from the shared library's 29 Comparator declarations.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 337 KB
PDF on GitHub: papers/theoretical-computer-science/readk-covariance/docs/manuscript.pdf
LaTeX source: papers/theoretical-computer-science/readk-covariance/docs/manuscript.tex
Related work: papers/theoretical-computer-science/readk-covariance/docs/related-work.md

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/theoretical-computer-science/readk-covariance/ 10 Lean files

Lakefile

papers/theoretical-computer-science/readk-covariance/lakefile.toml

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/theoretical-computer-science/readk-covariance/README.md, which gives their context and working directory.

Reproduce

lake exe cache get
bash verify.sh
python3 scripts/test_verifiers.py

Build the manuscript

pandoc docs/manuscript.md --from=markdown+tex_math_single_backslash --standalone --number-sections --to=latex --output=docs/manuscript.tex
tectonic docs/manuscript.tex --outdir docs

README: papers/theoretical-computer-science/readk-covariance/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior results. Wan, Wright, and Wu, ITCS 2014, introduced the covariance and the dummy-prefix construction. Shalev, Section 6.2, Theorem 31, proved the square-root influence bound and proposed the logarithmic potential.

Questions and answers

Is the Wan–Wright–Wu logarithmic variance bound for read-k decision trees true?

No, as a statement about every given read-k tree. A four-variable read-3 tree computing two-variable AND has tree covariance 5/4 and variance 3/4, exceeding Var(f) log₂ 3, and a nine-variable read-3 tree in which every query is relevant (covariance 4863/4096, variance 3007/4096) also violates it. This does not rule out a statement that every function has some efficient tree obeying a logarithmic variance bound.

What positive bound is proved?

For a finite Boolean decision tree with no coordinate repeated on a root-to-leaf path, the weighted sum of absolute child covariances is at most Σᵢ Iᵢ(f) log₂ max(1, kᵢ), so a read-k tree has covariance at most I(f) log₂ k, improving Shalev's 2√k I(f). The logarithmic potential was proposed by Shalev, and the equality family at k = 2^d is the dummy-prefix construction of Wan, Wright and Wu.

Does this resolve the Fourier entropy–influence conjecture, and is it formally verified?

It does not resolve the Fourier entropy–influence conjecture. The Lean 4 formalization covers the covariance inequalities, the equality family and the finite counterexamples, and contains no Fourier transform or entropy theorem.

Cite

Citation file papers/theoretical-computer-science/readk-covariance/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{Goyal2026DecisionTreeCovariance,
  author = {Goyal, Dev D.},
  title = {Logarithmic influence bounds and variance counterexamples for Boolean decision-tree covariance},
  year = {2026},
  month = oct,
  howpublished = {Preprint},
  version = {1.0.0},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/theoretical-computer-science/readk-covariance},
  note = {Preprint}
}