Lax Lean Archive

The reduction can be computed in polynomial time

Lax222097.ReductionTime · concepts/Lax222097/ReductionTime.lean · lax-222097

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

    Lemma

    The map (F,k)↦(GF,k+b(F))(F,k)\mapsto(G_F,k+b(F)) can be computed in polynomial time. The output vertices may be relabeled as consecutive integers.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax222097.Reduction
    2
    3/-!
    4---
    5title: The reduction can be computed in polynomial time
    6type: lemma
    7---
    8The map (F,k)↦(GF,k+b(F))(F,k)\mapsto(G_F,k+b(F)) can be computed in polynomial time.
    9The output vertices may be relabeled as consecutive integers.
    10-/
    11
    12namespace Lax222097.ReductionTime
    13
    14open GraphEncoding Reduction
    15
    16axiom reduction_polynomial_time :
    17 ∃ f : Instance → Instance,
    18 PolynomialTime f ∧
    19 ∀ I, Nonempty ((f I).graph ≃g reductionGraph I.graph) ∧
    20 (f I).threshold = I.threshold + offset I.graph
    21
    22end Lax222097.ReductionTime
    23
    Show Proof
    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…