One uniform polynomial-time program for the complete affine construction

The selected program computes every parameter from the original input lengths, a unary tampering count, and a unary target exponent. Canonical inputs compute the actual first phase followed by all subset-doubling rounds on the same original source words. The polynomial-time guarantee covers every input, including malformed words and infeasible entropy requests. Source and advice conditions belong to the statistical theorem.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerRuntime_eq (n d t L₀ e₀ L₁ e₁ er rounds : ℕ) (first : MatchedBlockRuntimeValid n 64 L₀ e₀) (adviceGuard : FlipFlopSizeGuard d (matchedBlockOutputBits 64 L₀) L₁ e₁) (right : MatchedBlockRuntimeValid d 24 L₁ er) (rowGuard : MatchedBlockRuntimeValid (matchedBlockOutputBits (growingMatchedBlockDepth t) L₁) 24 L₁ er) (last : GrowingMatchedBlockRuntimeValid n t L₁ er) (x : Fin n → Bool) (y : Fin d → Bool) (advice : List Bool) : affineCorrelationBreakerRuntime t L₀ e₀ L₁ e₁ er rounds (List.ofFn x) (List.ofFn y) advice = List.ofFn (affineCorrelationBreaker n d (growingMatchedBlockDepth t) L₀ e₀ L₁ e₁ er rounds x y advice)

The actual first phase and every subsequent runtime round match the semantic construction.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerRuntime_length (t L₀ e₀ L₁ e₁ er rounds : ℕ) (x y advice : List Bool) : (affineCorrelationBreakerRuntime t L₀ e₀ L₁ e₁ er rounds x y advice).length = if GrowingMatchedBlockRuntimeValid x.length t L₁ er then 2 ^ growingMatchedBlockDepth t * L₁ else 0

Every round has the same output width, including the zero-round initial phase.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerRuntime_length_le (t L₀ e₀ L₁ e₁ er rounds : ℕ) (x y advice : List Bool) : (affineCorrelationBreakerRuntime t L₀ e₀ L₁ e₁ er rounds x y advice).length ≤ 2 ^ 65 * (t + 1) * L₁

The complete runtime output is polynomially bounded even on invalid parameters.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerRuntime_mem_FP {t L₀ e₀ L₁ e₁ er rounds : List Bool → ℕ} {x y advice : List Bool → List Bool} (ht : Complexity.UnaryFn t) (hL₀ : Complexity.UnaryFn L₀) (he₀ : Complexity.UnaryFn e₀) (hL₁ : Complexity.UnaryFn L₁) (he₁ : Complexity.UnaryFn e₁) (her : Complexity.UnaryFn er) (hrounds : Complexity.UnaryFn rounds) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) (hadvice : advice ∈ Complexity.FP) : (fun (z : List Bool) => affineCorrelationBreakerRuntime (t z) (L₀ z) (e₀ z) (L₁ z) (e₁ z) (er z) (rounds z) (x z) (y z) (advice z)) ∈ Complexity.FP

Actual initialization and a unary number of rounds form one uniform polynomial-time program.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerSelectedRuntime_length (t target : ℕ) (x y advice : List Bool) : (affineCorrelationBreakerSelectedRuntime t target x y advice).length = 2 ^ growingMatchedBlockDepth t * affinePhaseOneScale x.length t advice.length (affineIterationTarget t target)

Every selected output has the prescribed growing-depth width.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerSelectedRuntime_length_le (t target : ℕ) (x y advice : List Bool) : (affineCorrelationBreakerSelectedRuntime t target x y advice).length ≤ 2 ^ 65 * (t + 1) * affinePhaseOneScale x.length t advice.length (affineIterationTarget t target)

The selected width has a polynomial bound in the chooser inputs.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerSelectedRuntime_eq (n t target : ℕ) (advice : List Bool) (x : Fin n → Bool) (y : Fin (affinePhaseOneRightBits n t advice.length (affineIterationTarget t target)) → Bool) : affineCorrelationBreakerSelectedRuntime t target (List.ofFn x) (List.ofFn y) advice = List.ofFn (affineCorrelationBreakerSelected n t target advice x y)

The selected total program computes the complete semantic construction with every guard discharged.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerSelectedRuntime_mem_FP {t target : List Bool → ℕ} {x y advice : List Bool → List Bool} (ht : Complexity.UnaryFn t) (htarget : Complexity.UnaryFn target) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) (hadvice : advice ∈ Complexity.FP) : (fun (z : List Bool) => affineCorrelationBreakerSelectedRuntime (t z) (target z) (x z) (y z) (advice z)) ∈ Complexity.FP

Parameter computation, normalization, initialization, and all rounds are uniformly polynomial-time.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerSelectedEval_pair (x y advice parameter targetWord : List Bool) : affineCorrelationBreakerSelectedEval (Complexity.pair (Complexity.pair x (Complexity.pair y advice)) (Complexity.pair parameter targetWord)) = affineCorrelationBreakerSelectedRuntime parameter.length targetWord.length x y advice

Decode three data words and the two unary parameters.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerSelectedEval_eq (n t target : ℕ) (advice : List Bool) (x : Fin n → Bool) (y : Fin (affinePhaseOneRightBits n t advice.length (affineIterationTarget t target)) → Bool) : affineCorrelationBreakerSelectedEval (Complexity.pair (Complexity.pair (List.ofFn x) (Complexity.pair (List.ofFn y) advice)) (Complexity.pair (List.replicate t true) (List.replicate target true))) = List.ofFn (affineCorrelationBreakerSelected n t target advice x y)

One paired evaluator serializes the entire selected semantic construction exactly.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerSelectedEval_mem_FP : affineCorrelationBreakerSelectedEval ∈ Complexity.FP

The single complete evaluator is polynomial-time on every encoded or malformed input.