Manuscript X-H-ST@1 · X-H-ST.tex · proposition · 943aa27e
Proposition: Certificate soundness
Stage C: finite evaluations of the classical residuals › Reports and sound threshold certificates · lines 1438–1449 · proof included or linked
X-H-ST@1#prop:threshold
If the installed enclosure is valid, PASS implies , and FAIL implies . No conclusion is drawn from UNDETERMINED.
Proof. The value belongs to its enclosure. The three cases follow from the stated set inclusions.