Lemma: Agent18_HellyLoads_20260911.six_load_uniqueness

Local arithmetic for the six-witness case of the BF-cover Helly proof: for functions w,n : Fin 6 → Nat, if every n(i) is at most one and n(i)+sum_j w(j)=2+w(i) for each i, then n=w pointwise and sum_j w(j)=2. This verifies the physical-edge load step, not graph realization or the full Helly theorem.

Exact formal statement

∀ (w n : Fin 6 → Nat),
  (∀ (i : Fin 6), LE.le.{0} (n i) 1) →
    (∀ (i : Fin 6),
        Eq.{1} (HAdd.hAdd.{0, 0, 0} (n i) (Finset.sum.{0, 0} Finset.univ.{0} fun i => w i))
          (HAdd.hAdd.{0, 0, 0} 2 (w i))) →
      And (Eq.{1} n w) (Eq.{1} (Finset.sum.{0, 0} Finset.univ.{0} fun i => w i) 2)

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

Environment availability: available.

Public JSON record