phase_failure_accumulates_packaged
plain-language theorem explainer
This packages the accumulation of unresolved phase costs from failed gates into a single statement that accepts an abstract GateFailureCost structure for each gate. Researchers tracking phase budgets over finite gate collections cite it when costs arrive bundled with their positivity witness rather than as a raw function. The proof is a one-line wrapper that invokes the underlying accumulation theorem and extracts the required positivity from the structure field.
Claim. Let $S$ be a nonempty finite set of natural numbers. Suppose that for every $c$ in $S$ the gate at $c$ fails to hit the balanced square-budget phase, and that each such failure is equipped with a positive real cost via the GateFailureCost structure. Then the sum of these costs over $S$ is strictly positive.
background
GateFails holds precisely when a gate misses the balanced square-budget phase condition. GateFailureCost is the structure that pairs an arbitrary real cost with the witness that failure implies positivity of that cost; only the positivity field is used downstream. cumulativeFailureCost is the plain sum of the supplied cost function over the finite set $S$ (defined via Finset.sum). The module states that this is the second phase-budget theorem: failed finite gates contribute positive unresolved phase cost, and finite sums of those costs accumulate. The key upstream result is phase_failure_accumulates, which states the same conclusion but takes the positivity hypothesis as a separate forall rather than packaged inside the structure.
proof idea
The proof is a one-line wrapper. It applies phase_failure_accumulates to the nonempty set and the failure predicate, then supplies the positivity hypothesis by calling the positive_of_failure field of the GateFailureCost structure on each element of $S$.
why it matters
It supplies the packaged interface for the second phase-budget theorem, allowing higher-level arguments to carry costs as opaque structures rather than explicit functions. The parent accumulation result (phase_failure_accumulates) is the direct source; this wrapper closes the interface so that downstream phase-budget calculations can consume GateFailureCost without exposing the internal positivity witness. No open scaffolding remains for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.