IndisputableMonolith.NumberTheory.T1PhaseBudgetBound

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.PhaseFailureCost
   3
   4/-!
   5# T1 Phase Budget Bound
   6
   7The third phase-budget theorem: a stable integer ledger with a finite T1/RCL
   8budget cannot carry unbounded unresolved finite-phase cost.
   9
  10The physical budget itself is kept as an explicit interface.  The theorems
  11below prove what follows from that interface without hiding the assumption.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace NumberTheory
  16namespace T1PhaseBudgetBound
  17
  18open PhaseFailureCost
  19open scoped BigOperators
  20
  21/-- A stable ledger budget bounds all finite unresolved phase-cost sums. -/
  22structure StableIntegerLedgerBudget (n : ℕ) (costOf : ℕ → ℝ) where
  23  budget : ℝ
  24  budget_nonneg : 0 ≤ budget
  25  bounds_all_finite_failures :
  26    ∀ S : Finset ℕ, cumulativeFailureCost n costOf S ≤ budget
  27
  28/-- A stable budget rules out unbounded unresolved finite-phase cost. -/
  29theorem no_unbounded_unresolved_phase_cost
  30    {n : ℕ} {costOf : ℕ → ℝ}
  31    (stable : StableIntegerLedgerBudget n costOf) :
  32    ¬ (∀ B : ℝ, ∃ S : Finset ℕ, B < cumulativeFailureCost n costOf S) := by
  33  intro hunbounded
  34  rcases hunbounded stable.budget with ⟨S, hS⟩
  35  exact not_lt_of_ge (stable.bounds_all_finite_failures S) hS
  36
  37/-- A uniform positive floor for failed gates in a finite set. -/
  38def UniformFailureFloor (n : ℕ) (costOf : ℕ → ℝ) (S : Finset ℕ) (δ : ℝ) : Prop :=
  39  0 < δ ∧
  40  (∀ c ∈ S, GateFails n c) ∧
  41  (∀ c ∈ S, δ ≤ costOf c)
  42
  43/-- If all gates in `S` fail with a uniform floor `δ`, the stable budget bounds
  44the size of `S`. -/
  45theorem failed_gate_count_bounded_by_budget
  46    {n : ℕ} {costOf : ℕ → ℝ} {S : Finset ℕ} {δ : ℝ}
  47    (stable : StableIntegerLedgerBudget n costOf)
  48    (floor : UniformFailureFloor n costOf S δ) :
  49    δ * (S.card : ℝ) ≤ stable.budget := by
  50  have hlower :=
  51    phase_failure_cost_lower_bound
  52      (n := n) (S := S) (costOf := costOf) (δ := δ)
  53      floor.2.1 floor.2.2
  54  exact le_trans hlower (stable.bounds_all_finite_failures S)
  55
  56end T1PhaseBudgetBound
  57end NumberTheory
  58end IndisputableMonolith
  59