Lax Lean Archive

Corollary 4

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

    There exists an FPT-reduction from Hitting Set, parameterized by solution size, to just-in-time scheduling parameterized by the number of second-stage machines. The construction preserves the parameter: a hitting-set instance with solution size kk produces a shop with exactly kk machines.

    The W[2]-hardness consequence follows from the W[2]-hardness of Hitting Set.

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

    Lean source view on GitHub

    1import Lax496464.Construction
    2import Lax496464.Problems
    3import Lax496464.W2Hardness
    4
    5/-!
    6---
    7title: Corollary 4
    8type: theorem
    9---
    10There exists an FPT-reduction from Hitting Set, parameterized by solution size, to
    11just-in-time scheduling parameterized by the number of second-stage machines.
    12The construction preserves the parameter: a hitting-set instance with solution size
    13kk produces a shop with exactly kk machines.
    14
    15The W[2]-hardness consequence follows from the W[2]-hardness of Hitting Set.
    16
    17# Formalization Notes
    18
    19The statement uses `W2Hard`, which unfolds to the existence of this reduction.
    20Its proof establishes correctness and the required running-time and parameter bounds.
    21It does not depend on the supporting `WH_*` development, included for completeness
    22beyond the scope of the scheduling project.
    23-/
    24
    25namespace Lax496464.Corollary4
    26
    27open Lax496464.Problems Lax496464.W2Hardness
    28
    29/-- **Corollary 4.** The problem is W[2]-hard with respect to the number of machines. -/
    30axiom w2Hard_byMachines : W2Hard byMachines
    31
    32end Lax496464.Corollary4
    33
    Show Proof
    Formalization Notes

    The statement uses W2HardW2Hard, which unfolds to the existence of this reduction. Its proof establishes correctness and the required running-time and parameter bounds. It does not depend on the supporting WH∗WH_* development, included for completeness beyond the scope of the scheduling project.

    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…