Finite Sums of Tail Certificates

Abstract

Finite tail certificates add with summed budgets and enclose the exact sum at every window.

Theorem 1.1 (Finite tail certificates sum and enclose).

$$\mathrm{Controlled}(\sum _{i\in s}{b}_i)\wedge \Vert \sum _{i\in s}{v}_i-\sum _{i\in s}{r}_i(W)\Vert \le \sum _{i\in s}{b}_i(W)\wedge \sum _{i\in s}{r}_i(W)-\sum _{i\in s}{b}_i(W)\le \sum _{i\in s}{v}_i\le \sum _{i\in s}{r}_i(W)+\sum _{i\in s}{b}_i(W)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/TailCertificate.finite_tail_certificates_sum_and_enclose (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite family of certificates, the pointwise sum of their budget functions remains controlled. At every window W, the absolute difference between the sum of the exact values and the sum of the window readings is at most the sum of the window budgets. Equivalently, the exact sum lies in the closed interval from the summed reading minus the summed budget to the summed reading plus the summed budget.

References

• Truth anchor: D5/S3/Analytic/TailCertificate.finite_tail_certificates_sum_and_enclose