phase_failure_accumulates
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not supply an explicit formula for the cost function beyond positivity.
- Does not extend the claim to infinite collections of gates.
- Does not quantify the size of the total cost beyond strict positivity.
- Does not address n-dependent scaling or interactions among distinct phases.
formal statement (Lean)
34theorem phase_failure_accumulates
35 {n : ℕ} {S : Finset ℕ} {costOf : ℕ → ℝ}
36 (hS : S.Nonempty)
37 (_hfails : ∀ c ∈ S, GateFails n c)
38 (hpos : ∀ c ∈ S, 0 < costOf c) :
39 0 < cumulativeFailureCost n costOf S := by
proof body
Term-mode proof.
40 unfold cumulativeFailureCost
41 exact Finset.sum_pos hpos hS
42
43/-- Lower bound: if every failed gate in `S` costs at least `δ`, then the
44total unresolved phase cost is at least `δ * S.card`. -/