Killed walks #
Walks whose length is random, killed before each step with probability 1 / q and stopped after T
steps, are Radhakrishnan's variant [Rad06] of the walks in the powering step of Dinur's
proof of the PCP theorem Dinur, Section 9. A killed walk on a D-regular multigraph
G is presented by T labels of G and T kill signals c : Fin T → Fin q: it follows the
labels until its kill time killTime c, the first step i with c i = 0 (or T if there is
none), and the remaining labels carry no meaning. Under uniformly random signals the kill time has
the geometric law truncated at T: it is m < T with probability (1 - 1 / q) ^ m / q
(card_filter_killTime_eq) and at least m ≤ T with probability (1 - 1 / q) ^ m
(card_filter_le_killTime).
Given that it is killed at step ℓ < T, a uniformly random killed walk is a uniformly random walk
of length ℓ (sum_ite_killTime_eq, card_filter_killTime_eq_and). Splitting it at a step
i < ℓ with splitWalk counts the killed walks crossing a given dart at step i by independent
factors for the i steps before it and the j = ℓ - (i + 1) steps after it, times the weight
|D| ^ (T - ℓ) (q - 1) ^ ℓ q ^ (T - (ℓ + 1)) of the length ℓ
(card_filter_killTime_eq_and_splitWalk). The factor
(q - 1) ^ ℓ = (q - 1) ^ i (q - 1) (q - 1) ^ j of that weight splits between the two sides of the
crossed edge: up to the truncation at T, the lengths i and j of the two sides are
independent, which is what the first-moment count of the powering step uses.
The killed walks are the darts of the killed power G.killedPow T q, whose edge labelled (k, c)
at v is the killed walk from v (neighbor_killedPow). Its rotation map reverses a killed walk
up to its kill time (rot_pow_killTime) and leaves its unused labels and its signals alone, so
that the reverse is killed at the same step.
Main definitions #
Cslib.RotationMap.killTime: the step at which a walk with given kill signals is killed.Cslib.RotationMap.killedPow: the killed power of a rotation map.
Main results #
Cslib.RotationMap.killTime_cons: a walk survives its first step unless its first signal is0, and is then killed one step after the walk along its remaining signals.Cslib.RotationMap.card_filter_killTime_eq,Cslib.RotationMap.card_filter_le_killTime: the truncated geometric law of the kill time.Cslib.RotationMap.sum_ite_killTime_eq,Cslib.RotationMap.card_filter_killTime_eq_and: given its kill time, a killed walk is a uniformly random walk of that length.Cslib.RotationMap.expect_killTime_eq,Cslib.RotationMap.expect_le_killTime,Cslib.RotationMap.expect_ite_killTime_eq,Cslib.RotationMap.expect_prod_ite_killTime_eq: the law of killed walks, as uniform averages.Cslib.RotationMap.card_filter_killTime_eq_and_splitWalk: the crossing count for killed walks.Cslib.RotationMap.neighbor_killedPow,Cslib.RotationMap.rot_pow_killTime: the edges of the killed power and their reverses.
References #
Under uniformly random signals, a walk of length T is killed at its step m < T with
probability (1 - 1 / q) ^ m / q: the signals that kill it there number
(q - 1) ^ m * q ^ (T - (m + 1)).
Under uniformly random signals, a walk of length T survives its first m ≤ T steps with
probability (1 - 1 / q) ^ m: the signals that let it number (q - 1) ^ m * q ^ (T - m).
The law of a killed walk. Given that it is killed at its step ℓ < T, a uniformly random
walk of length T with uniformly random kill signals is, up to that step, a uniformly random walk
of length ℓ: summing a function of its first ℓ steps over the walks and signals killed at step
ℓ sums it |D| ^ (T - ℓ) (q - 1) ^ ℓ q ^ (T - (ℓ + 1)) times over the walks of length ℓ.
The law of a killed walk, counting form: the walks of length T and kill signals for which
the walk is killed at its step ℓ < T and its first ℓ steps satisfy P number
#{w | P w} |D| ^ (T - ℓ) (q - 1) ^ ℓ q ^ (T - (ℓ + 1)).
The crossing count for killed walks. Counted by the dart d crossed at step i, the walks
of length T and kill signals for which the walk is killed at its step ℓ < T, crosses d at its
step i < ℓ, the reverse of its first i steps satisfies P d and its steps from i + 1 to ℓ
satisfy Q d are counted by independent factors and the weight of the length ℓ.
The law of killed walks, as averages #
Under uniformly random kill signals, a walk of length T survives its first m ≤ T steps with
probability (1 - 1 / q) ^ m.
Under uniformly random kill signals, a walk of length T is killed at its step m < T with
probability (1 - 1 / q) ^ m / q: it survives its first m steps but not its first m + 1.
The law of a killed walk: averaged over uniformly random labels and kill signals, a function
of the first ℓ < T labels, on the event that the walk is killed at step ℓ, averages to
(1 - 1 / q) ^ ℓ / q times its average over the label sequences of length ℓ.
The law of a killed walk, with a uniformly random start: a function of the walk along the
first ℓ < T labels, on the event that the walk is killed at step ℓ, averages to
(1 - 1 / q) ^ ℓ / q times its average over the walks of length ℓ.
The killed power G.killedPow T q: the multigraph on the vertices of G with
an edge for every walk in G of length T with kill signals in Fin q. The edge labelled (k, c)
at v is the walk from v along the labels k, stopped when it is killed at step killTime c;
its rotation map reverses the walk up to that step and leaves the unused labels and the signals
alone, so that the reverse is killed at the same step. A step of its random walk is a random walk
on G killed after each step with probability 1 / q, and stopped after T steps.
Instances For
The edge labelled (k, c) at v in the killed power leads to the vertex where the walk from
v along k is killed.