phase_failure_cost_lower_bound
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that any individual cost is positive without the GateFails premise.
- Does not assume a concrete functional form for costOf beyond the uniform lower bound δ.
- Does not extend the inequality to infinite collections of gates.
- Does not connect the numerical bound to Recognition Science constants such as phi or the alpha band.
formal statement (Lean)
45theorem phase_failure_cost_lower_bound
46 {n : ℕ} {S : Finset ℕ} {costOf : ℕ → ℝ} {δ : ℝ}
47 (_hfails : ∀ c ∈ S, GateFails n c)
48 (hlower : ∀ c ∈ S, δ ≤ costOf c) :
49 δ * (S.card : ℝ) ≤ cumulativeFailureCost n costOf S := by
proof body
Tactic-mode proof.
50 unfold cumulativeFailureCost
51 calc
52 δ * (S.card : ℝ) = S.sum (fun _ => δ) := by simp; ring
53 _ ≤ S.sum costOf := Finset.sum_le_sum hlower
54
55/-- Packaged form using `GateFailureCost`. -/