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

Diverges

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)

  59def Diverges (c : ℝ) : Prop := ∀ C : ℝ, defect c > C

proof body

Definition body.

  60
  61/-! ## Self-Referential Stabilization Queries -/
  62
  63/-- A self-referential stabilization query is a configuration c that
  64    "encodes" the assertion "I do not stabilize."
  65
  66    The key property: c is "true" iff ¬Stabilizes(c).
  67
  68    We model this as: c has an associated "truth value" that is
  69    the negation of its stabilization status.
  70
  71    Formally: c is a SelfRefQuery if there exists a "decoder" function
  72    that maps c to the proposition ¬Stabilizes(c). -/

depends on (24)

Lean names referenced from this declaration's body.