Worked example: web crawling – data acquisition as graph crawling

This file is the library's second tutorial, a companion to DescriptiveComplexity.Examples.ConjunctiveQueries: it walks, step by step, through the addition of a new problem domain, ending in an NP-completeness theorem and a machine-checked concrete encoding. The domain is Web data acquisition: graph crawling, the optimization problem underlying focused crawling of structured documents, formalized by Gauquier–Manolescu–Senellart 2026. A website is a rooted directed graph of pages and hyperlinks; a crawl is an r-rooted subtree; the decision problem asks for a crawl containing every target page within a cost budget. The paper proves this NP-complete (its Prop. 4) already for unit page costs, by reduction from Set Cover; that unit-cost variant is what this file formalizes, following the paper's proof.

The file follows the user-first arc of the conjunctive-query tutorial: start from the concrete problem in the user's own formalism (step 1), construct the encoding with the machinery of DescriptiveComplexity.Encoding – size bounds discharged at construction (step 3) – prove the encoded problem equivalent to the concrete one (step 6), and only then establish the NP-completeness of the encoded variant (steps 7–9), which faithfulness reads back to the concrete instances. Every step exercises machinery the CQ file does not, which is why this example is worth reading second:

• the budget is a cardinality threshold – a number in the unary representation of DescriptiveComplexity.Numbers.Unary, honest here because crawl costs are bounded by the page count – checked by a guessed injection (DescriptiveComplexity.nonempty_embedding_iff_ncard_le);
• the semantics contains a reachability condition, which is not first-order; the membership proof replaces it by a certificate (an order in which every crawled page has a crawled in-neighbour strictly below it), the directed, single-root sibling of the Steiner-tree certificate;
• the hardness reduction is an ordered FO reduction (≤ᶠᵒ[≤]): the paper's budget |U| + B + 1 needs a marked set with exactly one extra element, and a canonical singleton is definable only from an order – the same triage point as for Chromatic Number;
• the concrete instance type is single-sorted with a clamped budget, a second worked instance of DescriptiveComplexity.Encoding after the two-sorted CQ one.

Main results:

• DescriptiveComplexity.GraphCrawling: the bundled decision problem;
• DescriptiveComplexity.graphCrawling_sigmaSODefinable: membership in NP;
• DescriptiveComplexity.setCover_ordered_fo_reduction_graphCrawling : SetCover ≤ᶠᵒ[≤] GraphCrawling: the paper's reduction;
• DescriptiveComplexity.graphCrawling_NP_complete;
• DescriptiveComplexity.crawlEncoding with DescriptiveComplexity.crawlEncoding_faithful: the size-honest concrete encoding and its semantic faithfulness;
• DescriptiveComplexity.crawlDecoding and DescriptiveComplexity.crawlWF_NP_complete: the computable decoding of well-formed (single-root) websites, and completeness restricted to them.

Step 1: the concrete problem, in the user's own formalism

A user does not start from finite structures: they start from the data of their own development. Here that is a packaged crawling instance – a page count, a set of links, a root, a set of targets, a budget – with the textbook semantics as a plain Lean predicate. Nothing in this step mentions model theory; it is the problem as the paper states it, and it is what the final completeness theorem will be about, through the faithfulness theorem of step 5.

structure DescriptiveComplexity.CrawlInstance : Type

A packaged concrete crawling instance: n + 1 pages, the hyperlinks, the root page, the target pages, and the budget (clamped to n + 1 by its type: a crawl never has more pages than the site).

• n : ℕ

  The page count, minus one: pages are Fin (n + 1), so a website is never empty.

• edges : Finset (Fin (self.n + 1) × Fin (self.n + 1))

  The hyperlinks.

• root : Fin (self.n + 1)

  The root page, where crawls start.

• targets : Finset (Fin (self.n + 1))

  The target pages.

• budget : Fin (self.n + 2)

  The budget, clamped by its type: a crawl never has more pages than the site.

def DescriptiveComplexity.instDecidableEqCrawlInstance.decEq (x✝ x✝¹ : CrawlInstance) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCrawlInstance : DecidableEq CrawlInstance

Equations

• DescriptiveComplexity.instDecidableEqCrawlInstance = DescriptiveComplexity.instDecidableEqCrawlInstance.decEq

def DescriptiveComplexity.crawlSize : CrawlInstance → ℕ

The textbook size of a packaged instance: pages, links, targets, and the budget in unary. The one audited line of the encoding.

Equations

• DescriptiveComplexity.crawlSize { n := n, edges := E, root := root, targets := T, budget := B } = n + 1 + E.card + T.card + ↑B

def DescriptiveComplexity.ConcreteCrawlHolds : CrawlInstance → Prop

The textbook semantics of a packaged instance: some set of pages containing the root and every target, each of its pages reachable from the root by links inside it, within budget.

Equations

• One or more equations did not get rendered due to their size.

Step 2: the vocabulary of website graphs

An instance is a single finite structure: the pages, the directed links, a mark for the root, a mark for the targets, and a marked set whose cardinality is the budget – the unary representation of numbers, as used by Set Cover, Steiner Tree and the other threshold problems of the catalog.

inductive FirstOrder.Language.siteGraphRel : ℕ → Type

Relation symbols of the language of website graphs.

• edge : siteGraphRel 2

  edge a b: a hyperlink from page a to page b.

• root : siteGraphRel 1

  root a: the page a is the crawl's starting point.

• target : siteGraphRel 1

  target a: the page a must be crawled.

• marked : siteGraphRel 1

  marked a: the page a belongs to the marked set carrying the budget.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqSiteGraphRel {a✝ : ℕ} : DecidableEq (siteGraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqSiteGraphRel = FirstOrder.Language.instDecidableEqSiteGraphRel.decEq

def FirstOrder.Language.instDecidableEqSiteGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : siteGraphRel a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.siteGraph : Language

The relational language of website graphs: directed links, a root, a set of target pages, and a marked set whose cardinality is the crawling budget.

Equations

• FirstOrder.Language.siteGraph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.siteGraphRel }

instance FirstOrder.Language.instIsRelationalSiteGraph : Language.siteGraph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.wsEdge : Language.siteGraph.Relations 2

The edge symbol of website graphs.

Equations

• FirstOrder.Language.wsEdge = FirstOrder.Language.siteGraphRel.edge

@[reducible, inline]

abbrev FirstOrder.Language.wsRoot : Language.siteGraph.Relations 1

The root symbol of website graphs.

Equations

• FirstOrder.Language.wsRoot = FirstOrder.Language.siteGraphRel.root

@[reducible, inline]

abbrev FirstOrder.Language.wsTarget : Language.siteGraph.Relations 1

The target symbol of website graphs.

Equations

• FirstOrder.Language.wsTarget = FirstOrder.Language.siteGraphRel.target

@[reducible, inline]

abbrev FirstOrder.Language.wsMarked : Language.siteGraph.Relations 1

The mark symbol of website graphs.

Equations

• FirstOrder.Language.wsMarked = FirstOrder.Language.siteGraphRel.marked

Step 3: the encoding, size bounds discharged at construction

With the vocabulary fixed, the concrete instances are encoded as finite structures using DescriptiveComplexity.Encoding: a computable encoder (crawlRelBool, standalone so it can be audited in isolation) and the bundle whose card_le/le_card fields force the encoding to be size-honest – no padding, no compression – before anything is proved about its meaning.

Two packaging choices are dictated by the machinery:

• the budget is clamped by the type (Fin (n + 2)): a crawl never has more than n + 1 pages, so any larger budget is equivalent to n + 1 – and an unclamped ℕ budget, counted in unary in the size, would break le_card exactly as List-repetition would for CQ atoms. The WLOG is baked into the packaging;
• the budget is counted in unary in crawlSize. This is the unary representation of DescriptiveComplexity.Numbers.Unary, and it is honest here because the clamp keeps the budget below the page count – contrast the weighted problems of DescriptiveComplexity/Encoding/UnaryBlowup.lean, where unary weights are exactly what the size bounds reject.

def DescriptiveComplexity.crawlRelBool (i : CrawlInstance) {n : ℕ} (R : FirstOrder.Language.siteGraph.Relations n) : (Fin n → Fin (i.n + 1)) → Bool

The encoder, standalone and auditable (cf. cqRelBool): a plain def, so the compiler vouches that it computes, and the #guards below run it.

Equations

• DescriptiveComplexity.crawlRelBool i FirstOrder.Language.siteGraphRel.edge = fun (x : Fin 2 → Fin (i.n + 1)) => decide ((x 0, x 1) ∈ i.edges)
• DescriptiveComplexity.crawlRelBool i FirstOrder.Language.siteGraphRel.root = fun (x : Fin 1 → Fin (i.n + 1)) => decide (x 0 = i.root)
• DescriptiveComplexity.crawlRelBool i FirstOrder.Language.siteGraphRel.target = fun (x : Fin 1 → Fin (i.n + 1)) => decide (x 0 ∈ i.targets)
• DescriptiveComplexity.crawlRelBool i FirstOrder.Language.siteGraphRel.marked = fun (x : Fin 1 → Fin (i.n + 1)) => decide (↑(x 0) < ↑i.budget)

def DescriptiveComplexity.crawlEncoding : Encoding FirstOrder.Language.siteGraph CrawlInstance

The encoding of packaged crawling instances by Language.siteGraph-structures: the pages themselves as universe, the budget decoded as the marked initial segment DescriptiveComplexity.initSeg. Both size bounds are discharged at construction.

Equations

• One or more equations did not get rendered due to their size.

Step 4: abstract semantics – rooted reachability, crawls, and their certificates

The paper defines a crawl as an r-rooted subtree of the website; the semantics below phrases "some r-rooted subtree with node set S" as "every node of S is reachable from r by edges inside S" – equivalent, since the parent pointers of a breadth-first traversal assemble any such reachable set into a tree, and it is precisely those parent pointers that the first-order certificate recovers (each non-root node has an in-neighbour strictly closer to the root). Reachability itself is a transitive-closure condition, not first-order; as for connectivity in the Steiner-tree problem, the certificate is what makes the membership proof possible, and it reuses the DescriptiveComplexity.reachIn staging for the distance that Relation.ReflTransGen does not carry.

def DescriptiveComplexity.DiLink {A : Type} (Adjp : A → A → Prop) (S : A → Prop) (a b : A) : Prop

The directed step available inside a chosen set: an edge whose two endpoints are both chosen.

Equations

• DescriptiveComplexity.DiLink Adjp S a b = (S a ∧ S b ∧ Adjp a b)

def DescriptiveComplexity.ReachesAllOn {A : Type} (Adjp : A → A → Prop) (r : A) (S : A → Prop) : Prop

Every member of S is reachable from r by directed steps inside S – the shape of an r-rooted subtree with node set S, reachability being all a breadth-first traversal needs to assemble the tree.

Equations

• DescriptiveComplexity.ReachesAllOn Adjp r S = ∀ (x : A), S x → Relation.ReflTransGen (DescriptiveComplexity.DiLink Adjp S) r x

theorem DescriptiveComplexity.reachesAllOn_iff_exists_order {A : Type} [Finite A] (Adjp : A → A → Prop) (r : A) (S : A → Prop) : ReachesAllOn Adjp r S ↔ ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (x : A), S x → x ≠ r → ∃ (y : A), S y ∧ Adjp y x ∧ Lt y x

Rooted reachability is first-order certifiable: every member of S is reachable from r inside S exactly when some strict partial order makes every non-root member of S have a chosen in-neighbour strictly below it. Walking down the order reaches the root; the order “distance to the root” witnesses the converse. The in-neighbours below are the parent pointers of an r-rooted spanning subtree of S.

The crawling property

def DescriptiveComplexity.CrawlOn {A : Type} (Adjp : A → A → Prop) (Rp Tp Kp : A → Prop) : Prop

Some marked root admits a crawl: a set of pages containing the root and every target, entirely reachable from the root inside itself, of size (the paper's total cost, at unit page costs) at most the number encoded by the marked set.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.crawlOn_iff_certificate {A : Type} [Finite A] (Adjp : A → A → Prop) (Rp Tp Kp : A → Prop) : CrawlOn Adjp Rp Tp Kp ↔ ∃ (S : A → Prop), (∀ (x : A), Tp x → S x) ∧ (∃ (Rt : A → Prop), (∃ (x : A), Rt x) ∧ (∀ (x : A), Rt x → Rp x ∧ S x) ∧ (∀ (x y : A), Rt x → Rt y → x = y) ∧ ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (x : A), S x → ¬Rt x → ∃ (y : A), S y ∧ Adjp y x ∧ Lt y x) ∧ Nonempty ({ x : A // S x } ↪ { x : A // Kp x })

The certified form, with reachability witnessed by an order on the chosen set and the budget by an injection into the marked set: the shape the second-order definition guesses. The root is guessed as a relation constrained to hold of exactly one element, which the object language can express.

theorem DescriptiveComplexity.CrawlOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {RB TB KB : B → Prop} {AdjA : A → A → Prop} {RA TA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hR : ∀ (b : B), RB b ↔ RA (u b)) (hT : ∀ (b : B), TB b ↔ TA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) (h : CrawlOn AdjB RB TB KB) : CrawlOn AdjA RA TA KA

CrawlOn transports along an equivalence commuting with the four predicates.

theorem DescriptiveComplexity.CrawlOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {RB TB KB : B → Prop} {AdjA : A → A → Prop} {RA TA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hR : ∀ (b : B), RB b ↔ RA (u b)) (hT : ∀ (b : B), TB b ↔ TA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) : CrawlOn AdjB RB TB KB ↔ CrawlOn AdjA RA TA KA

CrawlOn transports along an equivalence, iff version.

Step 5: isomorphism-invariance and the bundled problem

As always, the invariance proof is a transport of the RelMap shorthands along the isomorphism via the shared relMap_equiv₁/₂ lemmas; the junk conventions were stated with the semantics (a structure marking no root is a no-instance, one marking several is read disjunctively).

def DescriptiveComplexity.WSEdge {A : Type} [FirstOrder.Language.siteGraph.Structure A] (a b : A) : Prop

A hyperlink in a website graph.

Equations

• DescriptiveComplexity.WSEdge a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wsEdge ![a, b]

def DescriptiveComplexity.WSRoot {A : Type} [FirstOrder.Language.siteGraph.Structure A] (a : A) : Prop

Being the root of a website graph.

Equations

• DescriptiveComplexity.WSRoot a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wsRoot ![a]

def DescriptiveComplexity.WSTarget {A : Type} [FirstOrder.Language.siteGraph.Structure A] (a : A) : Prop

Being a target page.

Equations

• DescriptiveComplexity.WSTarget a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wsTarget ![a]

def DescriptiveComplexity.WSMarked {A : Type} [FirstOrder.Language.siteGraph.Structure A] (a : A) : Prop

Belonging to the marked set carrying the budget.

Equations

• DescriptiveComplexity.WSMarked a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wsMarked ![a]

def DescriptiveComplexity.HasCheapCrawl (A : Type) [FirstOrder.Language.siteGraph.Structure A] : Prop

A website graph admits a crawl within budget: a set of pages containing the marked root and every target, reachable from the root inside itself, with at most as many pages as the marked set has elements. (Finiteness of the universe is part of the property: cardinality thresholds are only meaningful on finite structures.)

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.hasCheapCrawl_iso {A B : Type} [FirstOrder.Language.siteGraph.Structure A] [FirstOrder.Language.siteGraph.Structure B] (e : FirstOrder.Language.siteGraph.Equiv A B) : HasCheapCrawl A ↔ HasCheapCrawl B

The crawling property is isomorphism-invariant.

def DescriptiveComplexity.GraphCrawling : DecisionProblem FirstOrder.Language.siteGraph

GRAPH CRAWLING (Gauquier–Manolescu–Senellart 2026, decision variant, unit page costs), as a problem on website graphs: is there a crawl – a set of pages containing the marked root and every target, reachable from the root inside itself – of at most as many pages as the marked set has elements?

Equations

• DescriptiveComplexity.GraphCrawling = { Holds := fun (A : Type) (inst : FirstOrder.Language.siteGraph.Structure A) => DescriptiveComplexity.HasCheapCrawl A, iso_invariant := ⋯ }

Step 6: faithfulness – the encoded problem is the concrete one

The bridge between steps 1 and 5: the abstract problem computes the textbook semantics on every encoded instance (Encoding.Faithful). With the size bounds already discharged by the bundle of step 3, this equivalence is the whole of the encoding obligation – from here on, every theorem about GraphCrawling reads back to the concrete instances. The worked instance and the #guards then run the encoder against a hand computation.

The decoding direction is where well-formedness earns its keep. An abstract structure may mark several roots (read disjunctively by the semantics), and no packaged instance – carrying a single root – transcribes such a structure without deciding which root works, a computation a decoder should not contain. The well-formedness sentence crawlWFSentence ("exactly one root") removes these, and on well-formed structures a computable decoder crawlDecode exists: find the root, read the links, targets and clamped budget off the tables. It assembles into DescriptiveComplexity.crawlDecoding, runs (#guards below), and step 9 restricts the completeness theorem to well-formed instances accordingly (crawlWF_NP_complete). See DescriptiveComplexity/Decoding.lean for why the bundled computation – and not an ∃-only covering statement – is the meaningful notion.

theorem DescriptiveComplexity.crawlEncoding_faithful : crawlEncoding.Faithful ConcreteCrawlHolds GraphCrawling

The packaged encoding is faithful: the abstract problem GraphCrawling computes the textbook semantics on every encoded instance – obligation (1), with obligation (2) already discharged by the bundle.

def DescriptiveComplexity.crawlExample : CrawlInstance

A small worked instance: four pages, root 0, links 0 → 1, 1 → 2 and 0 → 3, targets {2, 3}, budget 4 – a tight yes-instance (both targets need the whole chain through 1).

Equations

• DescriptiveComplexity.crawlExample = { n := 3, edges := {(0, 1), (1, 2), (0, 3)}, root := 0, targets := {2, 3}, budget := 4 }

theorem DescriptiveComplexity.crawlExample_holds : ConcreteCrawlHolds crawlExample

The packaged instance is a concrete yes-instance: crawl everything.

As in the CQ tutorial, the encoder can be run: the #guards evaluate the encoded relations of the worked instance against the hand computation.

The well-formedness sentence, its meaning, and the decoder.

noncomputable def DescriptiveComplexity.crawlWFSentence : FirstOrder.Language.siteGraph.Sentence

Well-formedness of a website graph: exactly one root page. What makes an honest decoder possible.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.realize_crawlWFSentence {A : Type} [FirstOrder.Language.siteGraph.Structure A] : A ⊨ crawlWFSentence ↔ ∃ (x : A), WSRoot x ∧ ∀ (y : A), WSRoot y → y = x

def DescriptiveComplexity.crawlRoots (S : FinPresentation FirstOrder.Language.siteGraph) : Finset (Fin S.card)

The root pages of a presented website.

Equations

• DescriptiveComplexity.crawlRoots S = {x : Fin S.card | S.relBool FirstOrder.Language.wsRoot ![x] = true}

theorem DescriptiveComplexity.mem_crawlRoots (S : FinPresentation FirstOrder.Language.siteGraph) (x : Fin S.card) : x ∈ crawlRoots S ↔ WSRoot x

def DescriptiveComplexity.crawlDecodeAt (S : FinPresentation FirstOrder.Language.siteGraph) (r : Fin S.card) : CrawlInstance

Decode a presented website whose unique root has been found: read the links, targets and budget off the tables, the budget clamped to the page count as the packaging requires. (The root's existence is what makes the page count positive.)

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.crawlDecode (S : FinPresentation FirstOrder.Language.siteGraph) : Option CrawlInstance

The decoder: none unless the site has exactly one root.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.crawlDecode_sound (S : FinPresentation FirstOrder.Language.siteGraph) (i : CrawlInstance) (hi : i ∈ crawlDecode S) : ConcreteCrawlHolds i ↔ GraphCrawling.Holds (Fin S.card)

theorem DescriptiveComplexity.crawlDecode_total (S : FinPresentation FirstOrder.Language.siteGraph) (_hpos : 0 < S.card) (hW : (DecisionProblem.ofSentence crawlWFSentence).Holds (Fin S.card)) : (crawlDecode S).isSome = true

def DescriptiveComplexity.crawlDecoding : Decoding FirstOrder.Language.siteGraph (DecisionProblem.ofSentence crawlWFSentence) ConcreteCrawlHolds GraphCrawling

The computable decoding of well-formed website graphs. Together with crawlEncoding_faithful it closes the loop between the concrete and the abstract problem – a decoder that exists only because well-formedness removed the multi-root structures.

Equations

• DescriptiveComplexity.crawlDecoding = { dec := DescriptiveComplexity.crawlDecode, sound := DescriptiveComplexity.crawlDecode_sound, total := DescriptiveComplexity.crawlDecode_total }

def DescriptiveComplexity.crawlPres : FinPresentation FirstOrder.Language.siteGraph

The worked instance of step 1, presented as raw tables.

Equations

• One or more equations did not get rendered due to their size.

Step 7: membership in NP

NP is defined as Σ₁ second-order definability, so membership means exhibiting a second-order sentence: guess an object-level certificate, check it with a first-order kernel. The certificate is the one of DescriptiveComplexity.crawlOn_iff_certificate: the crawled set, its root, the order witnessing reachability, and the injection witnessing the budget – four relation variables, nine first-order clauses. The construction mirrors the Steiner-tree kernel (DescriptiveComplexity.Problems.Steiner.Membership), with three differences worth spotting: the step clause walks into each crawled page along a directed edge, the guessed root must exist and carry the vocabulary's root mark, and the budget injection is total on the whole crawled set, since the paper's cost counts every crawled page.

inductive DescriptiveComplexity.CrawlGuess : Type

The four relation variables guessed by the Σ₁ definition of Graph Crawling.

• set : CrawlGuess

  The crawled set of pages.

• root : CrawlGuess

  The root the crawl starts from.

• order : CrawlGuess

  The order certifying reachability from the root.

• inj : CrawlGuess

  The injection witnessing the budget.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCrawlGuess : DecidableEq CrawlGuess

Equations

• DescriptiveComplexity.instDecidableEqCrawlGuess x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCrawlGuess : Fintype CrawlGuess

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.crawlGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Graph Crawling.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.cgSetRel : crawlGuessBlock.lang.Relations 1

The symbol of the crawled-set relation variable.

Equations

• DescriptiveComplexity.cgSetRel = ⟨DescriptiveComplexity.CrawlGuess.set, DescriptiveComplexity.cgSetRel._proof_1⟩

def DescriptiveComplexity.cgRootRel : crawlGuessBlock.lang.Relations 1

The symbol of the root relation variable.

Equations

• DescriptiveComplexity.cgRootRel = ⟨DescriptiveComplexity.CrawlGuess.root, DescriptiveComplexity.cgRootRel._proof_1⟩

def DescriptiveComplexity.cgOrderRel : crawlGuessBlock.lang.Relations 2

The symbol of the order relation variable.

Equations

• DescriptiveComplexity.cgOrderRel = ⟨DescriptiveComplexity.CrawlGuess.order, DescriptiveComplexity.cgOrderRel._proof_1⟩

def DescriptiveComplexity.cgInjRel : crawlGuessBlock.lang.Relations 2

The symbol of the injection relation variable.

Equations

• DescriptiveComplexity.cgInjRel = ⟨DescriptiveComplexity.CrawlGuess.inj, DescriptiveComplexity.cgInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.crawlSOLang : FirstOrder.Language

The vocabulary of the kernel.

Equations

• DescriptiveComplexity.crawlSOLang = FirstOrder.Language.siteGraph.sum DescriptiveComplexity.crawlGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kCrEdgeSym : crawlSOLang.Relations 2

The edge symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCrEdgeSym = Sum.inl FirstOrder.Language.wsEdge

@[reducible, inline]

abbrev DescriptiveComplexity.kCrRootMarkSym : crawlSOLang.Relations 1

The root-mark symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCrRootMarkSym = Sum.inl FirstOrder.Language.wsRoot

@[reducible, inline]

abbrev DescriptiveComplexity.kCrTargetSym : crawlSOLang.Relations 1

The target symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCrTargetSym = Sum.inl FirstOrder.Language.wsTarget

@[reducible, inline]

abbrev DescriptiveComplexity.kCrMarkedSym : crawlSOLang.Relations 1

The budget-mark symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCrMarkedSym = Sum.inl FirstOrder.Language.wsMarked

@[reducible, inline]

abbrev DescriptiveComplexity.kCrSetSym : crawlSOLang.Relations 1

The crawled-set symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCrSetSym = Sum.inr DescriptiveComplexity.cgSetRel

@[reducible, inline]

abbrev DescriptiveComplexity.kCrRootSym : crawlSOLang.Relations 1

The root symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCrRootSym = Sum.inr DescriptiveComplexity.cgRootRel

@[reducible, inline]

abbrev DescriptiveComplexity.kCrLtSym : crawlSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCrLtSym = Sum.inr DescriptiveComplexity.cgOrderRel

@[reducible, inline]

abbrev DescriptiveComplexity.kCrInjSym : crawlSOLang.Relations 2

The injection symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kCrInjSym = Sum.inr DescriptiveComplexity.cgInjRel

The clauses

noncomputable def DescriptiveComplexity.crawlKernel : crawlSOLang.Sentence

The first-order kernel of the Σ₁ definition of Graph Crawling.

Equations

• One or more equations did not get rendered due to their size.

Realization

theorem DescriptiveComplexity.graphCrawling_sigmaSODefinable : SigmaSODefinable 1 GraphCrawling

Graph Crawling is Σ₁-definable: guess the crawled set, its root, an order certifying that everything crawled is reachable from the root, and an injection of the crawled set into the marked set, then check the nine conditions first-order.

Step 8: NP-hardness, by reduction from Set Cover

The hardness half follows the paper's proof: a set-cover instance becomes a depth-2 website – a root linking to one page per set of the family, each set page linking to the elements it contains – whose targets are the elements, and a cover of at most B sets is exactly a crawl of at most |U| + B + 1 pages (the root, the chosen sets, and all the elements).

The budget |U| + B + 1 is assembled per tag: the marked set of the produced instance is the elements (on the element tag, |U|), the marked elements of the source (on the set tag, B), and one copy of the minimum of the input's order (on the root tag, 1). The + 1 is why this is an ordered reduction: a marked set with exactly one more element needs a canonical singleton, which only an order provides. The root mark and the root's out-edges are guarded by minimality too, so the junk copies of the root tag are unmarked and edgeless.

Cardinality bookkeeping is by tag slices: a set of interpreted elements that is a per-tag family of subsets of the input has as cardinality the sum of the slices (DescriptiveComplexity.ncard_tagged_eq_sum), and both the crawl produced from a cover and the marked set decompose this way, so both directions of the correctness proof reduce to arithmetic on three slice sizes.

inductive DescriptiveComplexity.CrawlTag : Type

Tags for the interpretation of website graphs in set systems.

• root : CrawlTag

  (root, a): a copy of the crawl root (only the copy of the minimum is marked as root, linked, and counted).

• fam : CrawlTag

  (fam, a): the page of the set a of the family.

• elem : CrawlTag

  (elem, a): the page of the ground element a – a target.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCrawlTag : DecidableEq CrawlTag

Equations

• DescriptiveComplexity.instDecidableEqCrawlTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.instNonemptyCrawlTag : Nonempty CrawlTag

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCrawlTag : Fintype CrawlTag

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev DescriptiveComplexity.oSSElem : (FirstOrder.Language.setSystem.sum FirstOrder.Language.order).Relations 1

The ground-element symbol over the ordered expansion of set systems.

Equations

• DescriptiveComplexity.oSSElem = Sum.inl FirstOrder.Language.ssElem

@[reducible, inline]

abbrev DescriptiveComplexity.oSSFam : (FirstOrder.Language.setSystem.sum FirstOrder.Language.order).Relations 1

The family symbol over the ordered expansion of set systems.

Equations

• DescriptiveComplexity.oSSFam = Sum.inl FirstOrder.Language.ssFam

@[reducible, inline]

abbrev DescriptiveComplexity.oSSMem : (FirstOrder.Language.setSystem.sum FirstOrder.Language.order).Relations 2

The incidence symbol over the ordered expansion of set systems.

Equations

• DescriptiveComplexity.oSSMem = Sum.inl FirstOrder.Language.ssMem

@[reducible, inline]

abbrev DescriptiveComplexity.oSSMarked : (FirstOrder.Language.setSystem.sum FirstOrder.Language.order).Relations 1

The mark symbol over the ordered expansion of set systems.

Equations

• DescriptiveComplexity.oSSMarked = Sum.inl FirstOrder.Language.ssMarked

noncomputable def DescriptiveComplexity.crawlInterp : FOInterpretation (FirstOrder.Language.setSystem.sum FirstOrder.Language.order) FirstOrder.Language.siteGraph CrawlTag 1

The interpretation producing, from a set system, the depth-2 website of the paper's reduction: the minimum's root copy links to every set of the family, each set links to its elements, the elements are the targets, and the marked set carries |U| + B + 1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DescriptiveComplexity.crawl_edge_iff {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (t t' : CrawlTag) (w w' : Fin 1 → A) : WSEdge (t, w) (t', w') ↔ t = CrawlTag.root ∧ t' = CrawlTag.fam ∧ (∀ (a : A), w 0 ≤ a) ∧ SSFam (w' 0) ∨ t = CrawlTag.fam ∧ t' = CrawlTag.elem ∧ (SSMem (w' 0) (w 0) ∧ SSFam (w 0)) ∧ SSElem (w' 0)

@[simp]

theorem DescriptiveComplexity.crawl_root_iff {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (t : CrawlTag) (w : Fin 1 → A) : WSRoot (t, w) ↔ t = CrawlTag.root ∧ ∀ (a : A), w 0 ≤ a

@[simp]

theorem DescriptiveComplexity.crawl_target_iff {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (t : CrawlTag) (w : Fin 1 → A) : WSTarget (t, w) ↔ t = CrawlTag.elem ∧ SSElem (w 0)

@[simp]

theorem DescriptiveComplexity.crawl_marked_iff {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (t : CrawlTag) (w : Fin 1 → A) : WSMarked (t, w) ↔ match t with | CrawlTag.root => ∀ (a : A), w 0 ≤ a | CrawlTag.fam => SSMarked (w 0) | CrawlTag.elem => SSElem (w 0)

Counting by tag slices

def DescriptiveComplexity.InSlices {A : Type} (s : CrawlTag → Set A) (p : CrawlTag × (Fin 1 → A)) : Prop

Membership in a per-tag family of subsets of the input, stated at the raw product type so that it applies to interpreted elements.

Equations

• DescriptiveComplexity.InSlices s p = (p.2 0 ∈ s p.1)

theorem DescriptiveComplexity.ncard_inSlices {A : Type} [Finite A] (s : CrawlTag → Set A) : {p : crawlInterp.Map A | InSlices s p}.ncard = (s CrawlTag.root).ncard + (s CrawlTag.fam).ncard + (s CrawlTag.elem).ncard

The cardinality of a per-tag family of slices is the sum of the slice sizes.

def DescriptiveComplexity.coverSlices {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (G : A → Prop) : CrawlTag → Set A

The tag slices of the crawl produced from a subfamily G: the minimum on the root tag, G on the set tag, the ground elements on the element tag. Instantiated at G := SSMarked this is also the decomposition of the marked set.

Equations

• DescriptiveComplexity.coverSlices G DescriptiveComplexity.CrawlTag.root = {a : A | ∀ (b : A), a ≤ b}
• DescriptiveComplexity.coverSlices G DescriptiveComplexity.CrawlTag.fam = {a : A | G a}
• DescriptiveComplexity.coverSlices G DescriptiveComplexity.CrawlTag.elem = {a : A | DescriptiveComplexity.SSElem a}

theorem DescriptiveComplexity.ncard_min_slice {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : {a : A | ∀ (b : A), a ≤ b}.ncard = 1

On a finite linearly ordered nonempty type, the set of minima is a singleton.

theorem DescriptiveComplexity.marked_eq_slices {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] : {p : crawlInterp.Map A | WSMarked p} = {p : crawlInterp.Map A | InSlices (coverSlices SSMarked) p}

The marked set of the interpreted website decomposes into tag slices.

Correctness

theorem DescriptiveComplexity.hasSmallSetCover_iff_crawl_map (A : Type) [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : HasSmallSetCover A ↔ HasCheapCrawl (crawlInterp.Map A)

Correctness of the interpretation: the set system has a small cover iff the interpreted website has a cheap crawl.

noncomputable def DescriptiveComplexity.setCover_ordered_fo_reduction_graphCrawling : OrderedFOReduction SetCover GraphCrawling

Set Cover ordered-FO-reduces to Graph Crawling – the reduction of Gauquier–Manolescu–Senellart 2026, Prop. 4: a cover of at most B sets is a crawl of at most |U| + B + 1 pages of the depth-2 website.

Equations

• One or more equations did not get rendered due to their size.

Step 9: completeness

Membership and hardness combine into the completeness theorem – the formalized counterpart of Prop. 4 of Gauquier–Manolescu–Senellart 2026. Through the faithfulness theorem of step 6, it is a statement about the packaged concrete instances of step 1: ConcreteCrawlHolds is decided by a problem that is NP-complete, over an encoding that provably neither pads nor compresses.

theorem DescriptiveComplexity.graphCrawling_mem_NP : NP.Mem GraphCrawling

Graph Crawling is in NP.

theorem DescriptiveComplexity.graphCrawling_NP_hard : NP.Hard GraphCrawling

Graph Crawling is NP-hard: Set Cover, which is NP-hard, reduces to it by an ordered FO reduction.

theorem DescriptiveComplexity.graphCrawling_NP_complete : NP.Complete GraphCrawling

The graph crawling problem is NP-complete (Gauquier–Manolescu–Senellart 2026, Prop. 4).

theorem DescriptiveComplexity.crawlInterp_wf (A : Type) [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (DecisionProblem.ofSentence crawlWFSentence).Holds (crawlInterp.Map A)

The image of the hardness reduction is well-formed: the only root-marked page of an interpreted website is the minimum's root copy.

theorem DescriptiveComplexity.crawlWF_NP_complete : NP.Complete (DecisionProblem.ofSentence crawlWFSentence ⊓ GraphCrawling)

Well-formed graph crawling is NP-complete: crawling restricted to websites with exactly one root – the instances the decoder of step 6 handles. Both halves are one-line upgrades of the plain completeness proof (OrderedFOReduction.withInvariant, SigmaSODefinable.inf_ofSentence).