theorem proved term proof

`boundary_unreachable`

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

formal statement (Lean)

 266theorem boundary_unreachable :
 267    ∀ c : Config, c.value ≠ 0 := by

Term-mode proof.

 268  intro c
 269  exact ne_of_gt c.pos
 270
 271/-! ## Summary -/
 272
 273/-- Status report for Modal Geometry module. -/

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Config in IndisputableMonolith.Gravity.ILG decl_use
Status in IndisputableMonolith.Measurement.RSNative.Core decl_use
Config in IndisputableMonolith.Modal.Possibility decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use