Requested output widths for the actual advice correlation breaker

Truncate both actual outputs while retaining the original shared tag and entire right state. For any requested width within the program's output, the discrepancy from a fresh uniform honest output can only decrease. This is a comparison of the two actual laws, with no supplied security invariant or normalization assumption. A full extraction theorem can therefore reuse its error estimate at any shorter requested output width.

The map is total outside that range, completing excess positions by false; the statistical contraction is asserted only when no completion is used. The proof is elementary finite total-variation data processing and the uniformity of a Boolean prefix.

theorem Algebraic.Cutwidth.Extractor.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)

Within the input width the total map is the ordinary Boolean coordinate prefix.

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

Requesting the complete width leaves every output coordinate unchanged.

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

The total map completes every coordinate beyond the input width by false.

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

A prefix of a uniform Boolean word is uniform at every valid requested width.

theorem Algebraic.Cutwidth.Extractor.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')

The truncated law is the simultaneous output prefix of the two actual program outputs.

theorem Algebraic.Cutwidth.Extractor.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')

The actual truncated retained law is normalized on normalized source factors.

theorem Algebraic.Cutwidth.Extractor.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'))

Truncating both actual outputs preserves any bound on the original retained-law discrepancy.