Soundness and termination of finite partition enclosures

The finite enumeration supplies one input interval for each exact weight and observable. By [F2] and [F5], when endpoint conversion is finite, rounding the lower endpoint down and upper endpoint up preserves containment of each input interval; if conversion overflows, the algorithm returns unresolved and the theorem makes no finite-enclosure claim. The partition sum and weighted sum are finite acyclic expression DAGs by [F1] and [F3].

Order the nodes of each finite DAG topologically. Each input node encloses its exact value by step 1.1. At every operation node with a finite result, [F4] gives the interval extension prescribed for that operation and [F6] proves that its value encloses the exact operation on the predecessor values. Induction over the finite node order therefore places $Z$ in $\mathcal{Z}$ and $N$ in $\mathcal{N}$ whenever those intervals are returned.

The exact partition sum satisfies $Z>0$ because $\mathsf{X}$ is nonempty and every $w(x)>0$. If the returned lower endpoint of $\mathcal{Z}$ is positive, then $0\mathrm{\notin }\mathcal{Z}$ and [F4] defines outward interval division; applying [F6] to this final operation gives $N\mathrm{/}Z\in \mathcal{N}\mathrm{/}\mathcal{Z}=\mathcal{E}$. If the lower endpoint is nonpositive, or any operation is non-finite, [F1] returns an unresolved status and no quotient enclosure is claimed. Finally, the procedure performs finitely many conversions and finitely many operations because $\mathsf{X}$ is finite, and every operation returns a finite interval or a status; hence it terminates.