Lax Lean Archive

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

The auxiliary problem reduces to scheduling on two job lengths

Lax391470.Lemma1 · concepts/Lax391470/Lemma1.lean · lax-391470

proven

Loading review…

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

    For any two integer job lengths p>q≥1p > q \ge 1, the problem AUX(p,q)\mathrm{AUX}(p, q) is polynomial-time reducible to single machine scheduling with release times and deadlines on the job lengths {p,q}\{p, q\}.

    The reduction replaces every connected pair of pending jobs by the five jobs of the stacked construction. Its correctness is proved by an exchange argument: a feasible schedule of the stacked instance is rearranged, pair by pair in order of urgency, until every bin holds two jobs of its own pair, and the jobs left after time 00 are then read as a solution of the auxiliary instance.

    Concept map
    9 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 aux_manyOne_twoLengths proven

    2 reduce_correct proven

    3 reduce_polyTime proven

    Lean source view on GitHub

    1import Lax391470.BinaryEncoding
    2import Lax391470.StackedConstruction
    3import Lax429075.Reductions
    4
    5/-!
    6---
    7title: The auxiliary problem reduces to scheduling on two job lengths
    8type: theorem
    9---
    10For any two integer job lengths p>q≥1p > q \ge 1, the problem AUX(p,q)\mathrm{AUX}(p, q) is
    11polynomial-time reducible to single machine scheduling with release times and deadlines
    12on the job lengths {p,q}\{p, q\}.
    13
    14The reduction replaces every connected pair of pending jobs by the five jobs of the
    15stacked construction. Its correctness is proved by an exchange argument: a feasible
    16schedule of the stacked instance is rearranged, pair by pair in order of urgency, until
    17every bin holds two jobs of its own pair, and the jobs left after time 00 are then read
    18as a solution of the auxiliary instance.
    19
    20# Formalization notes
    21
    22A reduction is a function on all words. A word that does not encode an ordered instance
    23of the auxiliary problem is sent to the encoding of a fixed instance without a feasible
    24schedule: a single job of length pp whose deadline equals its release time.
    25
    26The three statements separate what is asserted. The first is the combinatorial content:
    27the map preserves and reflects membership. The second is the running time of that same
    28map on a Turing machine. The third is the lemma as the source states it, which follows
    29from the other two.
    30-/
    31
    32namespace Lax391470.Lemma1
    33
    34open Lax391470.BinaryEncoding Lax434930.PolynomialTime Lax429075.Reductions
    35
    36/-- An instance on the lengths `{p, q}` without a feasible schedule, when `p ≥ 1`: one job
    37of length `p` that is due when it is released. -/
    38def blocked (p : ℕ) : Scheduling.Instance where
    39 jobs := 1
    40 r _ := 0
    41 d _ := 0
    42 p _ := p
    43
    44/-- **The reduction**, as a map on words: the encoding of an ordered instance `A` is sent
    45to the encoding of its stacked instance, and every other word to the encoding of
    46`blocked p`. -/
    47noncomputable def reduce (p q : ℕ) (w : Word) : Word :=
    48 open Classical in
    49 if h : ∃ A : AuxiliaryProblem.Instance, encodeAux A = w ∧ A.Ordered then
    50 encodeInstance (StackedConstruction.inst p q h.choose)
    51 else encodeInstance (blocked p)
    52
    53/-- **The reduction is correct.** -/
    54axiom reduce_correct (p q : ℕ) (hq : 0 < q) (hqp : q < p) (w : Word) :
    55 w ∈ AUX p q ↔ reduce p q w ∈ TwoLengths p q
    56
    57/-- **The reduction runs in polynomial time.** -/
    58axiom reduce_polyTime (p q : ℕ) :
    59 Nonempty (Turing.TM2ComputableInPolyTime id id (reduce p q))
    60
    61/-- **Lemma 1.** For job lengths `p > q ≥ 1`, `AUX(p, q)` is polynomial-time reducible to
    62scheduling on the lengths `{p, q}`. -/
    63axiom aux_manyOne_twoLengths (p q : ℕ) (hq : 0 < q) (hqp : q < p) :
    64 ManyOne (AUX p q) (TwoLengths p q)
    65
    66end Lax391470.Lemma1
    67
    Show ProofShow ProofShow Proof
    Formalization notes

    A reduction is a function on all words. A word that does not encode an ordered instance of the auxiliary problem is sent to the encoding of a fixed instance without a feasible schedule: a single job of length pp whose deadline equals its release time.

    The three statements separate what is asserted. The first is the combinatorial content: the map preserves and reflects membership. The second is the running time of that same map on a Turing machine. The third is the lemma as the source states it, which follows from the other two.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…