pith. machine review for the scientific record. sign in
theorem proved term proof

ground_state_recognition_impossible

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)

 177theorem ground_state_recognition_impossible {N : ℕ} (hN : 0 < N) :
 178    ¬ T4_Recognition (InitialCondition.unity_config N hN) := by

proof body

Term-mode proof.

 179  intro ⟨⟨i, hi⟩⟩
 180  simp only [InitialCondition.unity_config] at hi
 181  exact hi rfl
 182
 183/-- **Static Ground State Impossible**: No configuration can simultaneously
 184    have zero total defect (forcing all entries to 1) AND support
 185    recognition (forcing at least one entry ≠ 1). -/

used by (2)

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

depends on (15)

Lean names referenced from this declaration's body.