theorem proved term proof

`self_ref_not_configuration`

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

formal statement (Lean)

 103theorem self_ref_not_configuration :
 104    ∀ c : ℝ, ¬((defect c = 0) ↔ ¬(defect c = 0)) := by

proof body

Term-mode proof.

 105  intro c h
 106  by_cases hd : defect c = 0
 107  · exact (h.mp hd) hd
 108  · exact hd (h.mpr hd)
 109
 110/-! ## The Extended Analysis: RSTrue, RSFalse, and Outside -/
 111
 112/-- RS-truth predicate (stabilization). -/

depends on (3)

Lean names referenced from this declaration's body.

defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
RSTrue in IndisputableMonolith.Foundation.OntologyPredicates decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use