Documentation

Formalizations.Combinatorics.SimpleGraph.Ihara.MomentBridge

Tree-like walks are walks on the path tree #

The projection T(G, v) → G that sends a path to its endpoint is a graph homomorphism. It maps the closed walks at the root of the path tree bijectively onto the closed tree-like walks of G at v. Hence the number of closed tree-like walks of length k is ∑_v (A(T(G, v))ᵏ)_{root, root}, and by Godsil's identity the matching polynomial of G controls the root resolvent of each path tree.

Main definitions #

Main results #

References #

source
def SimpleGraph.pathTreeProj {V : Type u_1} (G : SimpleGraph V) (u : V) :
G.pathTree u →g G

The down-projection π : T(G,v) →g G, sending a path-tree vertex (a path of G from v) to its endpoint. Adjacency in the path tree means one path extends the other by a single edge, so the two endpoints are adjacent in G; hence π is a graph homomorphism. This is the map along which closed walks at the root of the (forest) path tree project to closed tree-like walks of G.

Equations
Instances For
    source
    @[simp]
    theorem SimpleGraph.pathTreeProj_apply {V : Type u_1} (G : SimpleGraph V) (u : V) (a : G.PathFrom u) :
    (G.pathTreeProj u) a = a.fst
    source
    @[simp]
    theorem SimpleGraph.pathTreeProj_root {V : Type u_1} (G : SimpleGraph V) (u : V) :
    (G.pathTreeProj u) (G.pathTreeRoot u) = u

    The projection sends the path-tree root (the trivial path at u) to u.

    source
    theorem SimpleGraph.pathTreeProj_map_length {V : Type u_1} {G : SimpleGraph V} {u : V} (w : (G.pathTree u).Walk (G.pathTreeRoot u) (G.pathTreeRoot u)) :
    (Walk.map (G.pathTreeProj u) w).length = w.length

    A closed walk at the root of the path tree projects, under π, to a closed walk at u of G of the same length: this is the map whose image is exactly the tree-like walks (next lemma).

    Local injectivity of the projection (the path tree is an immersion of G) #

    The bijection "closed walks at the root of T(G,v) ↔ closed tree-like walks of G at v" is realised by Walk.map (pathTreeProj G v). Its injectivity rests on a purely local fact: π is injective on the neighbours of each path-tree vertex p. The neighbours of p are its unique parent (dropLast) and its children (one-edge extensions); π sends the parent to p's penultimate vertex (which lies on p) and each child to its fresh endpoint (which does not), and distinct children have distinct endpoints — so the projection separates all neighbours of p.

    source
    theorem SimpleGraph.Grows.child_unique {V : Type u_1} {G : SimpleGraph V} {u : V} {p a a' : G.PathFrom u} (h : Grows p a) (h' : Grows p a') (hv : a.fst = a'.fst) :
    a = a'

    Child uniqueness (dual of Grows.parent_unique): a one-edge extension of p is determined by its endpoint. If a and a' both grow from p and share an endpoint, they are equal.

    source
    theorem SimpleGraph.pathTreeProj_injOn_neighborSet {V : Type u_1} (G : SimpleGraph V) (u : V) (p : G.PathFrom u) :
    Set.InjOn (⇑(G.pathTreeProj u)) ((G.pathTree u).neighborSet p)

    π is injective on the neighbour set of each path-tree vertex — the path tree is an immersion of G. Parents coincide by parent_unique, children by child_unique; a child's endpoint is fresh (∉ p.support) while a parent's endpoint is p's penultimate (∈ p.support), so the two families never collide. This local injectivity drives the walk-lift bijection.

    source
    theorem SimpleGraph.pathTreeProj_walk_injective {V : Type u_1} {G : SimpleGraph V} {v : V} {x y : G.PathFrom v} (p p' : (G.pathTree v).Walk x y) :
    Walk.map (G.pathTreeProj v) p = Walk.map (G.pathTreeProj v) p' → p = p'

    Walk.map π is injective on walks of the path tree (with fixed endpoints): a walk of the forest T(G,v) is recovered from its G-projection. By induction, each step's next vertex is a neighbour of the current one, and π separates neighbours (pathTreeProj_injOn_neighborSet), so the lift is forced — the injective half of the lemma-1 bijection.

    The liftSeq↔path invariant (image is tree-like + surjectivity of the lift) #

    liftSeq (the intrinsic tree-like test of PathTreeLift) run on a projected path-tree walk tracks the current tree-vertex's path. One step in T(G,v) — Grows s y (extend) or Grows y s (retreat to parent) — mirrors exactly one liftSeq step (EXTEND push / RETREAT pop).

    source
    theorem SimpleGraph.liftSeq_step {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v : V} {s y : G.PathFrom v} (h : (G.pathTree v).Adj s y) (M : List V) :
    liftSeq (y.fst :: M) (↑s.snd).support = liftSeq M (↑y.snd).support

    One path-tree step = one liftSeq step. Walking T(G,v) from s to a neighbour y, feeding liftSeq the next projected vertex y.1 with stack s's path-support turns the stack into y's path-support: an EXTEND when y is a child of s (fresh endpoint, push) and a RETREAT when y is its parent (endpoint = penultimate, pop).

    source
    theorem SimpleGraph.liftSeq_map_invariant {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v : V} {s x : G.PathFrom v} (W : (G.pathTree v).Walk s x) :
    liftSeq (Walk.map (G.pathTreeProj v) W).support.tail (↑s.snd).support = some (↑x.snd).support

    The invariant. Running liftSeq on the G-projection of a path-tree walk W : s ⟶ x, started from s's path-support, returns x's path-support. Each tree step is one liftSeq step (liftSeq_step), so the stack walks in lockstep with the current tree-vertex's path.

    source
    theorem SimpleGraph.pathTreeProj_map_isTreeLike {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v : V} (W : (G.pathTree v).Walk (G.pathTreeRoot v) (G.pathTreeRoot v)) :
    (Walk.map (G.pathTreeProj v) W).IsTreeLike

    Image is tree-like (down well-definedness). The G-projection of any closed walk at the root of T(G,v) is a tree-like closed walk at v: instantiate the invariant at s = x = root, whose path-support is [v], giving liftSeq (W.map π).support.tail [v] = some [v], i.e. IsTreeLike.

    Surjectivity of the lift (the last half of the lemma-1 bijection) #

    Conversely, a G-walk that liftSeq accepts from a current tree-vertex ⟨a, pp⟩ lifts to a path-tree walk projecting back to it. The hypothesis liftSeq w.support.tail pp.support = some t supplies, at each step, exactly the EXTEND (fresh vertex → child) or RETREAT (penultimate → parent) decision, so the lift is built by recursion with no failure branch.

    source
    theorem SimpleGraph.exists_lift {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v a b : V} (w : G.Walk a b) (pp : G.Walk v a) (hpp : pp.IsPath) {t : List V} :
    liftSeq w.support.tail pp.support = some t → ∃ (q : G.PathFrom v) (W : (G.pathTree v).Walk ⟨a, ⟨pp, hpp⟩⟩ q), (Walk.map (G.pathTreeProj v) W).support = w.support ∧ (↑q.snd).support = t

    Existence of the lift. If liftSeq accepts the G-walk w : a ⟶ b started from the path pp : v ⟶ a (current tree-vertex ⟨a, pp⟩), returning final stack t, then w lifts to a path-tree walk W from ⟨a, pp⟩ to a vertex q with q's path-support = t whose projection has the same support as w. (Support equality dodges the dependent endpoint; support_injective upgrades it to walk equality once the endpoints are pinned, in the closed-walk corollary.)

    source
    theorem SimpleGraph.exists_root_lift {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v : V} (w : G.Walk v v) (hw : w.IsTreeLike) :
    ∃ (W : (G.pathTree v).Walk (G.pathTreeRoot v) (G.pathTreeRoot v)), Walk.map (G.pathTreeProj v) W = w

    Surjectivity of the projection onto tree-like walks. Every closed tree-like walk of G at v is the π-projection of a closed walk at the root of T(G,v): lift it from the root path (exists_lift), note the lift returns to the root (its final path-support is [v]), and upgrade the support equality to walk equality via support_injective.

    The lemma-1 count equality #

    Assembling the bijection: the number of closed tree-like walks of G at v of length k equals the number of closed walks of length k at the root of the path tree T(G,v). This is the matching-side input treeLikeWalkCount-summand = [A(T(G,v))ᵏ]_{root} of Godsil's moment theorem.

    source
    theorem SimpleGraph.card_treeLike_eq_pathTreeWalks {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) (v : V) :
    {w ∈ G.finsetWalkLength k v v | w.IsTreeLike}.card = ((G.pathTree v).finsetWalkLength k (G.pathTreeRoot v) (G.pathTreeRoot v)).card

    Lemma 1 (count form). #{closed tree-like walks of Gatv, length k} = #{closed walks at the root of T(G,v), length k}, via the bijection W ↦ W.map π (injective pathTreeProj_walk_injective, image-is-tree-like pathTreeProj_map_isTreeLike, surjective exists_root_lift).

    source
    theorem SimpleGraph.treeLikeWalkCount_eq_sum_pathTree_adjMatrix_pow {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) :
    treeLikeWalkCount k = ∑ v : V, (adjMatrix ℕ (G.pathTree v) ^ k) (G.pathTreeRoot v) (G.pathTreeRoot v)

    Lemma 1 → linear algebra. Godsil's tree-like walk count is the sum, over base vertices v, of the root–root entry of the k-th power of the path tree's adjacency matrix:

    treeLikeWalkCount G k = ∑_v [A(T(G,v))ᵏ]_{root,root}.

    Combines card_treeLike_eq_pathTreeWalks (the lemma-1 bijection) with adjMatrix_pow_apply_eq_card_walk (matrix powers count walks). This is the matching side of the trace-formula bridge expressed spectrally on each path tree — the entry point to the resolvent / Newton lemmas ([A(T)ᵏ]_root = the k-th moment coefficient of μ(T−root)/μ(T)).

    source
    theorem SimpleGraph.matchingPoly_pathTree_eq_charpoly {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (v : V) :
    (G.pathTree v).matchingPoly = (adjMatrix ℝ (G.pathTree v)).charpoly

    The path tree is a forest, so its matching polynomial is the characteristic polynomial of its adjacency matrix (matchingPoly_forest_eq_charpoly at pathTree_isAcyclic). This identifies the spectral object charpoly(A(T(G,v))) — whose (root,root) resolvent generates [A(T)ᵏ]_root — with the matching polynomial μ(T(G,v)) that enters Godsil's ratio identity μ(T−root)/μ(T) = μ(G−v)/μ(G). The hinge between the linear-algebra side (lemma 3) and the matching-polynomial side (lemma 2 = godsil_identity).

    source
    theorem SimpleGraph.godsil_resolvent_charpoly_form {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (u : V) :
    (adjMatrix ℝ ((G.pathTree u).deleteIncidenceSet (G.pathTreeRoot u))).charpoly * G.matchingPoly = (adjMatrix ℝ (G.pathTree u)).charpoly * (G.deleteIncidenceSet u).matchingPoly

    Lemma 2 in resolvent (charpoly) form. Substituting the forest bridge μ(forest) = charpoly(adjacency) into Godsil's identity godsil_identity (μ(G)·μ(T−r) = μ(G−u)·μ(T), the matching↔path-tree ratio, Divisibility) turns the matching-polynomial ratio into the spectral one:

    charpoly(A(T(G,u)−r)) · μ(G) = charpoly(A(T(G,u))) · μ(G−u),

    i.e. the path tree's root–root resolvent charpoly(T−r)/charpoly(T) equals the graph ratio μ(G−u)/μ(G). (T−r and G−u are the incidence-isolated forms deleteIncidenceSet, so both sides carry the same isolated-vertex factor X.) This is the exact spectral input that the generating-function step (Lemma 3) consumes — the diagonal resolvent Σ_k [A(T)ᵏ]_root z^k = charpoly(T−r)/charpoly(T) is now pinned to μ(G−u)/μ(G), which the vertex-deletion law sum_matchingPoly_deleteIncidenceSet sums (over u) to μ'(G)/μ(G). Both forest bridges are sound: T is acyclic (pathTree_isAcyclic) and T−r ≤ T stays acyclic (IsAcyclic.anti).