Manuscript Oai265-A@2 · Oai265-A.tex · lemma · c0a34a45

Lemma: Two-family entropy cancellation

Stage 1: audit of the five proof interfaces › The cancellation lemma · lines 533–577 · proof included or linked

Oai265-A@2#lem:cancellation

Let $ψ$ be pure on a finite site set $Λ$ , and suppose

A = D \cup ˙ i \in I_{0} ⋃ X_{i} \cup ˙ i \in I_{1} ⋃ X_{i}

is a partition. Fix an order on each finite $I_{f}$ , and put $B = Λ ∖ A$ . If

I_{ψ} X_{i} : B \cup j \in I_{f} j < i ⋃ X_{j} \leq ε_{i} (i \in I_{f}),

then

S_{ψ} (A) \leq S_{ψ} (D) + \frac{1}{2} i \sum ε_{i} .

Proof. Let $A_{f} = ⋃_{i \in I_{f}} X_{i}$ and $E_{f} = \sum_{i \in I_{f}} ε_{i}$ . The chain rule gives

S (B A_{f}) = S (B) + i \in I_{f} \sum S X_{i} B \cup j \in I_{f} j < i ⋃ X_{j} \geq S (B) + i \in I_{f} \sum S (X_{i}) - E_{f} .

Purity gives $S (B) = S (A)$ and $S (B A_{f}) = S (D A_{1 - f})$ . Subadditivity gives

S (B A_{f}) \leq S (D) + i \in I_{1 - f} \sum S (X_{i}) .

Add the inequalities for $f = 0, 1$ , cancel all tile entropies, and divide by two.

Displayed formulas in this passage

unlabeled · line 536
$A = D \cup ˙ i \in I_{0} ⋃ X_{i} \cup ˙ i \in I_{1} ⋃ X_{i}$
unlabeled · line 545
$I_{ψ} X_{i} : B \cup j \in I_{f} j < i ⋃ X_{j} \leq ε_{i} (i \in I_{f}),$
unlabeled · line 552
$S_{ψ} (A) \leq S_{ψ} (D) + \frac{1}{2} i \sum ε_{i} .$
unlabeled · line 561
$S (B A_{f}) = S (B) + i \in I_{f} \sum S X_{i} B \cup j \in I_{f} j < i ⋃ X_{j} \geq S (B) + i \in I_{f} \sum S (X_{i}) - E_{f} .$
unlabeled · line 572
$S (B A_{f}) \leq S (D) + i \in I_{1 - f} \sum S (X_{i}) .$