While this submission is a draft, it cannot be used by other submissions.

Para-NP-hardness along the steps between objectives

Lax434175.ThresholdParams · concepts/Lax434175/ThresholdParams.lean · lax-434175

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    A step between objectives (concept ThresholdWordsThresholdWords: 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 nn, the number of machines mm, the largest processing time pmax⁡p_{\max}, the numbers #p\#p and #r\#r 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
    61 concepts
    100%
    Conjunctive normal formAssembling problems from fieldsOne family for serial and parallel batchingBatching problems in three-field notationBatch scheduling on a single machineCommunication delaysBounds on the number of machines and jobsDeadlinesForbidden times and input encodingsInterruption as a field of parallel-machineschedulingScheduling kernelsMaximizing the minimum machine loadMachine sets and multiprocessor tasksConstraint modules and objectivesNon-preemptive scheduling on parallelmachinesCompletion-time objectivesOnline scheduling as a gameScheduling with operationsOne family for parallel machines and shopsOne family for parallel machines with andwithout preemptionParallel machinesProblems on parallel machines in three-fieldnotationParameters along embeddingsPrecedence constraints and time lagsPreemptive scheduling on parallel machinesPreemptive shop problems in three-fieldnotationPreemptive shop schedulingOptimization problems and embeddingsSingle-machine scheduling with rejectionRelease datesPreemption with restarts on parallelmachinesParameters of the zoo's resultsThe kinds of results on scheduling problemsA single server with setup timesNo-idle shops and batch setup timesOne family for shops with and withoutpreemptionShop problems in three-field notationShop schedulingThe standard reading of scheduling instancesand schedulesPara-NP-hardness along the steps betweenobjectivesThe steps between objectives on wordsThreshold reductions between objectivesTransportation delays and a transport robotScheduling problems as parameterizedproblems on wordsParameters of scheduling problemsBinary encoding of an input and a certificateThe complexity class NPThe complexity class PFixed-Parameter Time on the Word RAMFPT-Reductions, FPT, Hardness andCompletenessFinite Relational StructuresFirst-Order Formulas and the Classes Σ_tand Π_tModel Checking and Weighted FaginDefinabilityThe W-Hierarchy and the A-HierarchyNP-Hardness of a Problem on Words ofNumbersBinary encoding of finite wordsPolynomial-time computation by a wordRAMPolynomial-time computation by a TuringmachineThe word RAMComputing a function within a time boundParameterized Problems andFPT-Reductions on a Word RAM
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Lean source view on GitHub

    1import Lax434175.ThresholdWords
    2import Lax434175.ResultParameters
    3
    4/-!
    5---
    6title: Para-NP-hardness along the steps between objectives
    7type: theorem
    8---
    9A step between objectives (concept `ThresholdWords`: the makespan and the maximum
    10lateness to the number of late jobs and to the total tardiness, flow time to
    11tardiness, completion time to flow time) rewrites only the objective data and the
    12threshold of the standard word; the instance of the kernel, with its jobs,
    13machines, processing times and release dates, stays the same. So a parameter that
    14reads only the kernel instance takes the same value before and after the step.
    15
    16A parameter of the target objective is *bounded on the kernel instance* by one of
    17the source objective if, for any two instances with the same kernel instance, the
    18first is at most the second.
    19
    20**Theorem.** If the source objective is para-NP-hard for a parameter, and a
    21parameter of the target is bounded on the kernel instance by it, the target is
    22para-NP-hard for that parameter.
    23
    24**Theorem.** The number of jobs nn, the number of machines mm, the largest
    25processing time pmax⁡p_{\max}, the numbers #p\#p and #r\#r of distinct processing
    26times and release dates, the number of kinds of machines and the rank of the
    27processing time matrix are each bounded on the kernel instance by themselves.
    28-/
    29
    30namespace Lax434175.ThresholdParams
    31open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Results Lax434175.ThresholdWords
    32open Lax434175.ResultParameters
    33
    34variable (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. -/
    37def 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
    41axiom 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
    48axiom base_n (o o' : Objectives.Value) :
    49 BaseBound values o o' (lift (Ops.n _)) (lift (Ops.n _))
    50axiom base_m (o o' : Objectives.Value) :
    51 BaseBound values o o' (lift (Ops.m _)) (lift (Ops.m _))
    52axiom base_pmax (o o' : Objectives.Value) :
    53 BaseBound values o o' (lift (Ops.pmax _)) (lift (Ops.pmax _))
    54axiom base_numP (o o' : Objectives.Value) :
    55 BaseBound values o o' (lift (Ops.numP _)) (lift (Ops.numP _))
    56axiom base_numR (o o' : Objectives.Value) :
    57 BaseBound values o o' (lift (Ops.numR _)) (lift (Ops.numR _))
    58axiom base_kinds (o o' : Objectives.Value) :
    59 BaseBound values o o' (lift (Ops.kinds _)) (lift (Ops.kinds _))
    60axiom base_rank (o o' : Objectives.Value) :
    61 BaseBound values o o' (lift (Ops.rank _)) (lift (Ops.rank _))
    62
    63end Lax434175.ThresholdParams
    64
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…