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

SelfRefQuery

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)

  73structure SelfRefQuery where
  74  /-- The configuration -/
  75  config : ℝ
  76  /-- The self-referential property: c encodes "I don't stabilize" -/
  77  self_ref : (defect config = 0) ↔ ¬(defect config = 0)
  78
  79/-- **THEOREM 1**: Self-referential stabilization queries are contradictory.
  80
  81    If c encodes "c ⟺ ¬Stab(c)", then assuming c has any definite
  82    stabilization status leads to contradiction.
  83
  84    This is the heart of the Gödel dissolution: such c cannot exist
  85    as consistent configurations. -/

used by (4)

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

depends on (16)

Lean names referenced from this declaration's body.