Lax Lean Archive

Decoding, and well-formed graph crawling is NP-complete

Lax117614.CrawlDecoding · concepts/Lax117614/CrawlDecoding.lean · lax-117614

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 decoder is sound: an instance it reads off a presented website has a crawl within budget exactly when the presented website graph is a yes-instance of the graph crawling problem. It is total on well-formed websites: every nonempty presented website with exactly one root decodes to an instance. And well-formed graph crawling, whose yes-instances are exactly the website graphs with one root and a cheap crawl, is NP-complete, so the restriction the decoder needs loses nothing.

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

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 crawlDecode_sound proven

    2 crawlDecode_total proven

    3 wfGraphCrawling_iff proven

    4 wfGraphCrawling_NP_complete proven

    Lean source view on GitHub

    1import Lax904597.Classes
    2import Lax117614.WebsiteGraphs
    3import Lax117614.GraphCrawlingProblem
    4import Lax117614.CrawlInstances
    5
    6/-!
    7---
    8title: Decoding, and well-formed graph crawling is NP-complete
    9type: theorem
    10---
    11The decoder is sound: an instance it reads off a presented website has a
    12crawl within budget exactly when the presented website graph is a
    13yes-instance of the graph crawling problem. It is total on well-formed
    14websites: every nonempty presented website with exactly one root decodes
    15to an instance. And well-formed graph crawling, whose yes-instances are
    16exactly the website graphs with one root and a cheap crawl, is NP-complete,
    17so the restriction the decoder needs loses nothing.
    18-/
    19
    20namespace Lax117614.CrawlDecoding
    21
    22open FirstOrder FirstOrder.Language Structure
    23open Lax904597.Problems Lax904597.Classes
    24open Lax117614.WebsiteGraphs Lax117614.GraphCrawlingProblem Lax117614.CrawlInstances
    25
    26/-- The decoder is sound: an instance it reads off a presented website has a
    27crawl within budget exactly when the presented website graph is a
    28yes-instance of GraphCrawling. -/
    29axiom crawlDecode_sound : ∀ (S : FinPresentation siteGraph) (i : CrawlInstance),
    30 i ∈ crawlDecode S → (ConcreteCrawlHolds i ↔ GraphCrawling (Fin S.card))
    31
    32/-- The decoder is total on well-formed websites: a nonempty presented website
    33with exactly one root decodes to an instance. -/
    34axiom crawlDecode_total : ∀ S : FinPresentation siteGraph,
    35 0 < S.card → Fin S.card ⊨ crawlWFSentence → (crawlDecode S).isSome
    36
    37/-- The yes-instances of WFGraphCrawling are exactly the website graphs with
    38exactly one root satisfying `HasCheapCrawl`. -/
    39axiom wfGraphCrawling_iff : ∀ (A : Type) [siteGraph.Structure A],
    40 WFGraphCrawling A ↔ (A ⊨ crawlWFSentence ∧ HasCheapCrawl A)
    41
    42/-- WFGraphCrawling is NP-complete: the restriction to well-formed websites
    43loses nothing. -/
    44axiom wfGraphCrawling_NP_complete : NP.Complete WFGraphCrawling
    45
    46end Lax117614.CrawlDecoding
    47
    Show ProofShow ProofShow ProofShow 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…