Raw argument-order checks depend only on constraint-end lookups #
The original positional argument-order checker reads only the odd entry for each actual occurrence. Agreement on these entries preserves its complete Boolean result, even for malformed tables. This original table identity makes no rotation or genus assertion.
theorem Cslib.Complexity.CSP.verifyArgumentOrder_congr {Rel V : Type} (F : Logic.PL.CSP Rel V) (c d : Graph.RotationCertificate) (h : ∀ i < F.occurrences.length, c.successor.getD (2 * i + 1) 0 = d.successor.getD (2 * i + 1) 0) :
Agreement at every actual constraint-end position preserves the exact argument-order check, without a wellformedness or certificate-length premise. Variable-end entries and out-of-range entries are unrestricted.