Lemma: Agent18_HellyLoads_20260911.seven_load_impossible

Local arithmetic excluding seven omitted witnesses: there is no w : Fin 7 → Nat satisfying sum_j w(j)=2+w(i) for every i. In the BF-cover Helly argument these are the load equations at one physical edge; the graph matching/cover reduction is not formalized by this lemma.

Exact formal statement

∀ (w : Fin 7 → Nat),
  (∀ (i : Fin 7), Eq.{1} (Finset.sum.{0, 0} Finset.univ.{0} fun j => w j) (HAdd.hAdd.{0, 0, 0} 2 (w i))) → False

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.

Public JSON record