lemmaroutinestructure_uncertain
Walk variants avoid storing endpoints
Walk words expand to -bit variants that sum exactly to the conditional walk
endpoint-free walk generation for paths and clean blocks
Lemma·
lem:env-variants·§6.1 Generating paths without retaining their endpointsStatement (paper)
A length- word in the walk of Lemma can be expanded
into a bounded-alphabet family of variants described by bits
such that:
\begin{enumerate}
\item each fixed variant acts bijectively and measure-preservingly on
the full environment before any endpoint tests;
\item its transformation is independent of the indicated identifiers;
\item for each walk word and each environment in the required
conditional slice, exactly one variant passes the slice and wrap
tests at the indicated identifiers, and this variant gives the
conditional walk transformation;
\item the sum of valid variants, each with the probability of its
original walk word, is exactly the conditional average.
\end{enumerate}
The tests can be performed when their indicated vertices are visited.
In the admissible implementation range, field elements and identifiers
have bits, the total auxiliary bit string has bits, and .
In that range the transformations and tests use shared scratch space, and
the retained description of a variant uses bits.
In plain English
A length- walk word can be expanded into a bounded-alphabet family of variants, each describable in bits, where each variant is a bijective, measure-preserving map on the environment that does not depend on the indicated identifiers. For each word and environment in the conditional slice exactly one variant passes the slice and wrap tests and yields the conditional walk transformation, so summing valid variants with their original word probabilities gives the conditional average exactly.
Why it's here
This lets the walk be generated and averaged without retaining path endpoints: endpoint conditions become tests applied at visited vertices, and a guessed variant replaces the stored endpoint. Within the stated range (-bit elements and identifiers, ) this keeps scratch space at and variant descriptions at bits, which is what later path-generation and charging arguments rely on. Realizing the transformations and tests uses the estimator-interface realization theorem.
Classified routine:
A technical step in the paper's own walk construction: it applies the standard trick of replacing stored endpoints with guessed variants that are verified on the fly, and handles the space bookkeeping with the paper's controller-realization theorem (thm-ctrl-realization) and the walk of Lemma lem:env-gap.
Uses
Used by
Sources
PaperOpen
- Section
- §6.1 Generating paths without retaining their endpoints
- Page
- —
- Label
lem:env-variants- Line
sections/averaging.tex:180
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infostructure_uncertainProof forward-references thm:ctrl-realization for space accounting of nested restoration; this is a forward pointer, not a logical dependency.