Lemma: Agent18_KL2_20260911.two_switch_necessity

Starting with boundary (d,d,e,e), let a,b,d,e be duads. If the first switch uses any cross e/f endpoint pair and a is relevant for both d and e, the second switch uses any two distinct endpoints each having exactly-one membership in b at the intermediate boundary, and the final boundary has both aligned pairs disjoint, then a and b are disjoint, b is relevant for the original d and e, and the second pair also crosses e/f. The second e-end may repeat the first e-end. 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 e a b : Agent18_KL2_20260911.Mask) (i j k l : Agent18_KL2_20260911.Arm),
  Agent18_KL2_20260911.IsDuad d →
    Agent18_KL2_20260911.IsDuad e →
      Agent18_KL2_20260911.IsDuad a →
        Agent18_KL2_20260911.IsDuad b →
          Agent18_KL2_20260911.Cross i j →
            Agent18_KL2_20260911.Relevant d e a →
              Agent18_KL2_20260911.Legal (Agent18_KL2_20260911.pathSwitch (Agent18_KL2_20260911.initial d e) a i j) b k
                  l →
                Agent18_KL2_20260911.K1
                    (Agent18_KL2_20260911.pathSwitch
                      (Agent18_KL2_20260911.pathSwitch (Agent18_KL2_20260911.initial d e) a i j) b k l) →
                  And (Agent18_KL2_20260911.Disjoint a b)
                    (And (Agent18_KL2_20260911.Relevant d e b) (Agent18_KL2_20260911.Cross k l))

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

Environment availability: available.

Public JSON record