`past_theorem`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.InitialCondition
domain: Foundation
line: 149 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.InitialCondition on GitHub at line 149.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 146
 147    Answer: Because thermal equilibrium (maximum defect) is infinitely
 148    costly, while the zero-defect state is the unique cost minimum. -/
 149theorem past_theorem {N : ℕ} (hN : 0 < N) :
 150    (∃! c : Configuration N, total_defect c = 0) ∧
 151    total_defect (unity_config N hN) = 0 ∧
 152    (∀ c : Configuration N, total_defect (unity_config N hN) ≤ total_defect c) := by
 153  refine ⟨⟨unity_config N hN, unity_defect_zero hN, ?_⟩, unity_defect_zero hN,
 154    unity_is_global_minimum hN⟩
 155  intro c hc
 156  have h_entries : ∀ i, c.entries i = 1 :=
 157    (zero_defect_iff_unity hN c).mp hc
 158  have h_u_entries : ∀ i, (unity_config N hN).entries i = 1 := fun _ => rfl
 159  have h_eq : c.entries = (unity_config N hN).entries :=
 160    funext fun i => by rw [h_entries i, h_u_entries i]
 161  exact Configuration.mk.injEq .. |>.mpr h_eq
 162
 163end InitialCondition
 164end Foundation
 165end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.