IndisputableMonolith.NumberTheory.PhaseFailureCost

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase
   3
   4/-!
   5# Phase Failure Cost
   6
   7The second phase-budget theorem: failed finite gates contribute positive
   8unresolved phase cost, and finite sums of those costs accumulate.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace NumberTheory
  13namespace PhaseFailureCost
  14
  15open ErdosStrausBoxPhase
  16open scoped BigOperators
  17
  18/-- A gate fails when it does not hit the balanced square-budget phase. -/
  19def GateFails (n c : ℕ) : Prop :=
  20  ¬ HitsBalancedPhase n c
  21
  22/-- An abstract cost assignment for a failed gate.  The positivity field is
  23the only property needed for the finite accumulation theorems. -/
  24structure GateFailureCost (n c : ℕ) where
  25  cost : ℝ
  26  positive_of_failure : GateFails n c → 0 < cost
  27
  28/-- Cumulative unresolved phase cost over a finite gate set. -/
  29def cumulativeFailureCost (_n : ℕ) (costOf : ℕ → ℝ) (S : Finset ℕ) : ℝ :=
  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. -/
  34theorem phase_failure_accumulates
  35    {n : ℕ} {S : Finset ℕ} {costOf : ℕ → ℝ}
  36    (hS : S.Nonempty)
  37    (_hfails : ∀ c ∈ S, GateFails n c)
  38    (hpos : ∀ c ∈ S, 0 < costOf c) :
  39    0 < cumulativeFailureCost n costOf S := by
  40  unfold cumulativeFailureCost
  41  exact Finset.sum_pos hpos hS
  42
  43/-- Lower bound: if every failed gate in `S` costs at least `δ`, then the
  44total unresolved phase cost is at least `δ * S.card`. -/
  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
  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`. -/
  56theorem phase_failure_accumulates_packaged
  57    {n : ℕ} {S : Finset ℕ} {failure : ∀ c : ℕ, GateFailureCost n c}
  58    (hS : S.Nonempty)
  59    (hfails : ∀ c ∈ S, GateFails n c) :
  60    0 < cumulativeFailureCost n (fun c => (failure c).cost) S := by
  61  apply phase_failure_accumulates hS hfails
  62  intro c hc
  63  exact (failure c).positive_of_failure (hfails c hc)
  64
  65end PhaseFailureCost
  66end NumberTheory
  67end IndisputableMonolith
  68