The AHL stationary-measure vocabulary — walk decomposition, weights, and marginal sums

This file lands nodes W0–W2 of the Alon–Hoory–Linial irregular-Moore walk-count proof, i.e. the vocabulary the weighted AM–GM assembly (W3–W9) consumes. Building on the non-backtracking machinery of AHL.NBWalkCount / AHL.NBWeighted (nbWalksFrom, nbExtend, nb_concat_iff, card_nbWalksFrom), it packages three layers.

Contents

• W0 — the reusable one-step decomposition. nbWalksFrom_succ_eq_biUnion exhibits the length-(k+1) non-backtracking walks from x as the disjoint biUnion of the one-edge extensions of the length-k walks (k ≥ 1), with pairwiseDisjoint_nbExtend, the fiber cardinality card_nbExtend (= deg (prefix end) − 1), and the endpoint/penultimate fiber facts adj_of_mem_nbExtend / penultimate_of_mem_nbExtend. Both the cardinality (already landed) and every weighted marginal below then reduce through Finset.sum_biUnion. No new mathematics — this simply extracts the decomposition buried in card_nbWalksFrom_succ.
• W1 — the AHL walk weight. nbWeight ⟨v, p⟩ = ∏_{1 ≤ j < len} (deg (getVert j) − 1)⁻¹ (the product over the intermediate vertices only). It is positive under δ ≥ 2 (nbWeight_pos), is 1 on walks of length ≤ 1 (nbWeight_one), and multiplies by exactly (deg end − 1)⁻¹ under a one-edge extension (nbWeight_concat) — the mass-conservation identity driving the exact degree-bias.
• W2 — the marginal sums. Over the global sigma finset nbAll k (all length-k non-backtracking walks, tagged by start): the last-edge marginal nbLastWeight k u v (walks ending at v with penultimate u), the end marginal nbEndWeight k v (walks ending at v), and the total nbWeightTotal k. Their exact values (= 1, = deg v, = D) are AHL's stationarity xP = x, proved in the follow-up node W3–W5, not here; this file lands the defs and their membership rewrite mem_nbAll.

Formalization note — directed edges as (penultimate, end) pairs, not SimpleGraph.Dart

AHL runs its stationary walk over the D directed edges; the xP = x identity is a statement about the last directed edge of a walk. Mathlib offers SimpleGraph.Dart, but the landed counting vocabulary already carries the whole walk, whose last directed edge (penultimate, end) is recovered by Walk.penultimate and the endpoint tag s.1. We therefore formalize a directed edge as that (penultimate, end) pair and phrase the last-edge marginal nbLastWeight as a filter on those two fields — keeping the marginal identities as sums over the already-landed nbWalksFrom finsets with no Dart-to-walk bridge. (Walk.penultimate_concat is already in Mathlib, so the "penultimate of an extension" fiber fact needs no fresh lemma.)

W0 — the reusable one-step decomposition

theorem ACMax.pairwiseDisjoint_nbExtend {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (x : V) (k : ℕ) : (↑(nbWalksFrom G x k)).PairwiseDisjoint (nbExtend G x)

Disjointness of the extension fibers. Over distinct prefix walks the one-edge non-backtracking extension sets nbExtend G x are disjoint: a shared extension p.concat _ determines its prefix p via Walk.concat_inj. This is the disjointness the biUnion decomposition and every weighted regrouping below rely on.

theorem ACMax.card_nbExtend {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {x : V} {s : (v : V) × G.Walk x v} (hnn : ¬s.snd.Nil) : (nbExtend G x s).card = G.degree s.fst - 1

Fiber cardinality. A prefix walk s (non-nil, so its endpoint has a penultimate) has exactly deg s.1 − 1 non-backtracking extensions — one per neighbour of the endpoint other than the arrived-from vertex. This is nb_extension_count transported across the image.

theorem ACMax.penultimate_of_mem_nbExtend {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {x : V} {s s' : (v : V) × G.Walk x v} (hs' : s' ∈ nbExtend G x s) : s'.snd.penultimate = s.fst

Penultimate of an extension. Every extension of s has the prefix endpoint s.1 as its penultimate vertex: the old endpoint becomes the new intermediate vertex. (Immediate from Walk.penultimate_concat.)

theorem ACMax.nbWalksFrom_succ_eq_biUnion {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (x : V) {k : ℕ} (hk : 1 ≤ k) : nbWalksFrom G x (k + 1) = (nbWalksFrom G x k).biUnion (nbExtend G x)

The one-step decomposition (W0). For k ≥ 1, the length-(k+1) non-backtracking walks from x are exactly the disjoint union of the one-edge non-backtracking extensions of the length-k ones. Extracted from the proof of card_nbWalksFrom_succ; the cardinality and every weighted marginal of the AHL assembly are read off this identity via Finset.sum_biUnion.

W1 — the AHL walk weight

noncomputable def ACMax.nbWeight {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {x : V} (s : (v : V) × G.Walk x v) : ℝ

The AHL walk weight. For a length-len non-backtracking walk s = ⟨v, p⟩ starting at x, the weight is the product ∏_{1 ≤ j < len} (deg (p.getVert j) − 1)⁻¹ over the intermediate vertices only (endpoints 0 and len excluded; the empty product is 1 when len ≤ 1). This is AHL's non-returning-walk probability, cleared of the uniform starting mass.

Equations

• ACMax.nbWeight s = ∏ j ∈ Finset.Ico 1 s.snd.length, (↑(G.degree (s.snd.getVert j)) - 1)⁻¹

theorem ACMax.nbWeight_mk {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {x v : V} (p : G.Walk x v) : nbWeight ⟨v, p⟩ = ∏ j ∈ Finset.Ico 1 p.length, (↑(G.degree (p.getVert j)) - 1)⁻¹

Unfolding of nbWeight on an explicit sigma constructor.

theorem ACMax.nbWeight_one {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {x : V} {s : (v : V) × G.Walk x v} (h : s.snd.length ≤ 1) : nbWeight s = 1

The weight is 1 on short walks. For a walk of length ≤ 1 the intermediate range Ico 1 len is empty, so the weight is the empty product 1.

theorem ACMax.nbWeight_pos {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (hδ2 : ∀ (v : V), 2 ≤ G.degree v) {x : V} (s : (v : V) × G.Walk x v) : 0 < nbWeight s

Positivity. Under δ ≥ 2 every factor (deg (getVert j) − 1)⁻¹ is positive, so the whole weight is positive.

theorem ACMax.nbWeight_concat {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {x v t : V} (p : G.Walk x v) (hp : ¬p.Nil) (h : G.Adj v t) : nbWeight ⟨t, p.concat h⟩ = nbWeight ⟨v, p⟩ * (↑(G.degree v) - 1)⁻¹

Weight under a one-edge extension (mass conservation). Extending a non-nil walk p : G.Walk x v by an edge h : G.Adj v t multiplies the weight by exactly (deg v − 1)⁻¹ — the old endpoint v becomes the new intermediate vertex. This is the whole AHL trick: the weighted end-count obeys an exact degree law (unlike the raw end-count).

W2 — the marginal sums

def ACMax.nbAll {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) : Finset ((x : V) × (v : V) × G.Walk x v)

The global sigma finset of all length-k non-backtracking walks, tagged by their start: an element ⟨x, ⟨v, p⟩⟩ is a length-k non-backtracking walk p : G.Walk x v.

Equations

• ACMax.nbAll k = Finset.univ.sigma fun (x : V) => ACMax.nbWalksFrom G x k

theorem ACMax.mem_nbAll {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {k : ℕ} {t : (x : V) × (v : V) × G.Walk x v} : t ∈ nbAll k ↔ t.snd.snd.length = k ∧ IsNonBacktracking t.snd.snd

Membership in nbAll: ⟨x, ⟨v, p⟩⟩ lies in nbAll k iff p has length k and is non-backtracking (the start ranges over all of V).

noncomputable def ACMax.nbLastWeight {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) (u v : V) : ℝ

The last-edge marginal (AHL's xP = x, def only). The total weight of the length-k non-backtracking walks whose last directed edge is (u, v) — i.e. ending at v with penultimate u. Its value 1 (for k ≥ 1, G.Adj u v) is the stationarity identity proved in node W3.

Equations

• ACMax.nbLastWeight k u v = ∑ t ∈ ACMax.nbAll k with t.snd.fst = v ∧ t.snd.snd.penultimate = u, ACMax.nbWeight t.snd

noncomputable def ACMax.nbEndWeight {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) (v : V) : ℝ

The end marginal (def only). The total weight of the length-k non-backtracking walks ending at v; its value deg v (node W4) is the marginal of nbLastWeight over the neighbours of v.

Equations

• ACMax.nbEndWeight k v = ∑ t ∈ ACMax.nbAll k with t.snd.fst = v, ACMax.nbWeight t.snd

noncomputable def ACMax.nbWeightTotal {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) : ℝ

The total weight (def only). The total weight of all length-k non-backtracking walks; its value D = ∑ v, deg v (node W5) is the normalization ∑_v nbEndWeight k v.

Equations

• ACMax.nbWeightTotal k = ∑ t ∈ ACMax.nbAll k, ACMax.nbWeight t.snd