cumulativeFailureCost
plain-language theorem explainer
cumulativeFailureCost defines the total unresolved phase cost over any finite gate set S as the sum of per-gate costs supplied by costOf. Phase-budget researchers cite it when establishing accumulation of positive failure costs or when proving ledger stability bounds. The definition is a direct one-line abbreviation that applies the standard finite-set summation operator.
Claim. For a natural number $n$, a cost function $costOf : ℕ → ℝ$, and a finite set $S ⊆ ℕ$, the cumulative unresolved phase cost is $∑_{c ∈ S} costOf(c)$.
background
The Phase Failure Cost module develops the second phase-budget theorem: failed finite gates contribute positive unresolved phase cost, and finite sums of those costs accumulate. The cost function costOf is supplied externally and is typically the J-cost induced by a multiplicative recognizer or a recognition event. Upstream definitions include the cost map from MultiplicativeRecognizerL4 (derived cost of the comparator on positive ratios) and the cost map from ObserverForcing (J-cost of the recognition-event state).
proof idea
This is a direct definition that unfolds to the sum of costOf over the elements of S via Finset.sum.
why it matters
The definition supplies the accumulation operator used by the phase-failure-accumulates theorem, the lower-bound theorem, the StableIntegerLedgerBudget structure, and the no-unbounded-unresolved-phase-cost result. It thereby closes the finite-sum step of the second phase-budget theorem and feeds the visibility-from-floor-budget lemma that produces a balanced-phase hit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.