Lemma: Agent18_KL2_20260911.disjoint_relevant_outputs

For a duad d and two disjoint duads a,b each meeting d in exactly one colour, switching opposite copies of d by a and b yields disjoint outputs; applying both switches to one copy and neither to the other also yields disjoint outputs. 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.IsDuad d →
    Agent18_KL2_20260911.IsDuad a →
      Agent18_KL2_20260911.IsDuad b →
        Agent18_KL2_20260911.Disjoint a b →
          Agent18_KL2_20260911.Odd d a →
            Agent18_KL2_20260911.Odd d b →
              And (Agent18_KL2_20260911.Disjoint (Agent18_KL2_20260911.switch d a) (Agent18_KL2_20260911.switch d b))
                (Agent18_KL2_20260911.Disjoint (Agent18_KL2_20260911.switch (Agent18_KL2_20260911.switch d a) b) d)

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

Environment availability: available.

Public JSON record