Balanced-prefix transport of the retained advice law

On valid widths the total prefix map takes uniform Boolean words to uniform Boolean words. Existing balanced-state transport first contracts the honest-output discrepancy; forgetting the unused tampered coordinates then contracts the retained side information. Neither contraction requires nonnegative or normalized input weights.

theorem Algebraic.Cutwidth.Extractor.Internal.adviceOutputPrefix_eq_of_le {out d : ℕ} (size : out ≤ d) (bits : Fin d → Bool) : adviceOutputPrefix out bits = fun (i : Fin out) => bits (Fin.castLE size i)

theorem Algebraic.Cutwidth.Extractor.Internal.adviceOutputPrefix_self {d : ℕ} (bits : Fin d → Bool) : adviceOutputPrefix d bits = bits

theorem Algebraic.Cutwidth.Extractor.Internal.adviceOutputPrefix_apply_of_ge {out d : ℕ} (bits : Fin d → Bool) (i : Fin out) (outside : d ≤ ↑i) : adviceOutputPrefix out bits i = false

theorem Algebraic.Cutwidth.Extractor.Internal.adviceOutputPrefix_uniform {out d : ℕ} (size : out ≤ d) : mapWeight (adviceOutputPrefix out) (uniformWeight (Fin d → Bool)) = uniformWeight (Fin out → Bool)

theorem Algebraic.Cutwidth.Extractor.Internal.adviceTruncatedCorrelationBreakerWeight_eq_map (n m L e out : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (advice advice' : List Bool) : adviceTruncatedCorrelationBreakerWeight n m L e out w l r x x' y y' advice advice' = mapWeight (fun (p : ((Z × B) × (Fin (matchedBlockSeedBits L) → Bool)) × (Fin (matchedBlockSeedBits L) → Bool)) => ((p.1.1, adviceOutputPrefix out p.1.2), adviceOutputPrefix out p.2)) (adviceCorrelationBreakerWeight n m L e w l r x x' y y' advice advice')

theorem Algebraic.Cutwidth.Extractor.Internal.adviceTruncatedCorrelationBreakerWeight_probability (n m L e out : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (advice advice' : List Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (adviceTruncatedCorrelationBreakerWeight n m L e out w l r x x' y y' advice advice')

theorem Algebraic.Cutwidth.Extractor.Internal.adviceTruncatedCorrelationBreakerWeight_dist_le (n m L e out : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (advice advice' : List Bool) (size : out ≤ matchedBlockSeedBits L) : weightDist (adviceTruncatedCorrelationBreakerWeight n m L e out w l r x x' y y' advice advice') (uniformSecondWeight (adviceTruncatedCorrelationBreakerWeight n m L e out w l r x x' y y' advice advice')) ≤ weightDist (adviceCorrelationBreakerWeight n m L e w l r x x' y y' advice advice') (uniformSecondWeight (adviceCorrelationBreakerWeight n m L e w l r x x' y y' advice advice'))