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

For finite Boolean decision trees under uniform independent input bits, this paper proves an absolute tree-covariance bound by the sum of coordinate influences weighted by the base-two logarithm of global query multiplicity. No coordinate repeats along a root-to-leaf path. The resulting read-k bound has coefficient one. The known equality construction of Wan, Wright, and Wu attains this coefficient for powers of two. The logarithmic potential is due to Shalev. Two read-three trees disprove the proposed logarithmic variance replacement. One has four variables; the other has nine variables and distinct child functions at every query node. Lean 4.19 verifies the finite covariance results, equality family, and counterexamples. Exact rational programs reproduce both witnesses. The formalization does not contain a Fourier entropy theorem. The paper makes no claim of first priority.