def definition def or abbrev

`cumulativeFailureCost`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  29def cumulativeFailureCost (_n : ℕ) (costOf : ℕ → ℝ) (S : Finset ℕ) : ℝ :=

proof body

Definition body.

  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. -/

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

phase_failure_accumulates in IndisputableMonolith.NumberTheory.PhaseFailureCost decl_use
phase_failure_accumulates_packaged in IndisputableMonolith.NumberTheory.PhaseFailureCost decl_use
phase_failure_cost_lower_bound in IndisputableMonolith.NumberTheory.PhaseFailureCost decl_use
no_unbounded_unresolved_phase_cost in IndisputableMonolith.NumberTheory.T1PhaseBudgetBound decl_use
StableIntegerLedgerBudget in IndisputableMonolith.NumberTheory.T1PhaseBudgetBound decl_use
hits_balanced_phase_of_floor_and_budget in IndisputableMonolith.NumberTheory.VisibilityFromFloorBudget decl_use

depends on (9)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use