Uniform computation with two bounded enumeration loops

Both loop counts are supplied as polynomial-time unary numbers. Every call uses the actual sampler and selected affine algorithms. XOR is a one-bit-state fold; the outer list then feeds the checked majority program. No source distribution, extractor guard, or exponential count-generation claim enters these computation theorems.

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionCallRuntime_mem_FP {L C i j : List Bool → ℕ} {source : List Bool → List Bool} (hL : Complexity.UnaryFn L) (hC : Complexity.UnaryFn C) (hi : Complexity.UnaryFn i) (hj : Complexity.UnaryFn j) (hsource : source ∈ Complexity.FP) : (fun (z : List Bool) => [sourceReductionCallRuntime (L z) (C z) (source z) (i z) (j z)]) ∈ Complexity.FP

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionCandidatesRuntime_mem_FP {L C i : List Bool → ℕ} {source : List Bool → List Bool} (hL : Complexity.UnaryFn L) (hC : Complexity.UnaryFn C) (hi : Complexity.UnaryFn i) (hsource : source ∈ Complexity.FP) : (fun (z : List Bool) => sourceReductionCandidatesRuntime (L z) (C z) (source z) (i z)) ∈ Complexity.FP

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionRowsRuntime_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) => sourceReductionRowsRuntime (L z) (N z) (C z) (source z)) ∈ Complexity.FP

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

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

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionCandidatesRuntime_length (L C : ℕ) (source : List Bool) (i : ℕ) : (sourceReductionCandidatesRuntime L C source i).length = C

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

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

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