pith. machine review for the scientific record. sign in
structure definition def or abbrev

BoundedVisibilityEngine

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  46structure BoundedVisibilityEngine where
  47  bound : ℕ → ℕ
  48  costOf : ℕ → ℕ → ℝ
  49  stable :
  50    ∀ n : ℕ, NonIdentityReciprocal n → StableIntegerLedgerBudget n (costOf n)
  51  floor :
  52    ∀ n : ℕ, NonIdentityReciprocal n → KThetaFailureFloorHypothesis n (costOf n)
  53  visibility :
  54    ∀ n : ℕ, NonIdentityReciprocal n → BoundedFiniteQuotientPhaseVisibility n bound
  55
  56/-- A bounded visibility engine proves bounded phase visibility for every
  57nonidentity reciprocal ledger. -/

used by (4)

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

depends on (12)

Lean names referenced from this declaration's body.