Lax Lean Archive

Lemma 4

Lax496464.Lemma4 · concepts/Lax496464/Lemma4.lean · lax-496464

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

    After the greedy has considered the first kk jobs, the set it holds is feasible, uses only those jobs, and dominates every feasible set of jobs among them. Consequently the set it holds at the end is a feasible set of largest possible cardinality, which is the correctness of the algorithm of Section 6.1.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 greedy_card_max proven

    2 greedy_dominating proven

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Greedy
    2
    3/-!
    4---
    5title: Lemma 4
    6type: theorem
    7---
    8After the greedy has considered the first kk jobs, the set it holds is feasible, uses
    9only those jobs, and dominates every feasible set of jobs among them. Consequently the
    10set it holds at the end is a feasible set of largest possible cardinality, which is the
    11correctness of the algorithm of Section 6.1.
    12
    13# Formalization Notes
    14
    15The statement is about every run of the relation, since the rule leaves choices open, and
    16it is proved by induction along the run with the domination property as the invariant.
    17
    18The order is the counting one, which is stronger than what the paper's disjunction gives
    19where the cardinalities differ — see the definition for why the paper's will not carry
    20this induction. The conclusion of the algorithm's correctness is unaffected: an order
    21that dominates in this sense also dominates in cardinality.
    22
    23The run is presented as a sequence of sets indexed by how many jobs have been considered,
    24with a first member that is empty and a step at each job. Nothing requires the sequence
    25to be computed by anything in particular; what is claimed is that any sequence satisfying
    26the two conditions ends at an optimum.
    27
    28Equal preprocessing times and positive processing times are hypotheses, as in the
    29paper. Weights play no role: this is the unweighted case, and the conclusion is about
    30cardinality.
    31-/
    32
    33namespace Lax496464.Lemma4
    34
    35open Lax496464.FlowShop Lax496464.FlowShop.Instance
    36open Lax496464.EstOrder Lax496464.Greedy
    37
    38variable (I : Instance)
    39
    40/-- **Lemma 4.** Along any greedy run, the set held after `k` jobs is a feasible subset of
    41the first `k` jobs dominating every such feasible set. -/
    42axiom greedy_dominating (hest : EstOrdered I) {p : ℕ} (hp : ∀ i : I.Job, I.p i = p)
    43 (hq : ∀ i : I.Job, 0 < I.q i)
    44 (S : ℕ → Finset I.Job) (h0 : S 0 = ∅)
    45 (hrun : ∀ k, ∀ hk : k < I.jobs, Step I p (S k) (S (k + 1)) ⟨k, hk⟩) :
    46 ∀ k ≤ I.jobs,
    47 Feasible I (S k) ∧ S k ⊆ firstJobs I k ∧
    48 ∀ B : Finset I.Job, B ⊆ firstJobs I k → Feasible I B → SDom I (S k) B
    49
    50/-- **The greedy is optimal.** Its final set is a feasible set of largest cardinality. -/
    51axiom greedy_card_max (hest : EstOrdered I) {p : ℕ} (hp : ∀ i : I.Job, I.p i = p)
    52 (hq : ∀ i : I.Job, 0 < I.q i)
    53 (S : ℕ → Finset I.Job) (h0 : S 0 = ∅)
    54 (hrun : ∀ k, ∀ hk : k < I.jobs, Step I p (S k) (S (k + 1)) ⟨k, hk⟩) :
    55 Feasible I (S I.jobs) ∧
    56 ∀ B : Finset I.Job, Feasible I B → B.card ≤ (S I.jobs).card
    57
    58end Lax496464.Lemma4
    59
    Show ProofShow Proof
    Formalization Notes

    The statement is about every run of the relation, since the rule leaves choices open, and it is proved by induction along the run with the domination property as the invariant.

    The order is the counting one, which is stronger than what the paper's disjunction gives where the cardinalities differ — see the definition for why the paper's will not carry this induction. The conclusion of the algorithm's correctness is unaffected: an order that dominates in this sense also dominates in cardinality.

    The run is presented as a sequence of sets indexed by how many jobs have been considered, with a first member that is empty and a step at each job. Nothing requires the sequence to be computed by anything in particular; what is claimed is that any sequence satisfying the two conditions ends at an optimum.

    Equal preprocessing times and positive processing times are hypotheses, as in the paper. Weights play no role: this is the unweighted case, and the conclusion is about cardinality.

    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…