failed_gate_count_bounded_by_budget
plain-language theorem explainer
A stable integer ledger budget upper-bounds the total unresolved phase cost of any finite set of gates that each fail at or above a uniform positive threshold δ. Researchers modeling phase-failure constraints within Recognition Science cite the result to enforce finite failure counts under an explicit budget interface. The proof obtains the lower bound δ ⋅ |S| on cumulative failure cost and chains it by transitivity to the budget upper bound.
Claim. Suppose a stable integer ledger supplies a nonnegative budget $B$ that upper-bounds the cumulative failure cost of every finite set of gates. Suppose further that every gate in a finite set $S$ fails and incurs cost at least some fixed positive real number δ. Then δ ⋅ |S| ≤ B.
background
The T1 Phase Budget Bound module shows that a stable integer ledger with finite T1/RCL budget cannot carry unbounded unresolved finite-phase cost. The central interface is the StableIntegerLedgerBudget structure, which packages a nonnegative real budget together with the assertion that this budget upper-bounds cumulativeFailureCost n costOf S for every finite set S. The companion predicate UniformFailureFloor requires δ > 0, that every gate in S fails, and that each such gate costs at least δ.
proof idea
The proof first calls phase_failure_cost_lower_bound on the failure and cost-lower-bound data inside the UniformFailureFloor hypothesis, yielding δ ⋅ |S| ≤ cumulativeFailureCost n costOf S. It then applies le_trans to combine this lower bound with the budget upper bound supplied by the StableIntegerLedgerBudget hypothesis.
why it matters
The theorem supplies the third phase-budget result in the T1 series, confirming that a stable budget rules out unbounded unresolved finite-phase cost. It is invoked directly by the downstream theorem failed_gate_count_bounded_at_KTheta, which specializes the same bound to the KTheta floor hypothesis. Within the Recognition Science framework the result constrains total defect cost inside the eight-tick octave and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.