Killed walks #
The walk law Dinur's powering step actually needs: at every step the walk stops
with probability 1 / q, so its length is geometric rather than fixed.
A dart label is a pair of sequences: T edge labels and T stop signals. The
walk follows the edge labels until the first signal equal to 0 — the
stopping index — and its endpoint is where it stopped. Uniform labels
therefore realise a geometric length exactly, truncated at T, with the labels
past the stopping index carrying multiplicity but no meaning.
Why geometric and not fixed length #
Soundness decodes an assignment of the powered system by plurality and needs the
opinions at the two ends of a checked step to be truthful. Summed over the
checked steps that amounts to ∑ a_i · b_j over the prefix length i and the
suffix length j. With walks of fixed length those are tied by i + j = t - 1
and the sum can vanish — the two ends can be truthful at complementary lengths
and never at the same step, so nothing is charged. Killing makes
i and j independent, so the sum factorises into a product of two
plurality bounds. That factorisation is the whole reason for this construction.
Reversal #
Reversing a killed walk reverses only its effective prefix and leaves both the tail and the stop signals alone. Since the signals are untouched, the reversed walk stops at the same index, which is what makes reversal an involution — the requirement for the powered graph to be an undirected regular graph at all.
Main definitions #
stopAt— the stopping index of a signal sequenceRegGraph.preWalk,RegGraph.extWalk— the effective prefix, and overwriting itRegGraph.killedEnd,RegGraph.killedRev— the endpoint and the reversalRegGraph.killedPower— the resulting regular graph
Main results #
signal_ne_zero_of_lt,signal_eq_zero_of_stopAt_lt,stopAt_eq_of— what the stopping index meanslt_stopAt_iff— reaching stepidepends only on the firsti + 1signalscard_lt_stopAt,card_le_stopAt,card_stopAt_eq— how many signal sequences run for a given number of stepsRegGraph.card_preWalk_eq,RegGraph.card_killed_fibre— the weight an effective walk carriesRegGraph.killedEnd_killedRev,RegGraph.killedRev_killedRev— reversal undoes itselfRegGraph.deg_killedPower— the degree isdeg ^ T * q ^ T
The step at which a killed walk stops: the first index carrying the signal
0, or T if there is none.
Equations
- Complexity.stopAt c = List.findIdx (fun (i : Fin T) => ↑(c i) == 0) (List.finRange T)
Instances For
The walk is still running at step i exactly when the first i + 1
signals are all nonzero. This is the form the crossing decomposition needs: the
event "the walk reaches step i" depends only on the first i + 1 signal
coordinates, so it splits off as a factor.
The signal count. The walks still running at step i are exactly those
whose first i + 1 signals are all nonzero, and those coordinates are free of
one another, so they number (q-1) ^ (i+1) * q ^ (T-i-1). This is the factor
that the crossing decomposition peels off.
The exact-length signal count. The walks of effective length exactly m
number (q-1) ^ m * q ^ (T-m-1): the first m signals are nonzero, the m-th
is zero, and the rest are free.
Prefixes #
The fibre count. The killed-walk labels whose effective walk is exactly
a prescribed length-m walk number deg ^ (T-m) * (q-1) ^ m * q ^ (T-m-1): the
two conditions constrain the edge labels and the signals separately, so the
counts multiply. This is the weight each effective walk carries, and it is
geometric in m — the law both the plurality and the conditional prefix and
suffix follow.