def definition def or abbrev

`bandwidthBudget`

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

formal statement (Lean)

  54def bandwidthBudget (t : ℕ) : ℕ := bitBandwidthPerCycle * t

Definition body.

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

bandwidthBudget_succ in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
bandwidthBudget_zero in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
certify_requires_budget in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
cycles_lower_bound in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
insufficient_budget_no_certify in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
npWorkload_pos in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
PvsNPFromBITCert in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
pvsNP_one_statement in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use

Lean names referenced from this declaration's body.

bitBandwidthPerCycle in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use