Para-NP-hardness along the steps between objectives
Lax434175.ThresholdParams · concepts/Lax434175/ThresholdParams.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
A step between objectives (concept : the makespan and the maximum lateness to the number of late jobs and to the total tardiness, flow time to tardiness, completion time to flow time) rewrites only the objective data and the threshold of the standard word; the instance of the kernel, with its jobs, machines, processing times and release dates, stays the same. So a parameter that reads only the kernel instance takes the same value before and after the step.
A parameter of the target objective is bounded on the kernel instance by one of the source objective if, for any two instances with the same kernel instance, the first is at most the second.
Theorem. If the source objective is para-NP-hard for a parameter, and a parameter of the target is bounded on the kernel instance by it, the target is para-NP-hard for that parameter.
Theorem. The number of jobs , the number of machines , the largest processing time , the numbers and of distinct processing times and release dates, the number of kinds of machines and the rank of the processing time matrix are each bounded on the kernel instance by themselves.
Concept map
Evidence
This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.
1 base_kinds proven
2 base_m proven
3 base_n proven
4 base_numP proven
5 base_numR proven
6 base_pmax proven
7 base_rank proven
8 paraNPHard_step proven
Lean source view on GitHub
| 1 | import Lax434175.ThresholdWords |
| 2 | import Lax434175.ResultParameters |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Para-NP-hardness along the steps between objectives |
| 7 | type: theorem |
| 8 | --- |
| 9 | A step between objectives (concept `ThresholdWords`: the makespan and the maximum |
| 10 | lateness to the number of late jobs and to the total tardiness, flow time to |
| 11 | tardiness, completion time to flow time) rewrites only the objective data and the |
| 12 | threshold of the standard word; the instance of the kernel, with its jobs, |
| 13 | machines, processing times and release dates, stays the same. So a parameter that |
| 14 | reads only the kernel instance takes the same value before and after the step. |
| 15 | |
| 16 | A parameter of the target objective is *bounded on the kernel instance* by one of |
| 17 | the source objective if, for any two instances with the same kernel instance, the |
| 18 | first is at most the second. |
| 19 | |
| 20 | **Theorem.** If the source objective is para-NP-hard for a parameter, and a |
| 21 | parameter of the target is bounded on the kernel instance by it, the target is |
| 22 | para-NP-hard for that parameter. |
| 23 | |
| 24 | **Theorem.** The number of jobs , the number of machines , the largest |
| 25 | processing time , the numbers and of distinct processing |
| 26 | times and release dates, the number of kinds of machines and the rank of the |
| 27 | processing time matrix are each bounded on the kernel instance by themselves. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax434175.ThresholdParams |
| 31 | open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Results Lax434175.ThresholdWords |
| 32 | open Lax434175.ResultParameters |
| 33 | |
| 34 | variable (values : (i : OperationsFamily.FieldName) → (OperationsFamily.family.module i).Value) |
| 35 | |
| 36 | /-- `κt` is at most `κs` on any two instances with the same kernel instance. -/ |
| 37 | def BaseBound (o o' : Objectives.Value) (κs : TParameter (problem _ (Thresholds.withObjective values o))) |
| 38 | (κt : TParameter (problem _ (Thresholds.withObjective values o'))) : Prop := |
| 39 | ∀ x y D D', y.base = x.base → κt y D' ≤ κs x D |
| 40 | |
| 41 | axiom paraNPHard_step (hs : values .encoding = .standard) {o o' : Objectives.Value} {mode : StepMode} |
| 42 | (hm : stepOf o o' = some mode) {κs : TParameter (problem _ (Thresholds.withObjective values o))} |
| 43 | {κt : TParameter (problem _ (Thresholds.withObjective values o'))} |
| 44 | (hκ : BaseBound values o o' κs κt) : |
| 45 | ParaNPHard (StandardReading.ops.at (Thresholds.withObjective values o)) κs → |
| 46 | ParaNPHard (StandardReading.ops.at (Thresholds.withObjective values o')) κt |
| 47 | |
| 48 | axiom base_n (o o' : Objectives.Value) : |
| 49 | BaseBound values o o' (lift (Ops.n _)) (lift (Ops.n _)) |
| 50 | axiom base_m (o o' : Objectives.Value) : |
| 51 | BaseBound values o o' (lift (Ops.m _)) (lift (Ops.m _)) |
| 52 | axiom base_pmax (o o' : Objectives.Value) : |
| 53 | BaseBound values o o' (lift (Ops.pmax _)) (lift (Ops.pmax _)) |
| 54 | axiom base_numP (o o' : Objectives.Value) : |
| 55 | BaseBound values o o' (lift (Ops.numP _)) (lift (Ops.numP _)) |
| 56 | axiom base_numR (o o' : Objectives.Value) : |
| 57 | BaseBound values o o' (lift (Ops.numR _)) (lift (Ops.numR _)) |
| 58 | axiom base_kinds (o o' : Objectives.Value) : |
| 59 | BaseBound values o o' (lift (Ops.kinds _)) (lift (Ops.kinds _)) |
| 60 | axiom base_rank (o o' : Objectives.Value) : |
| 61 | BaseBound values o o' (lift (Ops.rank _)) (lift (Ops.rank _)) |
| 62 | |
| 63 | end Lax434175.ThresholdParams |
| 64 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments