Lax Lean Archive

Corollary 2

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

    The same table read the other way round solves the problem in O(P⋅nm)O(P \cdot n^m) time, where P=∑jpjP = \sum_j p_j is the total preprocessing time: instead of recording, for each weight, the latest instant at which the first stage may begin, record for each instant the largest weight attainable from it. The recursion is the same and so is its correctness; only the axis the table is indexed along changes.

    This is the better of the two bounds whenever the preprocessing times are small and the weights are not.

    Concept map
    7 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 4 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Problems
    2
    3/-!
    4---
    5title: Corollary 2
    6type: theorem
    7---
    8The same table read the other way round solves the problem in O(P⋅nm)O(P \cdot n^m) time,
    9where P=∑jpjP = \sum_j p_j is the total preprocessing time: instead of recording, for each
    10weight, the latest instant at which the first stage may begin, record for each instant
    11the largest weight attainable from it. The recursion is the same and so is its
    12correctness; only the axis the table is indexed along changes.
    13
    14This is the better of the two bounds whenever the preprocessing times are small and the
    15weights are not.
    16
    17# Formalization Notes
    18
    19No new combinatorial statement is needed. The dual table is the same predicate with its
    20two numerical arguments exchanged, so the correctness of recursion (1) is the correctness
    21of both programs, and only the running time is stated here.
    22
    23The instants the table runs over are the partial sums of preprocessing times, of which
    24there are at most P+1P+1; that is what makes PP, rather than the largest due date, the
    25quantity in the bound.
    26
    27The domain also asks that every processing time be positive, qj≥1q_j \ge 1. This is the paper's
    28standing assumption for the recursions behind the algorithms — a job with qj=0q_j = 0 has an
    29empty second operation, and the characterization of the feasible sets, on which everything
    30rests, is stated for jobs that have a genuine one — but the paper does not repeat it in each
    31claim, and a statement about a program that reads an arbitrary word has to.
    32-/
    33
    34namespace Lax496464.Corollary2
    35
    36open Lax496464.WordEncoding Lax496464.Problems Lax496464.ParameterizedComplexity
    37open Lax808846.Ram Lax808846.RamComputes
    38
    39open Classical in
    40/-- **Corollary 2.** The dual program decides the problem within `c · (P+1) · (n+1)^m`
    41instructions, plus the cost of sorting. -/
    42axiom corollary2_time :
    43 ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    44 ComputesInTime w prog
    45 {x | x ∈ DecisionInstances ∧ Fits c w x ∧
    46 c * (preSum x + 1) * (jobCount x + 1) ^ machineCount x ≤ 2 ^ w ∧
    47 (∀ j < jobCount x, 0 < procTime x j)}
    48 (fun x => if Yes x then [1] else [0])
    49 (fun x => c * (preSum x + 1) * (jobCount x + 1) ^ machineCount x +
    50 c * sortCost x)
    51
    52end Lax496464.Corollary2
    53
    Show Proof
    Formalization Notes

    No new combinatorial statement is needed. The dual table is the same predicate with its two numerical arguments exchanged, so the correctness of recursion (1) is the correctness of both programs, and only the running time is stated here.

    The instants the table runs over are the partial sums of preprocessing times, of which there are at most P+1P+1; that is what makes PP, rather than the largest due date, the quantity in 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…