structure definition def or abbrev

`StableIntegerLedgerBudget`

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

formal statement (Lean)

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

used by (6)

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

BoundedVisibilityEngine in IndisputableMonolith.NumberTheory.BoundedPhaseVisibility decl_use
failed_gate_count_bounded_at_KTheta in IndisputableMonolith.NumberTheory.BoundedPhaseVisibility decl_use
MinimalEngine in IndisputableMonolith.NumberTheory.MinimalVisibilityEngine decl_use
failed_gate_count_bounded_by_budget in IndisputableMonolith.NumberTheory.T1PhaseBudgetBound decl_use
no_unbounded_unresolved_phase_cost 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.

phase in IndisputableMonolith.Foundation.EightTick decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
cumulativeFailureCost in IndisputableMonolith.NumberTheory.PhaseFailureCost decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use