Sparse assignment length is bounded by formula bits

For every finite formula $F$, $|V(F)|\le |E(F)|$: the number of distinct natural-number indices appearing in its literal lists is at most the number of bits of its specified encoding. There is no bound on the numeric values of these indices and no restriction on clause lengths; the inequality also covers formulas with no literals. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. The variable list $V(F)$ is obtained by reading the indices of all literals in the flattened clause list in order and deleting duplicate occurrences while retaining the first occurrence of each index. Write $E(F)$ for this Boolean-list encoding of a formula $F$: for each literal $(b,j)$, take $[b]$ followed by the little-endian canonical binary digits of $j$ (the digits of $0$ form the empty list), replace each bit $d$ by $[\mathrm{false},d]$, and append $[\mathrm{true},\mathrm{false}]$; concatenate these literal encodings within each clause and append $[\mathrm{true},\mathrm{true}]$; then concatenate the clause encodings in formula order. In particular $E([])=[]$. The supplied body is admitted with sorry; no proof of this assertion is supplied there.