Uniform bounded evaluation of the complete finite source reduction

Two supplied unary counts bound the actual outer and candidate loops. Each call composes the sampler and selected affine program on the same original source. The two reductions then compute candidate XOR and strict majority, producing one bit on every input. The FP certificate includes parameter generation, binary advice encoding, and both bounded loops.

When the supplied counts equal the semantic counts and the growing sampler guard holds, the program computes sourceReductionExtractor exactly. The evaluator does not generate unrestricted exponential counts from their widths; choosing bounded counts for an eventual family is a separate layer. The construction follows Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 5.4 and the proof of Theorem 2: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.sourceReductionRowsRuntime_length (L N C : ℕ) (source : List Bool) : (sourceReductionRowsRuntime L N C source).length = N

The runtime preserves the supplied number of outer rows.

theorem Algebraic.Cutwidth.Extractor.sourceReductionRuntime_length (L N C : ℕ) (source : List Bool) : (sourceReductionRuntime L N C source).length = 1

Every parameter choice and source word produces one verdict bit.

theorem Algebraic.Cutwidth.Extractor.sourceReductionRuntime_zero_outer (L C : ℕ) (source : List Bool) : sourceReductionRuntime L 0 C source = [false]

The majority of no outer rows follows the false tie convention.

theorem Algebraic.Cutwidth.Extractor.sourceReductionRuntime_zero_candidates (L N : ℕ) (source : List Bool) : sourceReductionRuntime L N 0 source = [false]

Empty candidate rows all have false XOR, hence the verdict is false.

theorem Algebraic.Cutwidth.Extractor.sourceReductionRowsRuntime_eq (n L : ℕ) (base : GrowingMatchedBlockRuntimeValid n (sourceReductionSeedBits n L) L 4) (x : Fin n → Bool) : sourceReductionRowsRuntime L (sourceReductionOuterCount (matchedBlockSeedBits L)) (sourceReductionCandidateCount (matchedBlockSeedBits L)) (List.ofFn x) = List.ofFn (sourceReductionOutput n L x)

Exact binary enumeration computes every semantic XOR coordinate in its original order.

theorem Algebraic.Cutwidth.Extractor.sourceReductionRuntime_eq (n L N C : ℕ) (outer : N = sourceReductionOuterCount (matchedBlockSeedBits L)) (candidates : C = sourceReductionCandidateCount (matchedBlockSeedBits L)) (base : GrowingMatchedBlockRuntimeValid n (sourceReductionSeedBits n L) L 4) (x : Fin n → Bool) : sourceReductionRuntime L N C (List.ofFn x) = [sourceReductionExtractor n L x]

Exact supplied counts and the sampler guard identify the actual finite construction.

theorem Algebraic.Cutwidth.Extractor.sourceReductionRuntime_mem_FP {L N C : List Bool → ℕ} {source : List Bool → List Bool} (hL : Complexity.UnaryFn L) (hN : Complexity.UnaryFn N) (hC : Complexity.UnaryFn C) (hsource : source ∈ Complexity.FP) : (fun (z : List Bool) => sourceReductionRuntime (L z) (N z) (C z) (source z)) ∈ Complexity.FP

Supplied polynomial-time unary counts make both actual enumeration loops polynomial-time.

theorem Algebraic.Cutwidth.Extractor.sourceReductionEval_pair (source scale outerCount candidateCount : List Bool) : sourceReductionEval (Complexity.pair source (Complexity.pair scale (Complexity.pair outerCount candidateCount))) = sourceReductionRuntime scale.length outerCount.length candidateCount.length source

Decode the source word and all three supplied unary parameters.

theorem Algebraic.Cutwidth.Extractor.sourceReductionEval_length (input : List Bool) : (sourceReductionEval input).length = 1

Malformed paired words also produce exactly one bit.

theorem Algebraic.Cutwidth.Extractor.sourceReductionEval_eq (n L N C : ℕ) (outer : N = sourceReductionOuterCount (matchedBlockSeedBits L)) (candidates : C = sourceReductionCandidateCount (matchedBlockSeedBits L)) (base : GrowingMatchedBlockRuntimeValid n (sourceReductionSeedBits n L) L 4) (x : Fin n → Bool) : sourceReductionEval (Complexity.pair (List.ofFn x) (Complexity.pair (List.replicate L true) (Complexity.pair (List.replicate N true) (List.replicate C true)))) = [sourceReductionExtractor n L x]

The canonical paired evaluator computes the exact semantic Boolean output.

theorem Algebraic.Cutwidth.Extractor.sourceReductionEval_mem_FP : sourceReductionEval ∈ Complexity.FP

One total paired program includes all parameter, call, XOR, and majority computations.