2.29. Finite Crossover Gadget Semantics🔗

Cslib.BitString.cross equates opposite cyclic ports. Cslib.BitString.nearCross additionally accepts 0001 and 1110. Cslib.BitString.IsStandardizedInconsistent has exactly eight shapes. The literal Dvořák–Kupec Figure 1(a) gadget targets CROSS or NEAR-CROSS according to which optional complementary pairs occur:

open Cslib.BitString Cslib.Logic.PL.CSP.Crossover in
example : figureOneARelation (standardizedRelation true false false) =
    nearCross := figureOneARelation_standardized true false false

Cslib.Logic.PL.CSP.Crossover.figureOneAStandardized exposes the selected target as an ordinary primitive-positive gadget. Figure 1(b) then defines CROSS from NEAR-CROSS using one existential auxiliary:

open Cslib.BitString Cslib.Logic.PL.CSP.Crossover in
example : ∃ b, figureOneB.body.eval nearSem
    (Sum.elim ![false, true, false, true] b) = true :=
  (figureOneB.correct _).mp (by⊢ ![false, true, false, true] ∈ cross decideAll goals completed! 🐙)

Both bodies retain the source diagram's numbered port order and use guarded scope widths. These results concern finite semantics; geometric realization, planar substitution, hardness and a new native runtime certificate remain open.