The AHL stationary marginal VALUES — xP = x and its consequences (nodes W3–W5)

This file lands nodes W3–W5 of the Alon–Hoory–Linial irregular-Moore walk-count proof, the hard node of the ladder. Building on the weight vocabulary of AHL.AHLStationary (nbWeight, nbWeight_concat, nbWalksFrom_succ_eq_biUnion, the marginal defs nbLastWeight/nbEndWeight/nbWeightTotal), it proves that the weighted marginals attain their exact stationary values — the degree-bias is an identity, not an inequality.

Throughout hδ2 : ∀ v, 2 ≤ G.degree v. A directed edge is the (penultimate, end) pair of a walk.

Contents

• W3 — the last-edge marginal (nbLastWeight_eq_one, AHL's xP = x). For every k ≥ 1 and every directed edge (u, v) (G.Adj u v), the total weight of the length-k non-backtracking walks whose last directed edge is (u, v) is exactly 1. Proved by induction on k: the concat step splits a prefix's mass (deg end − 1)⁻¹ to each of its deg end − 1 extensions (nbWeight_concat), so the mass through each dart is invariant. The engine is nbLastWeight_succ_eq, the exact one-step recursion built from the extension bijection.
• W4 — the end marginal (nbEndWeight_eq_degree). The total weight of the length-k non-backtracking walks ending at v is exactly deg v; it is the marginal of nbLastWeight over the neighbours of v.
• W5 — the total (nbWeightTotal_eq). The total weight of all length-k non-backtracking walks is exactly D = ∑ v, deg v — the normalization the weighted AM–GM (W7) consumes.

theorem ACMax.penultimate_of_length_one {V : Type u_1} {G : SimpleGraph V} {x w : V} {p : G.Walk x w} (hp : p.length = 1) : p.penultimate = x

Penultimate of a length-1 walk is its start. A one-edge walk x → w has penultimate vertex getVert 0 = x.

The per-start expansion of a marginal sum

theorem ACMax.sum_nbAll_filter {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) (Q : V → V → Prop) [DecidableRel Q] : ∑ t ∈ nbAll k with Q t.snd.fst t.snd.snd.penultimate, nbWeight t.snd = ∑ x : V, ∑ s ∈ nbWalksFrom G x k with Q s.fst s.snd.penultimate, nbWeight s

Sigma-to-per-start expansion. A weighted marginal filtered by a predicate Q of the (end, penultimate) pair equals the sum over starts x of the per-start filtered weight. This is Finset.sum_sigma for the nbAll = univ.sigma nbWalksFrom decomposition.

theorem ACMax.nbLastWeight_eq_sum {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) (u v : V) : nbLastWeight k u v = ∑ x : V, ∑ s ∈ nbWalksFrom G x k with s.fst = v ∧ s.snd.penultimate = u, nbWeight s

The last-edge marginal nbLastWeight k u v, written as a sum over starts of the per-start weight of length-k walks ending at v with penultimate u.

theorem ACMax.sum_R_eq_sum {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (k : ℕ) (u v : V) : ∑ t ∈ nbAll k with t.snd.fst = u ∧ t.snd.snd.penultimate ≠ v, nbWeight t.snd = ∑ x : V, ∑ s ∈ nbWalksFrom G x k with s.fst = u ∧ s.snd.penultimate ≠ v, nbWeight s

The prefix (source) sum of the extension bijection, written as a sum over starts. These are the length-k walks ending at u whose penultimate avoids v (so they extend to v).

The one-step extension identity (the core of W3)

theorem ACMax.sum_nbExtend_ite {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {u v : V} (huv : G.Adj u v) {x : V} {k : ℕ} (hk : 1 ≤ k) {s' : (w : V) × G.Walk x w} (hs' : s' ∈ nbWalksFrom G x k) : (∑ s ∈ nbExtend G x s', if s.fst = v ∧ s.snd.penultimate = u then nbWeight s else 0) = if s'.fst = u ∧ s'.snd.penultimate ≠ v then nbWeight s' * (↑(G.degree u) - 1)⁻¹ else 0

The per-prefix extension mass. For a length-k non-backtracking prefix s' (k ≥ 1), the weight it contributes to length-(k+1) walks with last edge (u, v) is nbWeight s' · (deg u −1)⁻¹ when s' ends at u and its penultimate avoids v (so the extension to v is non-backtracking), and 0 otherwise. This is the mass-conservation identity behind xP = x.

theorem ACMax.innerLast_succ {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {u v : V} (huv : G.Adj u v) (x : V) {k : ℕ} (hk : 1 ≤ k) : ∑ s ∈ nbWalksFrom G x (k + 1) with s.fst = v ∧ s.snd.penultimate = u, nbWeight s = (∑ s' ∈ nbWalksFrom G x k with s'.fst = u ∧ s'.snd.penultimate ≠ v, nbWeight s') * (↑(G.degree u) - 1)⁻¹

Per-start one-step recursion. For a fixed start x and k ≥ 1, the per-start weight of length-(k+1) walks with last edge (u, v) is the per-start prefix mass (walks ending at u whose penultimate avoids v) scaled by (deg u − 1)⁻¹. Assembled from the biUnion decomposition and sum_nbExtend_ite.

theorem ACMax.sum_R_eq_sum_lastWeight {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {u v : V} (huv : G.Adj u v) {k : ℕ} (hk : 1 ≤ k) : ∑ t ∈ nbAll k with t.snd.fst = u ∧ t.snd.snd.penultimate ≠ v, nbWeight t.snd = ∑ w ∈ G.neighborFinset u \ {v}, nbLastWeight k w u

Refolding the prefix mass into last-edge marginals. The prefix sum (length-k walks ending at u, penultimate avoiding v) is the sum over admissible previous vertices w ∈ N(u) \ {v} of the last-edge marginals nbLastWeight k w u. A fiberwise partition on the penultimate.

theorem ACMax.nbLastWeight_succ_eq {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {u v : V} (huv : G.Adj u v) {k : ℕ} (hk : 1 ≤ k) : nbLastWeight (k + 1) u v = (∑ w ∈ G.neighborFinset u \ {v}, nbLastWeight k w u) * (↑(G.degree u) - 1)⁻¹

The exact one-step recursion (the engine of W3). For k ≥ 1 and G.Adj u v, the last-edge marginal at step k+1 is the sum of the previous-step last-edge marginals over the admissible predecessors w ∈ N(u) \ {v}, scaled by (deg u − 1)⁻¹ — the concat step redistributes each prefix's mass equally to its deg u − 1 extensions.

W3 — the last-edge marginal xP = x

theorem ACMax.nbLastWeight_eq_one {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (hδ2 : ∀ (w : V), 2 ≤ G.degree w) {k : ℕ} (hk : 1 ≤ k) {u v : V} : G.Adj u v → nbLastWeight k u v = 1

W3 (AHL's xP = x). Under δ ≥ 2, for every k ≥ 1 and every directed edge (u, v) the total weight of the length-k non-backtracking walks whose last directed edge is (u, v) is exactly 1. The weighted last-edge marginal is stationary. Proof by induction on k: the base case is the single edge u → v (weight 1); the step uses nbLastWeight_succ_eq, the induction hypothesis over the deg u − 1 predecessors, and mul_inv_cancel₀ with deg u − 1 ≠ 0.

W4 — the end marginal

theorem ACMax.nbEndWeight_eq_sum_lastWeight {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {v : V} {k : ℕ} (hk : 1 ≤ k) : nbEndWeight k v = ∑ u ∈ G.neighborFinset v, nbLastWeight k u v

The end marginal is the sum of the last-edge marginals over the neighbours. A fiberwise partition of the length-k walks ending at v by their penultimate vertex (which is always a neighbour of v).

theorem ACMax.nbEndWeight_eq_degree {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (hδ2 : ∀ (w : V), 2 ≤ G.degree w) {v : V} {k : ℕ} (hk : 1 ≤ k) : nbEndWeight k v = ↑(G.degree v)

W4. Under δ ≥ 2, for k ≥ 1 the total weight of the length-k non-backtracking walks ending at v is exactly deg v — the exact degree-bias (unlike the raw end-count, which obeys no usable law). Each summand of the neighbour partition is 1 by W3, so the sum is |N(v)| = deg v.

W5 — the total weight

theorem ACMax.nbWeightTotal_eq {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] (hδ2 : ∀ (w : V), 2 ≤ G.degree w) {k : ℕ} (hk : 1 ≤ k) : nbWeightTotal k = ∑ v : V, ↑(G.degree v)

W5. Under δ ≥ 2, for k ≥ 1 the total weight of all length-k non-backtracking walks is exactly D = ∑ v, deg v — the constant the weighted AM–GM (W7) normalizes against (its exponent collapse). Sum the end marginals (W4) over all endpoints.