Lax195003.WelzlOrdersNeighborhoodComplexity
Neighborhood complexity
concepts/Lax195003/WelzlOrdersNeighborhoodComplexity.lean · lax-195003
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
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.
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 Lax12.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 Lax12.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.
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments