Documentation

CslibFrontier.Logics.Propositional.CSP.Planar.Embedding.AttachmentLabels

Exact labels for attaching a two-port body #

One selected external port shares the chosen old coordinate. The other is a fresh last free coordinate. Old auxiliary blocks are concatenated in their original order. The proved kernel identifies exactly the selected pair and retains every other label.

source
def Cslib.Complexity.CSP.OrderedBoundary.attachPortLabel (k a b : ℕ) (j : Fin k) (t : Fin 2) :
(Fin k ⊕ Fin a) ⊕ Fin 2 ⊕ Fin b → Fin (k + 1) ⊕ Fin (a + b)

Retain old free indices by castSucc, share external port t with old j, and put the other external port last. Left auxiliaries precede the right auxiliary block.

Instances For
    source
    theorem Cslib.Complexity.CSP.OrderedBoundary.attachPortLabel_kernel (k a b : ℕ) (j : Fin k) (t : Fin 2) (u v : (Fin k ⊕ Fin a) ⊕ Fin 2 ⊕ Fin b) :
    attachPortLabel k a b j t u = attachPortLabel k a b j t v ↔ Function.update id (Sum.inl (Sum.inl j)) (Sum.inr (Sum.inl t)) u = Function.update id (Sum.inl (Sum.inl j)) (Sum.inr (Sum.inl t)) v

    The actual source-variable kernel is precisely the selected pair. All other free and auxiliary labels remain distinct, independently of which labels occur in either body.