Job sequencing is in NP

The bridge between the kernel of DescriptiveComplexity.Problems.JobSequencing.Kernel and what it means: DescriptiveComplexity.realize_jobSequencingKernel reads each clause back as a statement about the guessed relations, so that the two directions of the Σ₁ definition can be argued with DescriptiveComplexity.chain_sound and DescriptiveComplexity.exists_chain for the walks and DescriptiveComplexity.binNum_lt_iff for the two comparisons.

theorem DescriptiveComplexity.realize_jobSequencingKernel {A : Type} [FirstOrder.Language.jobSeq.Structure A] (ρ : jobSeqGuessBlock.Assignment A) : A ⊨ jobSequencingKernel ↔ (IsLinOrd JSLe ∧ IsLinOrd (JSched ρ)) ∧ (∀ (j : A), JLate ρ j → JSJob j) ∧ (∀ (s : Bool), (∀ (i x p : A), MinPos (JOrd ρ s) JSJob i → JSPosn p → (JPS ρ s i (x, p) ↔ ChainAdd (JSel ρ s) (JWt s) i (x, p))) ∧ (∀ (i j x p : A), SuccPos (JOrd ρ s) JSJob i j → JSPosn p → (JPS ρ s j (x, p) ↔ (JPS ρ s i (x, p) ↔ (ChainAdd (JSel ρ s) (JWt s) j (x, p) ↔ JCy ρ s j (x, p))))) ∧ (∀ (i j x p y q : A), SuccPos (JOrd ρ s) JSJob i j → x = y ∧ SuccPos JSLe JSPosn p q ∨ SuccPos JSLe (fun (x : A) => True) x y ∧ MaxPos JSLe JSPosn p ∧ MinPos JSLe JSPosn q → (JCy ρ s j (y, q) ↔ maj (JPS ρ s i (x, p)) (ChainAdd (JSel ρ s) (JWt s) j (x, p)) (JCy ρ s j (x, p)))) ∧ (∀ (i j x p : A), SuccPos (JOrd ρ s) JSJob i j → (∀ (y : A), JSLe x y) ∧ MinPos JSLe JSPosn p → ¬JCy ρ s j (x, p)) ∧ ∀ (i j x p : A), SuccPos (JOrd ρ s) JSJob i j → (∀ (y : A), JSLe y x) ∧ MaxPos JSLe JSPosn p → ¬maj (JPS ρ s i (x, p)) (ChainAdd (JSel ρ s) (JWt s) j (x, p)) (JCy ρ s j (x, p))) ∧ (∀ (j : A), JSJob j → (JLate ρ j ↔ ∃ (x : A) (p : A), JSPosn p ∧ ¬JDlineW j (x, p) ∧ JPS ρ true j (x, p) ∧ ∀ (y q : A), JSPosn q → (JSLe x y ∧ ¬x = y ∨ x = y ∧ JSLe p q) ∧ (¬y = x ∨ ¬q = p) → (JDlineW j (y, q) ↔ JPS ρ true j (y, q)))) ∧ ∀ (j : A), MaxPos JSLe JSJob j → ¬∃ (x : A) (p : A), JSPosn p ∧ ¬JBndW (x, p) ∧ JPS ρ false j (x, p) ∧ ∀ (y q : A), JSPosn q → (JSLe x y ∧ ¬x = y ∨ x = y ∧ JSLe p q) ∧ (¬y = x ∨ ¬q = p) → (JBndW (y, q) ↔ JPS ρ false j (y, q))

Reading the comparisons back

theorem DescriptiveComplexity.binNum_wide_lt_iff {A : Type} [Finite A] [FirstOrder.Language.jobSeq.Structure A] (hlin : IsLinOrd JSLe) (b b' : A × A → Prop) : binNum (wideLe JSLe) (WidePosn JSPosn) b < binNum (wideLe JSLe) (WidePosn JSPosn) b' ↔ ∃ (x : A) (p : A), JSPosn p ∧ ¬b (x, p) ∧ b' (x, p) ∧ ∀ (y q : A), JSPosn q → (JSLe x y ∧ ¬x = y ∨ x = y ∧ JSLe p q) ∧ (¬y = x ∨ ¬q = p) → (b (y, q) ↔ b' (y, q))

The comparison clauses say what they should: the shape the kernel writes – two wide positions, the second strictly above the first written out coordinate by coordinate – is DescriptiveComplexity.binNum_lt_iff on the wide positions. Both comparisons of the kernel go through this, the deadline against a completion time and the bound against the penalty total.

Membership

theorem DescriptiveComplexity.jobSequencing_sigmaSODefinable : SigmaSODefinable 1 JobSequencing

Job sequencing is Σ₁-definable: guess the schedule, the late jobs, the completion times along the schedule and the penalty total of the late jobs, and check first-order that both are ripple-carry additions, that a job is late exactly when its completion time exceeds its deadline, and that the penalty total does not exceed the bound. Since NP is defined as Σ₁-definability, this is the membership half of job sequencing.