The actual advice program at selected finite parameters

The total chooser fixes the right-source length and left-source entropy reserve m, common scale L, and local error exponent e. For unequal advice strings of the same chosen length, the actual program returns the requested out bits with error at most 2^(-target), retaining the entire original right state and the actual truncated tampered output.

Inputs are independent conditional on the shared tag. The honest right input is uniform on every row; the honest left input has the stated average joint point-mass envelope. These original-source hypotheses govern whether the entropy reserve is feasible; the chooser does not assert that it fits every left-input width. No program guard, primitive extractor certificate, intermediate security witness, or field instance is supplied by the caller.

The construction follows Chattopadhyay--Goyal--Li Algorithm 2, https://arxiv.org/abs/1505.00107, with an additional final extraction from the original left source. The explicit constants and conservative finite error accounting are checked deductions of this library. A uniform evaluator for these selected parameters is a separate runtime layer.

theorem Algebraic.Cutwidth.Extractor.adviceTruncatedCorrelationBreaker_parameters_dist_le (n a target out : ℕ) {Z A B : Type u} [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 (adviceSourceEntropy n a target out) → Bool) (advice advice' : List Bool) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (uniform : ∀ (z : Z), mapWeight (y z) (r z) = uniformWeight (Fin (adviceSourceEntropy n a target out) → Bool)) (length : advice.length = a) (length' : advice'.length = a) (different : advice ≠ advice') (left : ∑ z : Z, μ z ≤ (2 ^ adviceSourceEntropy n a target out)⁻¹) : let m := adviceSourceEntropy n a target out; have L := adviceScale n a target out; have e := adviceErrorExponent a target; have actual := adviceTruncatedCorrelationBreakerWeight n m L e out w l r x x' y y' advice advice'; weightDist actual (uniformSecondWeight actual) ≤ (2 ^ target)⁻¹

The explicit finite chooser gives the requested actual output width and dyadic error.