Catalog.Sparsity.ShallowMinorComposition
Lemma
Let \(\preccurlyeq_d\) and \(\nabla_d\) be as in Definition ShallowMinor.
If \(J \preccurlyeq_b H\) and \(H \preccurlyeq_a G\) for some \(a, b \in \mathbb{N}\), then \(J \preccurlyeq_{2ab + a + b} G\).
For a graph class \(\mathcal{C}\) and \(d \in \mathbb{N}\), define the depth-\(d\) reduct \(\mathcal{C} \nabla d = \{H : H \preccurlyeq_d G \text{ for some } G \in \mathcal{C}\}\). Then for all \(a, b \in \mathbb{N}\): \[(\mathcal{C} \nabla a) \nabla b \subseteq \mathcal{C} \nabla (2ab + a + b).\]
In particular, if \(\mathcal{C}\) has bounded expansion (resp. is nowhere dense as in Definition NowhereDense), then for every \(b \in \mathbb{N}\) the class \(\mathcal{C} \nabla b\) also has bounded expansion (resp. is nowhere dense).
Review notes
The radius bound \(2ab + a + b\) arises from composing two branch-set traversals: first crossing \(\phi_H(v)\) (radius \(\leq a\)) and then reaching an arbitrary vertex of \(\phi_J(u)\) via a path through at most \(b\) intermediate branch sets, each contributing a crossing of diameter \(\leq 2a\) plus the connecting edge. The reduct closure for nowhere denseness follows because \(\omega_b(\mathcal{C} \nabla a) \leq \omega_{2ab+a+b}(\mathcal{C})\), which is finite when \(\mathcal{C}\) is nowhere dense.
Lean encoding.
The contract introduces ShallowReduct as a definition (body is part of
the trust surface). The reduct is encoded as an existential over types:
\(\exists\, W,\, G : \texttt{SimpleGraph}\;W,\; C(G) \wedge
\texttt{IsShallowMinor}(H, G, d)\).
Two axioms: shallowMinor_trans (composition) and
nowhereDense_shallowReduct (ND closure). The reduct composition
inclusion \((\mathcal{C} \nabla a) \nabla b \subseteq \mathcal{C} \nabla
(2ab+a+b)\) is not stated separately as it follows directly from
shallowMinor_trans and the definition. Bounded expansion closure
is omitted (no catalog definition of bounded expansion).
Catalog/Sparsity/ShallowMinorComposition/Contract.lean (full)
| 1 | import Catalog.Sparsity.Preliminaries.Contract |
| 2 | import Catalog.Sparsity.ShallowMinor.Contract |
| 3 | import Catalog.Sparsity.NowhereDense.Contract |
| 4 | |
| 5 | open Catalog.Sparsity.ShallowMinor |
| 6 | open Catalog.Sparsity.NowhereDense |
| 7 | open Catalog.Sparsity.Preliminaries |
| 8 | |
| 9 | namespace Catalog.Sparsity.ShallowMinorComposition |
| 10 | |
| 11 | /-- The depth-`d` reduct of a graph class `C`: the class of all graphs |
| 12 | that are depth-`d` shallow minors of some graph in `C`. (Def 2.13) -/ |
| 13 | def ShallowReduct (C : GraphClass) (d : ℕ) : GraphClass := |
| 14 | fun {V : Type} [DecidableEq V] [Fintype V] (H : SimpleGraph V) => |
| 15 | ∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (G : SimpleGraph W), |
| 16 | C G ∧ IsShallowMinor H G d |
| 17 | |
| 18 | /-- Lemma 2.12: Composition of shallow minors. |
| 19 | If J ≼_b H and H ≼_a G, then J ≼_{2ab+a+b} G. -/ |
| 20 | axiom shallowMinor_trans |
| 21 | {V W U : Type} {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} |
| 22 | {a b : ℕ} : |
| 23 | IsShallowMinor J H b → IsShallowMinor H G a → |
| 24 | IsShallowMinor J G (2 * a * b + a + b) |
| 25 | |
| 26 | /-- Corollary 2.14: If C is nowhere dense, then C ∇ d is nowhere dense. -/ |
| 27 | axiom nowhereDense_shallowReduct (C : GraphClass) (d : ℕ) : |
| 28 | IsNowhereDense C → IsNowhereDense (ShallowReduct C d) |
| 29 | |
| 30 | end Catalog.Sparsity.ShallowMinorComposition |
| 31 |