no_unbounded_unresolved_phase_cost
plain-language theorem explainer
If an integer ledger maintains a finite nonnegative budget that upper-bounds the sum of unresolved phase costs over every finite gate set, then those cumulative costs cannot grow without bound. Researchers formalizing phase constraints within Recognition Science would reference this to confirm budget finiteness. The proof derives a contradiction by applying the bounding property to the budget value itself.
Claim. Let $n$ be a natural number and let $c:ℕ→ℝ$ be a cost function. Suppose there exists $B≥0$ such that the sum of $c(k)$ over every finite set $S$ is at most $B$. Then it is not the case that for every real $M$ there exists a finite set $S$ whose summed cost exceeds $M$.
background
The T1 Phase Budget Bound module contains three theorems on finite budgets for unresolved phases. The key definition is that of a stable integer ledger budget, which consists of a nonnegative real number together with the assertion that the cumulative failure cost, equal to the sum of the cost function over any finite collection of gates, never exceeds this number. This result is the third theorem in the module and relies on the explicit interface for the budget. Upstream definitions include the cumulative failure cost as the sum over the Finset and the structure encoding stability. The module keeps the physical budget as an explicit interface and derives consequences from it.
proof idea
The term proof begins by assuming the costs are unbounded. It then specializes the assumed universal quantifier to the budget value from the stable ledger, producing a finite set whose summed cost exceeds the budget. The final step applies the negation of the strict inequality to the bounding property, closing the contradiction.
why it matters
This theorem establishes that a stable budget in the T1 phase-budget setting rules out unbounded unresolved costs, completing the local finiteness argument. It aligns with the Recognition Science emphasis on finite budgets derived from the Recognition Composition Law. No immediate parent theorems are listed, leaving open how this bound integrates with mass or action calculations downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.