Lax Lean Archive

Corollary 1

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

    With a single second-stage machine and no weights, the problem is solved in O(n2)O(n^2) time. It is the program of the second theorem at m=1m = 1: the table has nn columns, the threshold is at most nn because every weight is one, and the two bounds multiply.

    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 1
    6type: theorem
    7---
    8With a single second-stage machine and no weights, the problem is solved in O(n2)O(n^2)
    9time. It is the program of the second theorem at m=1m = 1: the table has nn columns, the
    10threshold is at most nn because every weight is one, and the two bounds multiply.
    11
    12# Formalization Notes
    13
    14The claim is about the slice of instances with one machine and unit weights, so the
    15statement restricts the admissible words to those rather than asking a program to behave
    16on every input. A program is free to do anything outside the slice, which is what a claim
    17about a special case says.
    18
    19No sorting term appears. Putting nn jobs into earliest-start-time order costs
    20O(nlog⁡n)O(n \log n), which the bound already dominates.
    21
    22The bound does not mention the length of the word, because the length of a word encoding
    23an instance is itself Θ(n)\Theta(n) and the bound dominates it.
    24
    25The domain also asks that every processing time be positive, qj≥1q_j \ge 1. This is the paper's
    26standing assumption for the recursions behind the algorithms — a job with qj=0q_j = 0 has an
    27empty second operation, and the characterization of the feasible sets, on which everything
    28rests, is stated for jobs that have a genuine one — but the paper does not repeat it in each
    29claim, and a statement about a program that reads an arbitrary word has to.
    30-/
    31
    32namespace Lax496464.Corollary1
    33
    34open Lax496464.WordEncoding Lax496464.Problems Lax496464.ParameterizedComplexity
    35open Lax808846.Ram Lax808846.RamComputes
    36
    37open Classical in
    38/-- **Corollary 1.** On one machine with unit weights, the problem is decided within
    39`c · (n+1)²` instructions. -/
    40axiom corollary1_time :
    41 ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    42 ComputesInTime w prog
    43 {x | x ∈ DecisionInstances ∧ Fits c w x ∧ machineCount x = 1 ∧
    44 (∀ j < jobCount x, wt x j = 1) ∧ (∀ j < jobCount x, 0 < procTime x j)}
    45 (fun x => if Yes x then [1] else [0])
    46 (fun x => c * (jobCount x + 1) ^ 2)
    47
    48end Lax496464.Corollary1
    49
    Show Proof
    Formalization Notes

    The claim is about the slice of instances with one machine and unit weights, so the statement restricts the admissible words to those rather than asking a program to behave on every input. A program is free to do anything outside the slice, which is what a claim about a special case says.

    No sorting term appears. Putting nn jobs into earliest-start-time order costs O(nlog⁡n)O(n \log n), which the bound already dominates.

    The bound does not mention the length of the word, because the length of a word encoding an instance is itself Θ(n)\Theta(n) and the bound dominates it.

    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…