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)
112theorem total_defect_nonneg' {N : ℕ} (c : Configuration N) :
113 0 ≤ total_defect c := total_defect_nonneg c
proof body
Term-mode proof.
114
115/-! ## Uniform candidate and Jensen helpers -/
116
117/-- Constant-entry configuration with value `exp μ` in every slot. -/
depends on (6)
Lean names referenced from this declaration's body.
-
Configuration
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
total_defect
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
total_defect_nonneg
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
Configuration
in IndisputableMonolith.Foundation.RecognitionForcing
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use