phase_failure_cost_lower_bound
plain-language theorem explainer
If every gate in a finite set S fails to hit the balanced phase and carries cost at least δ, the total unresolved phase cost is at least δ times the cardinality of S. Phase-budget arguments in the Recognition Science number-theory layer cite this to control the size of failing gate collections. The proof rewrites the left-hand side as a uniform sum and invokes monotonicity of finite summation.
Claim. Let $S$ be a finite set of natural numbers. Suppose that for every $c$ in $S$ the gate fails to hit the balanced square-budget phase (i.e., $¬$HitsBalancedPhase$(n,c)$) and that costOf$(c) ≥ δ$. Then $δ · |S| ≤ ∑_{c∈S}$ costOf$(c)$.
background
The module PhaseFailureCost develops the second phase-budget theorem: failed finite gates contribute positive unresolved phase cost and these costs accumulate under finite summation. GateFails n c is the proposition that gate c does not hit the balanced square-budget phase for parameter n. cumulativeFailureCost n costOf S is defined simply as the sum of costOf over the elements of S. The theorem therefore supplies a uniform lower bound on that sum once a common floor δ is given for every failing gate.
proof idea
The tactic proof unfolds the definition of cumulativeFailureCost, rewrites δ times the cardinality of S as the sum of the constant δ over S, and applies Finset.sum_le_sum to the hypothesis that every cost is at least δ.
why it matters
The lower bound is invoked directly by failed_gate_count_bounded_by_budget to conclude that a stable integer ledger budget limits the number of failing gates, and it supports the visibility result hits_balanced_phase_of_floor_and_budget that guarantees at least one admissible gate succeeds. It therefore closes the accumulation step required for the phase-budget theorems that keep unresolved costs finite inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.