Lemma: Agent18_KL2_20260911.disjoint_switch_invariance

For arbitrary six-colour masks d,a,b, disjointness of a and b implies that switching d by a preserves its entire intersection mask with b, and therefore preserves exactly-one membership in b. This is finite six-colour boundary algebra; it does not assert the existence of an actual graph path, a graph cover, universal KL2, or a proof of Berge–Fulkerson.

Exact formal statement

∀ (d a b : Agent18_KL2_20260911.Mask),
  Agent18_KL2_20260911.Disjoint a b →
    And (Eq.{1} (HAnd.hAnd.{0, 0, 0} (Agent18_KL2_20260911.switch d a) b) (HAnd.hAnd.{0, 0, 0} d b))
      (Iff (Agent18_KL2_20260911.Odd (Agent18_KL2_20260911.switch d a) b) (Agent18_KL2_20260911.Odd d b))

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

Environment availability: available.

Public JSON record