The certificate of job sequencing

The syntax of the Σ₁ definition of DescriptiveComplexity.JobSequencing: the existential block and the first-order kernel. What is guessed is

• sched, the schedule – a binary relation the kernel forces to be a linear order, which on a finite universe is a permutation;
• late, the jobs that miss their deadline;
• ps s and cy s, the running totals and the carries of two walks: at s = true the completion times, walking the jobs along sched and adding execution times, and at s = false the penalties of the late jobs, walking them along the instance's own order.

Both walks run on the wide positions of DescriptiveComplexity.Numbers.Wide, since a completion time is a sum of every execution time and a penalty total a sum of every penalty; neither need fit where the instance writes. They are the same five clauses read twice, so the clause family is a function of s, as in DescriptiveComplexity.Problems.Partition.Membership.

What is new here, and what job sequencing needs that no earlier problem did, is comparing two numbers rather than adding them: a job is late when its deadline is smaller than its completion time, and the schedule is good when the bound is not smaller than the penalty total. Both are written by the highest differing position (DescriptiveComplexity.binNum_lt_iff), the deadline and the bound being read on the wide positions through their lowest block (DescriptiveComplexity.binNum_wide_bot).

The existential block

inductive DescriptiveComplexity.JIdx : Type

The relation variables of the certificate: the schedule, the late jobs, and the running totals and carries of the two walks.

• sched : JIdx

  The schedule.

• late : JIdx

  The jobs that miss their deadline.

• ps (s : Bool) : JIdx

  The running total of the walk s.

• cy (s : Bool) : JIdx

  The carries of the walk s.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqJIdx : DecidableEq JIdx

Equations

• DescriptiveComplexity.instDecidableEqJIdx = DescriptiveComplexity.instDecidableEqJIdx.decEq

def DescriptiveComplexity.instDecidableEqJIdx.decEq (x✝ x✝¹ : JIdx) : Decidable (x✝ = x✝¹)

Equations

• DescriptiveComplexity.instDecidableEqJIdx.decEq DescriptiveComplexity.JIdx.sched DescriptiveComplexity.JIdx.sched = isTrue ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq DescriptiveComplexity.JIdx.sched DescriptiveComplexity.JIdx.late = isFalse DescriptiveComplexity.instDecidableEqJIdx.decEq._proof_1
• DescriptiveComplexity.instDecidableEqJIdx.decEq DescriptiveComplexity.JIdx.sched (DescriptiveComplexity.JIdx.ps s) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq DescriptiveComplexity.JIdx.sched (DescriptiveComplexity.JIdx.cy s) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq DescriptiveComplexity.JIdx.late DescriptiveComplexity.JIdx.sched = isFalse DescriptiveComplexity.instDecidableEqJIdx.decEq._proof_4
• DescriptiveComplexity.instDecidableEqJIdx.decEq DescriptiveComplexity.JIdx.late DescriptiveComplexity.JIdx.late = isTrue ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq DescriptiveComplexity.JIdx.late (DescriptiveComplexity.JIdx.ps s) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq DescriptiveComplexity.JIdx.late (DescriptiveComplexity.JIdx.cy s) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq (DescriptiveComplexity.JIdx.ps s) DescriptiveComplexity.JIdx.sched = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq (DescriptiveComplexity.JIdx.ps s) DescriptiveComplexity.JIdx.late = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq (DescriptiveComplexity.JIdx.ps a) (DescriptiveComplexity.JIdx.ps b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq (DescriptiveComplexity.JIdx.ps s) (DescriptiveComplexity.JIdx.cy s_1) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq (DescriptiveComplexity.JIdx.cy s) DescriptiveComplexity.JIdx.sched = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq (DescriptiveComplexity.JIdx.cy s) DescriptiveComplexity.JIdx.late = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq (DescriptiveComplexity.JIdx.cy s) (DescriptiveComplexity.JIdx.ps s_1) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqJIdx.decEq (DescriptiveComplexity.JIdx.cy a) (DescriptiveComplexity.JIdx.cy b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.instFintypeJIdx : Fintype JIdx

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.jobSeqGuessBlock : SOBlock

The single existential block of the Σ₁ definition of job sequencing: the schedule (binary), the late jobs (unary), and, for each walk, the running totals and the carries (ternary: a job and a wide position, itself a pair).

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.jqSchedRel : jobSeqGuessBlock.lang.Relations 2

The symbol of the schedule relation variable.

Equations

• DescriptiveComplexity.jqSchedRel = ⟨DescriptiveComplexity.JIdx.sched, DescriptiveComplexity.jqSchedRel._proof_1⟩

def DescriptiveComplexity.jqLateRel : jobSeqGuessBlock.lang.Relations 1

The symbol of the late-jobs relation variable.

Equations

• DescriptiveComplexity.jqLateRel = ⟨DescriptiveComplexity.JIdx.late, DescriptiveComplexity.jqLateRel._proof_1⟩

def DescriptiveComplexity.jqPSRel (s : Bool) : jobSeqGuessBlock.lang.Relations 3

The symbol of the running total of the walk s.

Equations

• DescriptiveComplexity.jqPSRel s = ⟨DescriptiveComplexity.JIdx.ps s, ⋯⟩

def DescriptiveComplexity.jqCyRel (s : Bool) : jobSeqGuessBlock.lang.Relations 3

The symbol of the carries of the walk s.

Equations

• DescriptiveComplexity.jqCyRel s = ⟨DescriptiveComplexity.JIdx.cy s, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.jqSOLang : FirstOrder.Language

The vocabulary of the kernel.

Equations

• DescriptiveComplexity.jqSOLang = FirstOrder.Language.jobSeq.sum DescriptiveComplexity.jobSeqGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.jqJobSym : jqSOLang.Relations 1

The job symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqJobSym = Sum.inl FirstOrder.Language.jsJob

@[reducible, inline]

abbrev DescriptiveComplexity.jqPosnSym : jqSOLang.Relations 1

The position symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqPosnSym = Sum.inl FirstOrder.Language.jsPosn

@[reducible, inline]

abbrev DescriptiveComplexity.jqTimeSym : jqSOLang.Relations 2

The execution-time symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqTimeSym = Sum.inl FirstOrder.Language.jsTime

@[reducible, inline]

abbrev DescriptiveComplexity.jqDlineSym : jqSOLang.Relations 2

The deadline symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqDlineSym = Sum.inl FirstOrder.Language.jsDline

@[reducible, inline]

abbrev DescriptiveComplexity.jqPenSym : jqSOLang.Relations 2

The penalty symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqPenSym = Sum.inl FirstOrder.Language.jsPen

@[reducible, inline]

abbrev DescriptiveComplexity.jqBndSym : jqSOLang.Relations 1

The bound symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqBndSym = Sum.inl FirstOrder.Language.jsBnd

@[reducible, inline]

abbrev DescriptiveComplexity.jqLeSym : jqSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqLeSym = Sum.inl FirstOrder.Language.jsLe

@[reducible, inline]

abbrev DescriptiveComplexity.jqSchedSym : jqSOLang.Relations 2

The schedule symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqSchedSym = Sum.inr DescriptiveComplexity.jqSchedRel

@[reducible, inline]

abbrev DescriptiveComplexity.jqLateSym : jqSOLang.Relations 1

The late-jobs symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqLateSym = Sum.inr DescriptiveComplexity.jqLateRel

@[reducible, inline]

abbrev DescriptiveComplexity.jqPSSym (s : Bool) : jqSOLang.Relations 3

The running-total symbol of the walk s in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqPSSym s = Sum.inr (DescriptiveComplexity.jqPSRel s)

@[reducible, inline]

abbrev DescriptiveComplexity.jqCySym (s : Bool) : jqSOLang.Relations 3

The carry symbol of the walk s in the kernel's vocabulary.

Equations

• DescriptiveComplexity.jqCySym s = Sum.inr (DescriptiveComplexity.jqCyRel s)

Formula builders

def DescriptiveComplexity.jqJobF {α : Type} (x : α) : jqSOLang.Formula α

x is a job, as a formula.

Equations

• DescriptiveComplexity.jqJobF x = DescriptiveComplexity.jqJobSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.jqPosnF {α : Type} (x : α) : jqSOLang.Formula α

x is a bit position, as a formula.

Equations

• DescriptiveComplexity.jqPosnF x = DescriptiveComplexity.jqPosnSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.jqTimeF {α : Type} (j p : α) : jqSOLang.Formula α

The execution time of j has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.jqTimeF j p = DescriptiveComplexity.jqTimeSym.formula₂ (FirstOrder.Language.var j) (FirstOrder.Language.var p)

def DescriptiveComplexity.jqDlineF {α : Type} (j p : α) : jqSOLang.Formula α

The deadline of j has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.jqDlineF j p = DescriptiveComplexity.jqDlineSym.formula₂ (FirstOrder.Language.var j) (FirstOrder.Language.var p)

def DescriptiveComplexity.jqPenF {α : Type} (j p : α) : jqSOLang.Formula α

The penalty of j has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.jqPenF j p = DescriptiveComplexity.jqPenSym.formula₂ (FirstOrder.Language.var j) (FirstOrder.Language.var p)

def DescriptiveComplexity.jqBndF {α : Type} (p : α) : jqSOLang.Formula α

The bound has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.jqBndF p = DescriptiveComplexity.jqBndSym.formula₁ (FirstOrder.Language.var p)

def DescriptiveComplexity.jqLeF {α : Type} (x y : α) : jqSOLang.Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.jqLeF x y = DescriptiveComplexity.jqLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.jqEqF {α : Type} (x y : α) : jqSOLang.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.jqEqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.jqSchedF {α : Type} (x y : α) : jqSOLang.Formula α

x is scheduled at or before y, as a formula.

Equations

• DescriptiveComplexity.jqSchedF x y = DescriptiveComplexity.jqSchedSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.jqLateF {α : Type} (x : α) : jqSOLang.Formula α

x is late, as a formula.

Equations

• DescriptiveComplexity.jqLateF x = DescriptiveComplexity.jqLateSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.jqPSF {α : Type} (s : Bool) (i x p : α) : jqSOLang.Formula α

Bit (x, p) of the running total of the walk s at i, as a formula.

Equations

• DescriptiveComplexity.jqPSF s i x p = (DescriptiveComplexity.jqPSSym s).formula ![FirstOrder.Language.var i, FirstOrder.Language.var x, FirstOrder.Language.var p]

def DescriptiveComplexity.jqCyF {α : Type} (s : Bool) (i x p : α) : jqSOLang.Formula α

The carry at (x, p) of the step appending i to the walk s, as a formula.

Equations

• DescriptiveComplexity.jqCyF s i x p = (DescriptiveComplexity.jqCySym s).formula ![FirstOrder.Language.var i, FirstOrder.Language.var x, FirstOrder.Language.var p]

def DescriptiveComplexity.jqOrdF {α : Type} (s : Bool) (x y : α) : jqSOLang.Formula α

The order the walk s follows: the schedule for the completion times, the instance's own order for the penalties.

Equations

• DescriptiveComplexity.jqOrdF true x y = DescriptiveComplexity.jqSchedF x y
• DescriptiveComplexity.jqOrdF false x y = DescriptiveComplexity.jqLeF x y

def DescriptiveComplexity.jqSelF {α : Type} (s : Bool) (i : α) : jqSOLang.Formula α

The jobs the walk s adds up: all of them for the completion times, the late ones for the penalties.

Equations

• DescriptiveComplexity.jqSelF true i = DescriptiveComplexity.jqJobF i
• DescriptiveComplexity.jqSelF false i = DescriptiveComplexity.jqLateF i

def DescriptiveComplexity.jqWtF {α : Type} (s : Bool) (i p : α) : jqSOLang.Formula α

The number the walk s adds: the execution time, or the penalty.

Equations

• DescriptiveComplexity.jqWtF true i p = DescriptiveComplexity.jqTimeF i p
• DescriptiveComplexity.jqWtF false i p = DescriptiveComplexity.jqPenF i p

noncomputable def DescriptiveComplexity.jqBotF {α : Type} (x : α) : jqSOLang.Formula α

x is a minimum of the order, as a formula.

Equations

• DescriptiveComplexity.jqBotF x = FirstOrder.Language.Formula.iAlls Unit (DescriptiveComplexity.jqLeF (Sum.inl x) (Sum.inr ()))

noncomputable def DescriptiveComplexity.jqTopF {α : Type} (x : α) : jqSOLang.Formula α

x is a maximum of the order, as a formula.

Equations

• DescriptiveComplexity.jqTopF x = FirstOrder.Language.Formula.iAlls Unit (DescriptiveComplexity.jqLeF (Sum.inr ()) (Sum.inl x))

noncomputable def DescriptiveComplexity.jqAddF {α : Type} (s : Bool) (i x p : α) : jqSOLang.Formula α

The bit the job i contributes to the walk s at the wide position (x, p): its number's bit, in the lowest block, if the walk adds it up.

Equations

• DescriptiveComplexity.jqAddF s i x p = DescriptiveComplexity.jqSelF s i ⊓ (DescriptiveComplexity.jqBotF x ⊓ DescriptiveComplexity.jqWtF s i p)

noncomputable def DescriptiveComplexity.jqDlineWF {α : Type} (j x p : α) : jqSOLang.Formula α

Bit (x, p) of the deadline of j, read on the wide positions.

Equations

• DescriptiveComplexity.jqDlineWF j x p = DescriptiveComplexity.jqBotF x ⊓ DescriptiveComplexity.jqDlineF j p

noncomputable def DescriptiveComplexity.jqBndWF {α : Type} (x p : α) : jqSOLang.Formula α

Bit (x, p) of the bound, read on the wide positions.

Equations

• DescriptiveComplexity.jqBndWF x p = DescriptiveComplexity.jqBotF x ⊓ DescriptiveComplexity.jqBndF p

def DescriptiveComplexity.jqXor3F {α : Type} (x y z : jqSOLang.Formula α) : jqSOLang.Formula α

The exclusive or of three formulas, as x ↔ (y ↔ z).

Equations

• DescriptiveComplexity.jqXor3F x y z = x.iff (y.iff z)

def DescriptiveComplexity.jqMaj3F {α : Type} (x y z : jqSOLang.Formula α) : jqSOLang.Formula α

The majority of three formulas.

Equations

• DescriptiveComplexity.jqMaj3F x y z = x ⊓ y ⊔ (x ⊓ z ⊔ y ⊓ z)

noncomputable def DescriptiveComplexity.jqMinItemF {α : Type} (s : Bool) (i : α) : jqSOLang.Formula α

i is the first job of the walk s, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqMaxItemF {α : Type} (s : Bool) (i : α) : jqSOLang.Formula α

i is the last job of the walk s, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqSuccItemF {α : Type} (s : Bool) (i j : α) : jqSOLang.Formula α

j is the job right after i in the walk s, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqMinPosnF {α : Type} (p : α) : jqSOLang.Formula α

p is the lowest position, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqMaxPosnF {α : Type} (p : α) : jqSOLang.Formula α

p is the highest position, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqSuccPosnF {α : Type} (p q : α) : jqSOLang.Formula α

q is the position right above p, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqSuccAllF {α : Type} (x y : α) : jqSOLang.Formula α

y is the element right after x in the whole universe, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqMinWideF {α : Type} (x p : α) : jqSOLang.Formula α

(x, p) is the lowest wide position, as a formula.

Equations

• DescriptiveComplexity.jqMinWideF x p = DescriptiveComplexity.jqBotF x ⊓ DescriptiveComplexity.jqMinPosnF p

noncomputable def DescriptiveComplexity.jqMaxWideF {α : Type} (x p : α) : jqSOLang.Formula α

(x, p) is the highest wide position, as a formula.

Equations

• DescriptiveComplexity.jqMaxWideF x p = DescriptiveComplexity.jqTopF x ⊓ DescriptiveComplexity.jqMaxPosnF p

noncomputable def DescriptiveComplexity.jqSuccWideF {α : Type} (x p y q : α) : jqSOLang.Formula α

(y, q) is the wide position right above (x, p), as a formula.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.jqWideLeF {α : Type} (x p y q : α) : jqSOLang.Formula α

(x, p) ≤ (y, q) on the wide positions, as a formula.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.jqWideNeF {α : Type} (x p y q : α) : jqSOLang.Formula α

(y, q) ≠ (x, p) on the wide positions, as a formula.

Equations

• DescriptiveComplexity.jqWideNeF x p y q = FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.jqEqF y x) ⊔ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.jqEqF q p)

The clauses

noncomputable def DescriptiveComplexity.jqReflClause : jqSOLang.Sentence

Kernel clause: the order is reflexive.

Equations

• DescriptiveComplexity.jqReflClause = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.jqLeF (Sum.inr 0) (Sum.inr 0))

noncomputable def DescriptiveComplexity.jqTransClause : jqSOLang.Sentence

Kernel clause: the order is transitive.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqAntisymmClause : jqSOLang.Sentence

Kernel clause: the order is antisymmetric.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqTotalClause : jqSOLang.Sentence

Kernel clause: the order is total.

Equations

• DescriptiveComplexity.jqTotalClause = FirstOrder.Language.Formula.iAlls (Fin 2) (DescriptiveComplexity.jqLeF (Sum.inr 0) (Sum.inr 1) ⊔ DescriptiveComplexity.jqLeF (Sum.inr 1) (Sum.inr 0))

noncomputable def DescriptiveComplexity.jqSchedReflClause : jqSOLang.Sentence

Kernel clause: the schedule is reflexive.

Equations

• DescriptiveComplexity.jqSchedReflClause = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.jqSchedF (Sum.inr 0) (Sum.inr 0))

noncomputable def DescriptiveComplexity.jqSchedTransClause : jqSOLang.Sentence

Kernel clause: the schedule is transitive.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqSchedAntisymmClause : jqSOLang.Sentence

Kernel clause: the schedule is antisymmetric.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqSchedTotalClause : jqSOLang.Sentence

Kernel clause: the schedule is total.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqLateJobClause : jqSOLang.Sentence

Kernel clause: only jobs are late.

Equations

• DescriptiveComplexity.jqLateJobClause = FirstOrder.Language.Formula.iAlls (Fin 1) ((DescriptiveComplexity.jqLateF (Sum.inr 0)).imp (DescriptiveComplexity.jqJobF (Sum.inr 0)))

noncomputable def DescriptiveComplexity.jqBaseClause (s : Bool) : jqSOLang.Sentence

Kernel clause: at the first job of the walk s the running total is that job's contribution.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqSumClause (s : Bool) : jqSOLang.Sentence

Kernel clause: each step of the walk s adds a bit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqCarryClause (s : Bool) : jqSOLang.Sentence

Kernel clause: each step of the walk s propagates its carry.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqBottomClause (s : Bool) : jqSOLang.Sentence

Kernel clause: nothing is carried into the lowest wide position.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqTopClause (s : Bool) : jqSOLang.Sentence

Kernel clause: nothing is carried out of the highest wide position.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqWalkClauses (s : Bool) : jqSOLang.Sentence

The clauses of one walk.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqLateDefClause : jqSOLang.Sentence

Kernel clause: a job is late exactly when its deadline is smaller than its completion time, compared at the highest wide position where the two differ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jqFinalClause : jqSOLang.Sentence

Kernel clause: the penalty total the second walk ends on does not exceed the bound – there is no wide position carrying the total's bit above which the two agree.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.jobSequencingKernel : jqSOLang.Sentence

The first-order kernel of the Σ₁ definition of job sequencing.

Equations

• One or more equations did not get rendered due to their size.

Reading an assignment

What the guessed relations mean, and what the numbers the kernel talks about decode to. Everything the walks carry lives on the wide positions, so each number of the instance appears there through its lowest block – named by minimality, since that is all a formula can say, which is why the predicates below quantify over Unit → A the way the kernel's ∀ produces.

def DescriptiveComplexity.JWide {A : Type} [FirstOrder.Language.jobSeq.Structure A] (b : A → Prop) (u : A × A) : Prop

A number of the instance, read on the wide positions: its own bits, in the lowest block.

Equations

• DescriptiveComplexity.JWide b u = ((∀ (y : Unit → A), DescriptiveComplexity.JSLe u.1 (y ())) ∧ b u.2)

theorem DescriptiveComplexity.jWide_iff {A : Type} [FirstOrder.Language.jobSeq.Structure A] {b : A → Prop} {u : A × A} : JWide b u ↔ (∀ (y : A), JSLe u.1 y) ∧ b u.2

theorem DescriptiveComplexity.binNum_jWide {A : Type} [FirstOrder.Language.jobSeq.Structure A] [Finite A] (hlin : IsLinOrd JSLe) {a₀ : A} (h₀ : ∀ (y : A), JSLe a₀ y) (b : A → Prop) : binNum (wideLe JSLe) (WidePosn JSPosn) (JWide b) = binNum JSLe JSPosn b

Read on the wide positions, a number still has its value.

def DescriptiveComplexity.JBit {A : Type} [FirstOrder.Language.jobSeq.Structure A] (s : Bool) (i p : A) : Prop

The bits the walk s adds up: the execution times, or the penalties.

Equations

• DescriptiveComplexity.JBit true i p = DescriptiveComplexity.JSTime i p
• DescriptiveComplexity.JBit false i p = DescriptiveComplexity.JSPen i p

noncomputable def DescriptiveComplexity.JVal {A : Type} [FirstOrder.Language.jobSeq.Structure A] (s : Bool) (i : A) : ℕ

The number the walk s adds up: the execution time, or the penalty.

Equations

• DescriptiveComplexity.JVal true i = DescriptiveComplexity.JSTimeVal i
• DescriptiveComplexity.JVal false i = DescriptiveComplexity.JSPenVal i

def DescriptiveComplexity.JWt {A : Type} [FirstOrder.Language.jobSeq.Structure A] (s : Bool) (i : A) : A × A → Prop

The bit the walk s reads at a wide position.

Equations

• DescriptiveComplexity.JWt s i = DescriptiveComplexity.JWide (DescriptiveComplexity.JBit s i)

def DescriptiveComplexity.JDlineW {A : Type} [FirstOrder.Language.jobSeq.Structure A] (j : A) : A × A → Prop

The deadline of a job, read on the wide positions.

Equations

• DescriptiveComplexity.JDlineW j = DescriptiveComplexity.JWide (DescriptiveComplexity.JSDline j)

def DescriptiveComplexity.JBndW {A : Type} [FirstOrder.Language.jobSeq.Structure A] : A × A → Prop

The bound, read on the wide positions.

Equations

• DescriptiveComplexity.JBndW = DescriptiveComplexity.JWide DescriptiveComplexity.JSBnd

theorem DescriptiveComplexity.binNum_jWt {A : Type} [FirstOrder.Language.jobSeq.Structure A] [Finite A] (hlin : IsLinOrd JSLe) {a₀ : A} (h₀ : ∀ (y : A), JSLe a₀ y) (s : Bool) (i : A) : binNum (wideLe JSLe) (WidePosn JSPosn) (JWt s i) = JVal s i

theorem DescriptiveComplexity.binNum_jDlineW {A : Type} [FirstOrder.Language.jobSeq.Structure A] [Finite A] (hlin : IsLinOrd JSLe) {a₀ : A} (h₀ : ∀ (y : A), JSLe a₀ y) (j : A) : binNum (wideLe JSLe) (WidePosn JSPosn) (JDlineW j) = JSDlineVal j

theorem DescriptiveComplexity.binNum_jBndW {A : Type} [FirstOrder.Language.jobSeq.Structure A] [Finite A] (hlin : IsLinOrd JSLe) {a₀ : A} (h₀ : ∀ (y : A), JSLe a₀ y) : binNum (wideLe JSLe) (WidePosn JSPosn) JBndW = JSBound A

def DescriptiveComplexity.JSched {A : Type} (ρ : jobSeqGuessBlock.Assignment A) (a b : A) : Prop

The schedule, read off an assignment of the block.

Equations

• DescriptiveComplexity.JSched ρ a b = ρ DescriptiveComplexity.JIdx.sched ![a, b]

def DescriptiveComplexity.JLate {A : Type} (ρ : jobSeqGuessBlock.Assignment A) (j : A) : Prop

The late jobs, read off an assignment of the block.

Equations

• DescriptiveComplexity.JLate ρ j = ρ DescriptiveComplexity.JIdx.late ![j]

def DescriptiveComplexity.JPS {A : Type} (ρ : jobSeqGuessBlock.Assignment A) (s : Bool) (i : A) (u : A × A) : Prop

The running total of the walk s, read off an assignment of the block.

Equations

• DescriptiveComplexity.JPS ρ s i u = ρ (DescriptiveComplexity.JIdx.ps s) ![i, u.1, u.2]

def DescriptiveComplexity.JCy {A : Type} (ρ : jobSeqGuessBlock.Assignment A) (s : Bool) (i : A) (u : A × A) : Prop

The carries of the walk s, read off an assignment of the block.

Equations

• DescriptiveComplexity.JCy ρ s i u = ρ (DescriptiveComplexity.JIdx.cy s) ![i, u.1, u.2]

def DescriptiveComplexity.JOrd {A : Type} [FirstOrder.Language.jobSeq.Structure A] (ρ : jobSeqGuessBlock.Assignment A) (s : Bool) : A → A → Prop

The order the walk s follows: the guessed schedule for the completion times, the instance's own order for the penalties.

Equations

• DescriptiveComplexity.JOrd ρ true = DescriptiveComplexity.JSched ρ
• DescriptiveComplexity.JOrd ρ false = DescriptiveComplexity.JSLe

def DescriptiveComplexity.JSel {A : Type} [FirstOrder.Language.jobSeq.Structure A] (ρ : jobSeqGuessBlock.Assignment A) (s : Bool) : A → Prop

The jobs the walk s adds up: all of them for the completion times, the late ones for the penalties.

Equations

• DescriptiveComplexity.JSel ρ true = DescriptiveComplexity.JSJob
• DescriptiveComplexity.JSel ρ false = DescriptiveComplexity.JLate ρ