One uniform program for the selected finite advice construction

The evaluator computes the chosen scale, local error exponent, and right width from the original source/advice lengths and unary target/output parameters. It normalizes the right word to that width and executes the actual advice chain and final output prefix. Canonical inputs agree exactly with adviceTruncatedCorrelationBreaker at the same selected parameters as the checked statistical theorem. This equality needs no entropy premise.

All chooser values have uniform unary certificates. Complete loop bounds include both source words, the generated parameters, remaining advice, and current state. The polynomial-time certificate holds on every encoded input, including malformed pairs and infeasible statistical parameters. Only fixed powers of two appear in parameter generation. No search or unbounded-iteration closure is used.

theorem Algebraic.Cutwidth.Extractor.adviceErrorExponent_unaryFn {a target : List Bool → ℕ} (ha : Complexity.UnaryFn a) (htarget : Complexity.UnaryFn target) : Complexity.UnaryFn fun (z : List Bool) => adviceErrorExponent (a z) (target z)

Generate the local error exponent uniformly from unary advice length and target.

theorem Algebraic.Cutwidth.Extractor.adviceScale_unaryFn {n a target out : List Bool → ℕ} (hn : Complexity.UnaryFn n) (ha : Complexity.UnaryFn a) (htarget : Complexity.UnaryFn target) (hout : Complexity.UnaryFn out) : Complexity.UnaryFn fun (z : List Bool) => adviceScale (n z) (a z) (target z) (out z)

Generate the common scale uniformly from all four unary chooser inputs.

theorem Algebraic.Cutwidth.Extractor.adviceSourceEntropy_unaryFn {n a target out : List Bool → ℕ} (hn : Complexity.UnaryFn n) (ha : Complexity.UnaryFn a) (htarget : Complexity.UnaryFn target) (hout : Complexity.UnaryFn out) : Complexity.UnaryFn fun (z : List Bool) => adviceSourceEntropy (n z) (a z) (target z) (out z)

The source reserve and normalized right width are uniformly unary-computable.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedRightWord_length (m : ℕ) (y : List Bool) : (adviceSelectedRightWord m y).length = m

The normalized right input always has exactly its selected width.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedRightWord_eq (m : ℕ) (y : List Bool) (length : y.length = m) : adviceSelectedRightWord m y = y

Normalization leaves every canonical right input unchanged.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedRightWord_mem_FP {m : List Bool → ℕ} {y : List Bool → List Bool} (hm : Complexity.UnaryFn m) (hy : y ∈ Complexity.FP) : (fun (z : List Bool) => adviceSelectedRightWord (m z) (y z)) ∈ Complexity.FP

Prefix normalization with false completion has a uniform polynomial-time certificate.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerRuntime_zero (target : ℕ) (x y advice : List Bool) : adviceSelectedCorrelationBreakerRuntime target 0 x y advice = []

A request for zero output bits returns immediately for every input.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerRuntime_length (target out : ℕ) (x y advice : List Bool) : (adviceSelectedCorrelationBreakerRuntime target out x y advice).length = out

The total runtime produces exactly the requested output width on arbitrary words.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerRuntime_eq (n target out : ℕ) (advice : List Bool) (x : Fin n → Bool) (y : Fin (adviceSourceEntropy n advice.length target out) → Bool) : adviceSelectedCorrelationBreakerRuntime target out (List.ofFn x) (List.ofFn y) advice = List.ofFn (adviceTruncatedCorrelationBreaker n (adviceSourceEntropy n advice.length target out) (adviceScale n advice.length target out) (adviceErrorExponent advice.length target) out x y advice)

Canonical source words compute exactly the actual selected truncated program.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerRun_length_le (target out : ℕ) (x y advice : List Bool) (i : ℕ) : have n := x.length; have a := advice.length; have L := adviceScale n a target out; have e := adviceErrorExponent a target; have m := adviceSourceEntropy n a target out; (encodeAdviceRunState (adviceRun L e x (adviceSelectedRightWord m y) advice i)).length ≤ 4 * n + 2 * m + 2 * L + 2 * e + 2 * a + matchedBlockOutputBits 64 L + 12

Every complete loop encoding is bounded, including the generated right-source padding.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerRuntime_mem_FP {target out : List Bool → ℕ} {x y advice : List Bool → List Bool} (htarget : Complexity.UnaryFn target) (hout : Complexity.UnaryFn out) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) (hadvice : advice ∈ Complexity.FP) : (fun (z : List Bool) => adviceSelectedCorrelationBreakerRuntime (target z) (out z) (x z) (y z) (advice z)) ∈ Complexity.FP

The whole selected program is uniform in its numerical inputs and all original words.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerEval_pair (x y advice targetWord outWord : List Bool) : adviceSelectedCorrelationBreakerEval (Complexity.pair (Complexity.pair x y) (Complexity.pair advice (Complexity.pair targetWord outWord))) = adviceSelectedCorrelationBreakerRuntime targetWord.length outWord.length x y advice

The codec retains both sources and advice, followed by unary target/output words.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerEval_eq (n target out : ℕ) (advice : List Bool) (x : Fin n → Bool) (y : Fin (adviceSourceEntropy n advice.length target out) → Bool) : adviceSelectedCorrelationBreakerEval (Complexity.pair (Complexity.pair (List.ofFn x) (List.ofFn y)) (Complexity.pair advice (Complexity.pair (List.replicate target true) (List.replicate out true)))) = List.ofFn (adviceTruncatedCorrelationBreaker n (adviceSourceEntropy n advice.length target out) (adviceScale n advice.length target out) (adviceErrorExponent advice.length target) out x y advice)

The single paired evaluator exactly serializes the selected statistical construction.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerEval_length (z : List Bool) : (adviceSelectedCorrelationBreakerEval z).length = (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd z))).length

Every evaluator output has the length of the decoded output request.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerEval_length_le (z : List Bool) : (adviceSelectedCorrelationBreakerEval z).length ≤ z.length

Even malformed encoded inputs produce an output no longer than their input.

theorem Algebraic.Cutwidth.Extractor.adviceSelectedCorrelationBreakerEval_mem_FP : adviceSelectedCorrelationBreakerEval ∈ Complexity.FP

One total string function evaluates all selected parameters in polynomial time.