Explicit sampler-index equivalences preserve sampling #
Changing the enumeration of outer seeds and candidate positions preserves the source threshold, test density, and failure probability. The actual reduction uses this transport with fixed-width binary encodings.
theorem
Algebraic.Cutwidth.Extractor.SomewhereSampler.reindex
{α : Type u_1}
{Outer : Type u_2}
{Outer' : Type u_3}
{Candidate : Type u_4}
{Candidate' : Type u_5}
{Ω : Type u_6}
[Fintype α]
[Fintype Outer]
[Fintype Outer']
[Fintype Ω]
{S : α → Outer → Candidate → Ω}
{L ε δ : ℝ}
(sample : SomewhereSampler S L ε δ)
(outer : Outer' ≃ Outer)
(candidate : Candidate' ≃ Candidate)
:
SomewhereSampler (fun (x : α) (y : Outer') (z : Candidate') => S x (outer y) (candidate z)) L ε δ
Bijections of both index types preserve the full somewhere-sampler guarantee.