Internally realized disequality for selfdual languages missing a constant

The minimum-arity descent of [DK15], Lemma 3, printed pp. 437–438, is applied only to actual original-language gadgets with supplied checked boundaries. Every descent step uses the proved projection or adjacent-equality constructor. Common complement rules out the unary-pin outcome. The result supplies the original-language body and its full numerical ordered certificate internally, without assuming arbitrary pp planar closure.

The semantic descent adapts RelationMinor's existing constants argument by Erik Demaine; the actual-body closure and certificate reconstruction are original. This static existence result makes no uniform preprocessing, bare recognition or geometric-planarity assertion.

theorem Cslib.Complexity.CSP.OrderedBoundary.exists_disequality_of_common_not {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} (hnot : Logic.PL.CSP.HasPolymorphism arity sem fun (a : Fin 1 → Bool) => !a 0) (hfalse : ¬Logic.PL.CSP.HasPolymorphism arity sem fun (x : Fin 1 → Bool) => false) : ∃ (g : Logic.PL.CSP.PPGadget arity sem Logic.PL.CSP.RelationMinor.disequality), Nonempty (GadgetWitness g)

A common complement and failure of the false constant operation supply an actual original-language disequality gadget with an internally realized ordered numerical boundary. The alphabet need not be finite, and neither an enabling pin nor a pp/embedding oracle is assumed. The failed constant itself supplies a nonempty original relation.