Neighborhood complexity
Lax195003.WelzlOrdersNeighborhoodComplexity · concepts/Lax195003/WelzlOrdersNeighborhoodComplexity.lean · lax-195003
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The neighborhood complexity of a finite graph G is the largest number of distinct traces left by vertex neighborhoods on a set A of at most k vertices. A graph satisfies the linear bound with constant c if for every positive k. A graph class has linear neighborhood complexity if one constant c ≥ 1 works uniformly for every graph in the class.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | import Mathlib.Data.Nat.Lattice |
| 3 | import Mathlib.Data.Set.Card |
| 4 | import Lax199508.GraphClasses |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Neighborhood complexity |
| 9 | type: definition |
| 10 | --- |
| 11 | The neighborhood complexity `π_G(k)` of a finite graph *G* is the largest |
| 12 | number of distinct traces `N(v) ∩ A` left by vertex neighborhoods on a set |
| 13 | *A* of at most *k* vertices. A graph satisfies the linear bound with constant |
| 14 | *c* if `π_G(k) ≤ c · k` for every positive *k*. A graph class has linear |
| 15 | neighborhood complexity if one constant *c* ≥ 1 works uniformly for every |
| 16 | graph in the class. |
| 17 | |
| 18 | # Formalization notes |
| 19 | |
| 20 | The trace count is defined directly as the natural cardinality of the set of |
| 21 | traces. On the finite carrier `Fin n` this is the exact number of distinct |
| 22 | sets `N(v) ∩ A`. Working with `Set` keeps the trace literal and requires no |
| 23 | decidability instances. |
| 24 | |
| 25 | Graph classes use the registered `Lax12.GraphClasses.GraphClass` |
| 26 | representation. The neighborhood trace count itself remains defined locally |
| 27 | below. |
| 28 | |
| 29 | The paper defines the maximum over sets of size at most `k`. On the finite |
| 30 | carrier `Fin n`, the natural supremum below is that maximum. The bound is |
| 31 | required only for positive `k`: at `k = 0`, the empty vertex set has the one |
| 32 | trace `∅`, so the literal inequality `π_G(0) ≤ c · 0` would be false. |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax195003.WelzlOrdersNeighborhoodComplexity |
| 36 | |
| 37 | open Lax199508.GraphClasses |
| 38 | |
| 39 | /-- The number of distinct traces `N(v) ∩ A` that vertex neighborhoods leave |
| 40 | on the vertex set `A`. -/ |
| 41 | noncomputable def traceCount {V : Type*} (G : SimpleGraph V) |
| 42 | (A : Set V) : ℕ := |
| 43 | {S : Set V | ∃ v : V, S = G.neighborSet v ∩ A}.ncard |
| 44 | |
| 45 | /-- The maximum number of distinct neighborhood traces on a vertex set of |
| 46 | cardinality at most `k`. -/ |
| 47 | noncomputable def neighborhoodComplexity {n : ℕ} |
| 48 | (G : SimpleGraph (Fin n)) (k : ℕ) : ℕ := |
| 49 | sSup {q : ℕ | ∃ A : Set (Fin n), |
| 50 | A.ncard ≤ k ∧ q = traceCount G A} |
| 51 | |
| 52 | /-- The graph `G` has neighborhood complexity at most `c · k` for every |
| 53 | positive `k`. -/ |
| 54 | def HasLinearNeighborhoodComplexityWithConstant {n : ℕ} |
| 55 | (G : SimpleGraph (Fin n)) (c : ℕ) : Prop := |
| 56 | ∀ k : ℕ, 1 ≤ k → neighborhoodComplexity G k ≤ c * k |
| 57 | |
| 58 | /-- One natural constant `c ≥ 1` bounds the neighborhood complexity of every |
| 59 | graph satisfying the class predicate `C` by `c · k`: the class has linear |
| 60 | neighborhood complexity. -/ |
| 61 | def HasLinearNeighborhoodComplexity (C : GraphClass) : Prop := |
| 62 | ∃ c : ℕ, 1 ≤ c ∧ |
| 63 | ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → |
| 64 | HasLinearNeighborhoodComplexityWithConstant G c |
| 65 | |
| 66 | end Lax195003.WelzlOrdersNeighborhoodComplexity |
| 67 |
Formalization notes
The trace count is defined directly as the natural cardinality of the set of traces. On the finite carrier this is the exact number of distinct sets . Working with keeps the trace literal and requires no decidability instances.
Graph classes use the registered representation. The neighborhood trace count itself remains defined locally below.
The paper defines the maximum over sets of size at most . On the finite carrier , the natural supremum below is that maximum. The bound is required only for positive : at , the empty vertex set has the one trace , so the literal inequality would be false.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments