Lemma: Agent18_KL2_20260911.relevant_switch

If d and a are duads with exactly one common colour, switching d by a yields another duad different from d. 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 : Agent18_KL2_20260911.Mask),
  Agent18_KL2_20260911.IsDuad d →
    Agent18_KL2_20260911.IsDuad a →
      Agent18_KL2_20260911.Odd d a →
        And (Agent18_KL2_20260911.IsDuad (Agent18_KL2_20260911.switch d a)) (Ne.{1} (Agent18_KL2_20260911.switch d a) d)

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

Environment availability: available.

Public JSON record