Lax Lean Archive

Theorem 2

Lax496464.Theorem2 · concepts/Lax496464/Theorem2.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

    Just-in-time scheduling in a two-stage flexible flow shop is solved in O(W⋅nm)O(W \cdot n^m) time, where WW is the threshold, nn the number of jobs and mm the number of second-stage machines: the table of Section 3 has nmn^m columns and W+1W+1 rows, and recursion (1) fills each entry from two earlier ones.

    The answer is read off the table at the mm smallest indices: a set of weight W′W' compatible with them and preprocessable from the instant 00 is exactly a feasible solution of weight W′W'.

    Concept map
    9 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 achievable_readoff proven

    2 theorem2_time proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.DynamicProgram
    2import Lax496464.Problems
    3
    4/-!
    5---
    6title: Theorem 2
    7type: theorem
    8---
    9Just-in-time scheduling in a two-stage flexible flow shop is solved in
    10O(W⋅nm)O(W \cdot n^m) time, where WW is the threshold, nn the number of jobs and mm the
    11number of second-stage machines: the table of Section 3 has nmn^m columns and W+1W+1 rows,
    12and recursion (1) fills each entry from two earlier ones.
    13
    14The answer is read off the table at the mm smallest indices: a set of weight W′W'
    15compatible with them and preprocessable from the instant 00 is exactly a feasible
    16solution of weight W′W'.
    17
    18# Formalization Notes
    19
    20Two statements: the read-off, which is a combinatorial fact about the table, and the
    21running time, which is a claim about a program.
    22
    23The read-off is what connects the recursion to the problem. Compatibility with the mm
    24smallest indices is schedulability on mm machines and no more, and a budget of 00 is
    25the first-stage machine starting at the beginning of time, so the two ends of the table
    26meet the definition of a feasible set. Without it the recursion would compute something
    27about a table and nothing about the shop.
    28
    29The running time is stated with explicit constants rather than asymptotically, and with
    30the +1+1s the product needs to stay meaningful at the extremes: a threshold of zero, a
    31shop with no machines, and a shop with no jobs each drive the bare product to zero or
    32one, and no program answers in no instructions. The two forms agree up to the constant as
    33soon as there is a job and a machine.
    34
    35The fitting condition carries a clause beyond the usual one, that the table itself fits
    36into memory. The table is indexed by a set of thresholds and a weight, and a machine
    37whose memory holds 2w2^w cells cannot address more than that; a statement that omitted it
    38would claim a running time the machine has no room to achieve.
    39
    40The sorting term is the cost of putting the jobs into earliest-start-time order, which
    41Section 3 assumes done. It is the only place the input's own length enters the bound.
    42
    43The domain also asks that every processing time be positive, qj≥1q_j \ge 1. This is the paper's
    44standing assumption for the recursions behind the algorithms — a job with qj=0q_j = 0 has an
    45empty second operation, and the characterization of the feasible sets, on which everything
    46rests, is stated for jobs that have a genuine one — but the paper does not repeat it in each
    47claim, and a statement about a program that reads an arbitrary word has to.
    48-/
    49
    50namespace Lax496464.Theorem2
    51
    52open Lax496464.FlowShop Lax496464.FlowShop.Instance
    53open Lax496464.EstOrder Lax496464.DynamicProgram
    54open Lax496464.WordEncoding Lax496464.Problems Lax496464.ParameterizedComplexity
    55open Lax808846.Ram Lax808846.RamComputes
    56
    57/-- **The read-off.** A set of weight `W'` compatible with the `m` smallest indices that
    58can be preprocessed from a nonnegative instant is exactly a feasible set of weight `W'`. -/
    59axiom achievable_readoff (I : Instance) (hest : EstOrdered I) (W' : ℕ) :
    60 (∃ P' : ℤ, 0 ≤ P' ∧ Achievable I (firstM I) W' P') ↔
    61 ∃ Z : Finset I.Job, Feasible I Z ∧ weight I Z = W'
    62
    63open Classical in
    64/-- **Theorem 2.** One word RAM program decides the problem within
    65`c · (W+1) · (n+1)^m` instructions, plus the cost of sorting, at every word length
    66admitting the instance and its table. -/
    67axiom theorem2_time :
    68 ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    69 ComputesInTime w prog
    70 {x | x ∈ DecisionInstances ∧ Fits c w x ∧
    71 c * (threshold x + 1) * (jobCount x + 1) ^ machineCount x ≤ 2 ^ w ∧
    72 (∀ j < jobCount x, 0 < procTime x j)}
    73 (fun x => if Yes x then [1] else [0])
    74 (fun x => c * (threshold x + 1) * (jobCount x + 1) ^ machineCount x +
    75 c * sortCost x)
    76
    77end Lax496464.Theorem2
    78
    Show ProofShow Proof
    Formalization Notes

    Two statements: the read-off, which is a combinatorial fact about the table, and the running time, which is a claim about a program.

    The read-off is what connects the recursion to the problem. Compatibility with the mm smallest indices is schedulability on mm machines and no more, and a budget of 00 is the first-stage machine starting at the beginning of time, so the two ends of the table meet the definition of a feasible set. Without it the recursion would compute something about a table and nothing about the shop.

    The running time is stated with explicit constants rather than asymptotically, and with the +1+1s the product needs to stay meaningful at the extremes: a threshold of zero, a shop with no machines, and a shop with no jobs each drive the bare product to zero or one, and no program answers in no instructions. The two forms agree up to the constant as soon as there is a job and a machine.

    The fitting condition carries a clause beyond the usual one, that the table itself fits into memory. The table is indexed by a set of thresholds and a weight, and a machine whose memory holds 2w2^w cells cannot address more than that; a statement that omitted it would claim a running time the machine has no room to achieve.

    The sorting term is the cost of putting the jobs into earliest-start-time order, which Section 3 assumes done. It is the only place the input's own length enters the bound.

    The domain also asks that every processing time be positive, qj≥1q_j \ge 1. This is the paper's standing assumption for the recursions behind the algorithms — a job with qj=0q_j = 0 has an empty second operation, and the characterization of the feasible sets, on which everything rests, is stated for jobs that have a genuine one — but the paper does not repeat it in each claim, and a statement about a program that reads an arbitrary word has to.

    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…