Ordered certificates and a trailing isolated constraint center

A trailing nullary constraint adds a declared point and no darts. The actual componentwise numerical convention accepts that point separately; the supplied table and all original argument rotations are retained. This is structural and does not erase the nullary relation from satisfiability semantics.

theorem Cslib.Complexity.CSP.incidenceGraph_append_nullary {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) : incidenceGraph (F ++ [(r, [])]) = { vertices := (incidenceGraph F).vertices ++ [F.numVars + List.length F], edges := (incidenceGraph F).edges }

A trailing nullary adds exactly one isolated constraint declaration.

theorem Cslib.Complexity.CSP.scopeLength_append_nullary {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) (i : ℕ) : scopeLength (F ++ [(r, [])]) i = scopeLength F i

The extra zero-width entry agrees even with the length reader's missing-entry default.

theorem Cslib.Complexity.CSP.verifyArgumentOrder_append_nullary {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) (c : Graph.RotationCertificate) : verifyArgumentOrder (F ++ [(r, [])]) c = verifyArgumentOrder F c

Every original clockwise argument successor is unchanged on the very same raw table.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_append_nullary {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (c : Graph.RotationCertificate) : verifyRotationCertificate (F ++ [(r, [])]) c = verifyRotationCertificate F c

Appending or removing an isolated nullary constraint retains the exact accepted raw ordered numerical certificate. Its truth value under relation semantics is not asserted.