Splitting a walk at a step

The surgery behind the crossing decomposition: a walk of length ℓ and a position i < ℓ split it into a prefix of length i, the label crossed at i, and a suffix of length ℓ - (i+1); gluing puts them back.

Dinur's first-moment count is organised around this. Conditioned on a killed walk crossing a given dart at step i, what remains is exactly a free prefix and a free suffix — and because the killed law makes their lengths independent too, the count factorises into two copies of the plurality bound.

Main definitions

• RegGraph.segPre, RegGraph.segSuf — the two pieces of a split walk
• RegGraph.segGlue — gluing them back with a crossing label

Main results

• RegGraph.segPre_segGlue, RegGraph.segMid_segGlue, RegGraph.segSuf_segGlue — gluing then splitting is the identity
• RegGraph.segGlue_split — splitting then gluing is the identity
• RegGraph.walkAt_segSuf, RegGraph.revWalk_segSuf — the suffix walk tracks the original, and reversing it gives the reversed walk's prefix
• RegGraph.card_crossing_eq — the walks crossing a dart at a step, counted as independent prefix and suffix factors
• RegGraph.card_label_fibre — labels grouped by their effective walk
• RegGraph.card_label_crossing — the two combined: crossing labels counted as prefix times suffix times fibre weight
• RegGraph.walkAt_preWalk — a killed walk's crossings are the underlying fixed-length walk's crossings

def Complexity.RegGraph.segPre (G : RegGraph) {ℓ : ℕ} (W : Fin ℓ → G.D) {i : ℕ} (hi : i ≤ ℓ) : Fin i → G.D

The first i steps of a walk.

Equations

• G.segPre W hi = G.preWalk W hi

def Complexity.RegGraph.segSuf (G : RegGraph) {ℓ : ℕ} (W : Fin ℓ → G.D) (i : ℕ) : Fin (ℓ - (i + 1)) → G.D

The steps of a walk after position i.

Equations

• G.segSuf W i k = W ⟨i + 1 + ↑k, ⋯⟩

def Complexity.RegGraph.segGlue (G : RegGraph) {ℓ i : ℕ} (p : Fin i → G.D) (d : G.D) (s : Fin (ℓ - (i + 1)) → G.D) : Fin ℓ → G.D

Glue a prefix, a crossing label and a suffix into one walk.

Equations

• G.segGlue p d s k = if hk : ↑k < i then p ⟨↑k, hk⟩ else if hk2 : ↑k = i then d else s ⟨↑k - (i + 1), ⋯⟩

@[simp]

theorem Complexity.RegGraph.segPre_segGlue (G : RegGraph) {ℓ i : ℕ} (hi : i ≤ ℓ) (p : Fin i → G.D) (d : G.D) (s : Fin (ℓ - (i + 1)) → G.D) : G.segPre (G.segGlue p d s) hi = p

@[simp]

theorem Complexity.RegGraph.segMid_segGlue (G : RegGraph) {ℓ i : ℕ} (hi : i < ℓ) (p : Fin i → G.D) (d : G.D) (s : Fin (ℓ - (i + 1)) → G.D) : G.segGlue p d s ⟨i, hi⟩ = d

@[simp]

theorem Complexity.RegGraph.segSuf_segGlue (G : RegGraph) {ℓ i : ℕ} (p : Fin i → G.D) (d : G.D) (s : Fin (ℓ - (i + 1)) → G.D) : G.segSuf (G.segGlue p d s) i = s

theorem Complexity.RegGraph.segGlue_split (G : RegGraph) {ℓ i : ℕ} (hi : i < ℓ) (W : Fin ℓ → G.D) : G.segGlue (G.segPre W ⋯) (W ⟨i, hi⟩) (G.segSuf W i) = W

Splitting a walk and gluing it back returns the walk.

theorem Complexity.RegGraph.walkAt_segSuf (G : RegGraph) {ℓ : ℕ} (v : G.V) (W : Fin ℓ → G.D) (i m : ℕ) : m ≤ ℓ - (i + 1) → G.walkAt (ℓ - (i + 1)) (G.walkAt ℓ v W (i + 1)) (G.segSuf W i) m = G.walkAt ℓ v W (i + 1 + m)

The suffix walk, started at the vertex the original walk reaches at step i + 1, tracks the original walk.

theorem Complexity.RegGraph.revWalk_segSuf (G : RegGraph) {ℓ : ℕ} (v : G.V) (W : Fin ℓ → G.D) {i : ℕ} (hi : i < ℓ) : G.revWalk (G.walkAt ℓ v W (i + 1)) (G.segSuf W i) = G.segPre (G.revWalk v W) ⋯

Reversal commutes with splitting. Reversing the suffix of a walk gives the prefix of the reversed walk: both are the walk that runs from the far end back to the crossing point. This is what makes the suffix condition in the powered constraint the same as a condition on walks out of the dart's head.

The crossing bijection

theorem Complexity.RegGraph.card_crossing_eq (G : RegGraph) {ℓ i : ℕ} (hi : i < ℓ) (a : G.V) (d : G.D) (Pre : (Fin i → G.D) → Prop) [DecidablePred Pre] (Suf : (Fin (ℓ - (i + 1)) → G.D) → Prop) [DecidablePred Suf] : {x : G.V × (Fin ℓ → G.D) | G.walkAt ℓ x.1 x.2 i = a ∧ x.2 ⟨i, hi⟩ = d ∧ Pre (G.revWalk x.1 (G.segPre x.2 ⋯)) ∧ Suf (G.segSuf x.2 i)}.card = (Finset.filter Pre Finset.univ).card * (Finset.filter Suf Finset.univ).card

The crossing decomposition. The walks of length ℓ that cross a given dart (a, d) at step i are in bijection with pairs of a walk out of a of length i — the reversed prefix — and a walk of length ℓ - (i+1) — the suffix. Any conditions imposed on the two pieces therefore contribute independent factors, which is what makes the first moment factorise.

From labels to walks

theorem Complexity.RegGraph.card_label_fibre (G : RegGraph) {T q ℓ : ℕ} (hq : 0 < q) (hℓ : ℓ < T) (P : G.V × (Fin ℓ → G.D) → Prop) [DecidablePred P] : {z : G.V × (Fin T → G.D) × (Fin T → Fin q) | stopAt z.2.2 = ℓ ∧ P (z.1, G.preWalk z.2.1 ⋯)}.card = (Finset.filter P Finset.univ).card * (G.deg ^ (T - ℓ) * ((q - 1) ^ ℓ * q ^ (T - ℓ - 1)))

Labels grouped by their effective walk. Any condition on the starting vertex and the effective walk is counted by counting walks, each weighted by the number of labels carrying it. This is the step that turns a statement about killed-walk labels into one about walks, where the crossing decomposition applies.

theorem Complexity.RegGraph.card_label_crossing (G : RegGraph) {T q ℓ i : ℕ} (hq : 0 < q) (hℓ : ℓ < T) (hi : i < ℓ) (a : G.V) (d : G.D) (Pre : (Fin i → G.D) → Prop) [DecidablePred Pre] (Suf : (Fin (ℓ - (i + 1)) → G.D) → Prop) [DecidablePred Suf] : {z : G.V × (Fin T → G.D) × (Fin T → Fin q) | stopAt z.2.2 = ℓ ∧ G.walkAt ℓ z.1 (G.preWalk z.2.1 ⋯) i = a ∧ G.preWalk z.2.1 ⋯ ⟨i, hi⟩ = d ∧ Pre (G.revWalk z.1 (G.segPre (G.preWalk z.2.1 ⋯) ⋯)) ∧ Suf (G.segSuf (G.preWalk z.2.1 ⋯) i)}.card = (Finset.filter Pre Finset.univ).card * (Finset.filter Suf Finset.univ).card * (G.deg ^ (T - ℓ) * ((q - 1) ^ ℓ * q ^ (T - ℓ - 1)))

The crossing count, at the level of labels. Chaining the two previous lemmas: the killed-walk labels of effective length ℓ whose walk crosses the dart (a, d) at step i, subject to any conditions on the reversed prefix and on the suffix, number

(prefix count) * (suffix count) * (fibre weight).

The two conditions never interact — that is the independence the killed law buys, and the reason the first moment factorises into two plurality bounds.

theorem Complexity.RegGraph.walkAt_preWalk (G : RegGraph) {T ℓ : ℕ} (h : ℓ ≤ T) (x : G.V) (s : Fin T → G.D) (k : ℕ) : k ≤ ℓ → G.walkAt ℓ x (G.preWalk s h) k = G.walkAt T x s k

A walk following a prefix of a label sequence agrees with the full walk for as long as the prefix lasts. This identifies the crossings of a killed walk with those of the underlying fixed-length walk, which is what lets the correlation bound — stated for fixed length — apply to them.