Ordered numerical witnesses for the complete construction grammar

Every existing RelationMinor.Construction internally supplies a checked ordered numerical witness on exactly its existing original-language Construction.gadget body. The recursion includes the enabling pin and disequality trees. No finite alphabet, body-occurrence, connectedness, degree, target-genus or external gadget-provider hypothesis is needed.

This is static numerical data. It does not identify this model with geometric embeddings, provide a native compiler or prove the full planar CSP dichotomy. The higher-arity CROSS and one-hot macro expansion, normalization and geometric source comparison remain separate tasks.

Main definitions

• Cslib.Logic.PL.CSP.RelationMinor.Construction.orderedWitness: exact-body witness.

noncomputable def Cslib.Logic.PL.CSP.RelationMinor.Construction.orderedWitness {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (c : Construction arity sem R) : Complexity.CSP.OrderedBoundary.GadgetWitness c.gadget

Every finite construction tree supplies a checked ordered numerical witness for exactly its existing PP interpreter. Enabling pin and disequality witnesses recurse to original atoms; no additional provider premise is present.

theorem Cslib.Logic.PL.CSP.RelationMinor.Available.nonempty_orderedGadget {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (h : Available arity sem R) : ∃ (g : PPGadget arity sem R), Nonempty (Complexity.CSP.OrderedBoundary.GadgetWitness g)

Availability supplies an actual original-language gadget together with its checked ordered numerical witness, without a finite-language or target-embedding assumption.