phase_failure_accumulates
plain-language theorem explainer
Failed gates in a nonempty finite collection each carry positive cost, so their total unresolved phase cost is strictly positive. Number theorists and Recognition Science modelers cite this when establishing lower bounds on phase budget overruns from gate failures. The argument reduces directly to the standard fact that the sum of positive terms over a nonempty finite set is positive.
Claim. Let $S$ be a nonempty finite set of natural numbers. Suppose that for each $c$ in $S$ the gate fails to hit the balanced square-budget phase and that the assigned cost of $c$ is positive. Then the sum of those costs over $S$ is strictly positive.
background
The module develops the second phase-budget theorem: failed finite gates contribute positive unresolved phase cost, and finite sums of those costs accumulate. GateFails n c holds precisely when a gate does not hit the balanced square-budget phase. cumulativeFailureCost n costOf S is the finite sum of costOf values over the elements of S. The setting rests on the eight-tick phase definition, whose values are multiples of π/4.
proof idea
The proof is a one-line wrapper. It unfolds the definition of cumulativeFailureCost to expose the finite sum, then invokes the standard lemma that the sum of strictly positive reals over a nonempty finite set is positive.
why it matters
This theorem supplies the core positivity step for the packaged form phase_failure_accumulates_packaged that appears immediately downstream. It completes the second phase-budget theorem in the NumberTheory module and connects directly to the eight-tick octave (T7) through the imported phase definition. The result supports lower bounds on unresolved costs within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.