Lax Lean Archive

Corollary 3

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

    When all preprocessing times are equal, the problem is solved in O(nm+1)O(n^{m+1}) time. With pj=pp_j = p the total preprocessing time a partial solution has spent is determined by how many jobs it has selected, so the instant the dual table runs over takes only n+1n+1 values, and the bound of the second corollary becomes O(n⋅nm)O(n \cdot n^m).

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Problems
    2import Lax496464.ProperInstances
    3
    4/-!
    5---
    6title: Corollary 3
    7type: theorem
    8---
    9When all preprocessing times are equal, the problem is solved in O(nm+1)O(n^{m+1}) time. With
    10pj=pp_j = p the total preprocessing time a partial solution has spent is determined by how
    11many jobs it has selected, so the instant the dual table runs over takes only n+1n+1
    12values, and the bound of the second corollary becomes O(n⋅nm)O(n \cdot n^m).
    13
    14# Formalization Notes
    15
    16The slice is stated on the decoded instance, as the existence of a common preprocessing
    17time, rather than as a condition on the entries of the word. The two say the same thing
    18on an admissible word, and the first is the condition a reader checks the claim against.
    19
    20The uniform case is a restriction on the instance only; no assumption is made about the
    21weights, which may be arbitrary. That is what distinguishes this corollary from the
    22unweighted case of the fourth theorem.
    23
    24The domain also asks that every processing time be positive, qj≥1q_j \ge 1. This is the paper's
    25standing assumption for the recursions behind the algorithms — a job with qj=0q_j = 0 has an
    26empty second operation, and the characterization of the feasible sets, on which everything
    27rests, is stated for jobs that have a genuine one — but the paper does not repeat it in each
    28claim, and a statement about a program that reads an arbitrary word has to.
    29-/
    30
    31namespace Lax496464.Corollary3
    32
    33open Lax496464.WordEncoding Lax496464.Problems Lax496464.ParameterizedComplexity
    34open Lax496464.ProperInstances
    35open Lax808846.Ram Lax808846.RamComputes
    36
    37open Classical in
    38/-- **Corollary 3.** With equal preprocessing times the problem is decided within
    39`c · (n+1)^(m+1)` instructions, plus the cost of sorting. -/
    40axiom corollary3_time :
    41 ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    42 ComputesInTime w prog
    43 {x | x ∈ DecisionInstances ∧ Fits c w x ∧
    44 (∃ I W, EncodesDecisionInstance x I W ∧ Uniform I) ∧
    45 c * (jobCount x + 1) ^ (machineCount x + 1) ≤ 2 ^ w ∧
    46 (∀ j < jobCount x, 0 < procTime x j)}
    47 (fun x => if Yes x then [1] else [0])
    48 (fun x => c * (jobCount x + 1) ^ (machineCount x + 1) + c * sortCost x)
    49
    50end Lax496464.Corollary3
    51
    Show Proof
    Formalization Notes

    The slice is stated on the decoded instance, as the existence of a common preprocessing time, rather than as a condition on the entries of the word. The two say the same thing on an admissible word, and the first is the condition a reader checks the claim against.

    The uniform case is a restriction on the instance only; no assumption is made about the weights, which may be arbitrary. That is what distinguishes this corollary from the unweighted case of the fourth theorem.

    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…