The execution bound covers storage quantisation, and nothing wider

Every element entering the store is dither-quantised with a per-column step recorded beside it. The execution bound answers a narrow question about that step: given inputs known only to within their quantisation, how far can the program’s output move?

The bound is conformal, built from K=63 draws, taking the m-th order statistic at level m/(K+1). Programs are placed into one of four tiers — linear-exact, smooth-first-order, branch-margin-guarded, or hard-refused — and a program that cannot be placed is refused rather than approximated.

Margin guards are evaluated per element. An aggregate margin is the wrong shape for this: a single benign element can pin it and defeat the safety factor for every other element in the batch. That was a real defect, not a hypothetical one, and the per-element form is the fix.

The coverage harness is a release gate rather than a diagnostic. A width falsifier has to assert that width tracks the actual perturbation, because a mutation that only ever widens a bound passes every coverage test while telling you nothing.

Where this sits against validated numerics

Arb, INTLAB, IntervalArithmetic.jl, CAPD, and Taylor-model implementations produce guaranteed enclosures across rounding, truncation, and discretisation. This bound does none of that and is not an alternative to them. It is a probabilistic statement about one error source, published with its scope attached. Describing it as a general-purpose enclosure would lose that comparison twice over.