Lax Lean Archive

Theorem 3

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

    Two further programs, each fast when one quantity of the instance is small.

    The endpoint sweep of Section 4 carries a subset of the jobs alive at the current instant, and so runs in O(W⋅2ω⋅n)O(W \cdot 2^{\omega} \cdot n) time, where ω\omega is the largest number of jobs alive at one instant.

    The profile sweep of Section 5 carries, instead of that subset, only how many of its jobs are due at each of the next qmax⁡q_{\max} instants, and so runs in O(W⋅mqmax⁡⋅n)O(W \cdot m^{q_{\max}} \cdot n) time.

    Neither bound involves the number of machines in the exponent, so both are useful precisely where the program of the second theorem is not.

    Concept map
    7 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 theorem3_qmax_time proven

    2 theorem3_width_time proven

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Problems
    2
    3/-!
    4---
    5title: Theorem 3
    6type: theorem
    7---
    8Two further programs, each fast when one quantity of the instance is small.
    9
    10The endpoint sweep of Section 4 carries a subset of the jobs alive at the current
    11instant, and so runs in O(W⋅2ω⋅n)O(W \cdot 2^{\omega} \cdot n) time, where ω\omega is the
    12largest number of jobs alive at one instant.
    13
    14The profile sweep of Section 5 carries, instead of that subset, only how many of its jobs
    15are due at each of the next qmax⁡q_{\max} instants, and so runs in
    16O(W⋅mqmax⁡⋅n)O(W \cdot m^{q_{\max}} \cdot n) time.
    17
    18Neither bound involves the number of machines in the exponent, so both are useful
    19precisely where the program of the second theorem is not.
    20
    21# Formalization Notes
    22
    23Two statements, one per program, each with its own fitting condition for its own table,
    24and each restricted to no slice: both programs decide the problem on every instance, and
    25what changes from one to the other is only the bound.
    26
    27The width ω\omega and the largest processing time qmax⁡q_{\max} are functions of the word.
    28No claim is made that a program computes them — neither program needs to, since neither
    29allocates a table indexed by them in advance — but a running time stated in terms of a
    30quantity that was not a function of the input would not be a statement about a program at
    31all.
    32
    33The second bound is written with m+1m+1 rather than mm in the base, and both with n+1n+1
    34rather than nn, for the reason the second theorem gives: at the extremes the bare
    35product collapses to zero and no program answers in no instructions. The forms agree up
    36to the constant as soon as there is a job and a machine.
    37
    38The sweep of Section 4 assumes the endpoints distinct, which the rescaling of the same
    39section supplies; that is a step of the proof and not a hypothesis of the claim, since
    40the rescaling is computed by the program itself.
    41
    42The domain also asks that every processing time be positive, qj≥1q_j \ge 1. This is the paper's
    43standing assumption for the recursions behind the algorithms — a job with qj=0q_j = 0 has an
    44empty second operation, and the characterization of the feasible sets, on which everything
    45rests, is stated for jobs that have a genuine one — but the paper does not repeat it in each
    46claim, and a statement about a program that reads an arbitrary word has to.
    47-/
    48
    49namespace Lax496464.Theorem3
    50
    51open Lax496464.WordEncoding Lax496464.Problems Lax496464.ParameterizedComplexity
    52open Lax808846.Ram Lax808846.RamComputes
    53
    54open Classical in
    55/-- **Theorem 3, the endpoint sweep.** The problem is decided within
    56`c · (W+1) · 2^ω · (n+1)` instructions, plus the cost of sorting. -/
    57axiom theorem3_width_time :
    58 ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    59 ComputesInTime w prog
    60 {x | x ∈ DecisionInstances ∧ Fits c w x ∧
    61 c * (threshold x + 1) * 2 ^ widthOf x * (jobCount x + 1) ≤ 2 ^ w ∧
    62 (∀ j < jobCount x, 0 < procTime x j)}
    63 (fun x => if Yes x then [1] else [0])
    64 (fun x => c * (threshold x + 1) * 2 ^ widthOf x * (jobCount x + 1) +
    65 c * sortCost x)
    66
    67open Classical in
    68/-- **Theorem 3, the profile sweep.** The problem is decided within
    69`c · (W+1) · (m+1)^q_max · (n+1)` instructions, plus the cost of sorting. -/
    70axiom theorem3_qmax_time :
    71 ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    72 ComputesInTime w prog
    73 {x | x ∈ DecisionInstances ∧ Fits c w x ∧
    74 c * (threshold x + 1) * (machineCount x + 1) ^ qmaxOf x * (jobCount x + 1)
    75 ≤ 2 ^ w ∧ (∀ j < jobCount x, 0 < procTime x j)}
    76 (fun x => if Yes x then [1] else [0])
    77 (fun x => c * (threshold x + 1) * (machineCount x + 1) ^ qmaxOf x *
    78 (jobCount x + 1) + c * sortCost x)
    79
    80end Lax496464.Theorem3
    81
    Show ProofShow Proof
    Formalization Notes

    Two statements, one per program, each with its own fitting condition for its own table, and each restricted to no slice: both programs decide the problem on every instance, and what changes from one to the other is only the bound.

    The width ω\omega and the largest processing time qmax⁡q_{\max} are functions of the word. No claim is made that a program computes them — neither program needs to, since neither allocates a table indexed by them in advance — but a running time stated in terms of a quantity that was not a function of the input would not be a statement about a program at all.

    The second bound is written with m+1m+1 rather than mm in the base, and both with n+1n+1 rather than nn, for the reason the second theorem gives: at the extremes the bare product collapses to zero and no program answers in no instructions. The forms agree up to the constant as soon as there is a job and a machine.

    The sweep of Section 4 assumes the endpoints distinct, which the rescaling of the same section supplies; that is a step of the proof and not a hypothesis of the claim, since the rescaling is computed by the program itself.

    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…