cumulativeFailureCost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assume individual costs are positive.
- Does not restrict the form of the cost function costOf.
- Does not address infinite collections of gates.
- Does not compute numerical values for any concrete costOf.
formal statement (Lean)
29def cumulativeFailureCost (_n : ℕ) (costOf : ℕ → ℝ) (S : Finset ℕ) : ℝ :=
proof body
Definition body.
30 S.sum costOf
31
32/-- If every gate in a nonempty finite set fails and each failed gate has
33positive cost, then the cumulative cost is positive. -/