General resolution-proof dual-certificate optimality conjecture

Let $F$ be an unsatisfiable CNF formula and let $T$ be a general resolution proof of its unsatisfiability. For each clause $C$ of $F$, let $\mathsf{occ}(C)\subseteq L(T)$ be the leaves labelled by $C$, and define its effective depth $d(C)$ by

$$2^{-d(C)}=\sum_{\ell\in\mathsf{occ}(C)}2^{-\mathsf{depth}(\ell)}.$$

Set

$$\mu_C^{(0)}=2^{-d(C)/2},\qquad \mu_C=\frac{\mu_C^{(0)}}{\sum_{C'\in F}\mu_{C'}^{(0)}}.$$

General resolution-proof certificate conjecture. For any unsatisfiable formula $F$ and resolution proof $T$, the resulting vector $\bm\mu$ satisfies

$$\sqrt{\sum_{C\in F}\mu_C^2}+\sum_{z\in\mathsf{var}(F)}\sqrt{\sum_{C\in\partial z}\mu_C^2}=\frac{1+\sum_{z\in\mathsf{var}(F)}\sqrt{\sum_{C\in\partial z}2^{-d(C)}}}{\sum_{C\in F}2^{-d(C)/2}}<1+\sqrt{2}.$$

The claim would extend the paper's optimality result from read-once resolution proofs to arbitrary resolution proofs, establishing optimality of the lower bound among unsatisfiable-matrix constructions. It is presented as an open conjecture.