Lemma: Agent18_KL2_20260911.two_switch_sufficiency
Starting with boundary (d,d,e,e), if a and b are disjoint duads each relevant for both original duads, then for every first e-end i and first f-end j and every second f-end l, the first switch is legal, switching b between the other e-end (i xor 1) and l is legal in the intermediate boundary, and the final boundary lies in K1. This covers both possible actual second f-ends, including when l=j. 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 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 →
LT.lt.{0} i 2 →
LE.le.{0} 2 j →
LE.le.{0} 2 l →
Agent18_KL2_20260911.Relevant d e a →
Agent18_KL2_20260911.Relevant d e b →
Agent18_KL2_20260911.Disjoint a b →
And (Agent18_KL2_20260911.Legal (Agent18_KL2_20260911.initial d e) a i j)
(And
(Agent18_KL2_20260911.Legal
(Agent18_KL2_20260911.pathSwitch (Agent18_KL2_20260911.initial d e) a i j) b
(HXor.hXor.{0, 0, 0} i 1) l)
(Agent18_KL2_20260911.K1
(Agent18_KL2_20260911.pathSwitch
(Agent18_KL2_20260911.pathSwitch (Agent18_KL2_20260911.initial d e) a i j) b
(HXor.hXor.{0, 0, 0} i 1) l)))This is a published formal lemma. Its scope is the exact statement above.
Environment availability: available.