Finite logarithmic bounds for the selected affine parameters

The number of candidates remains the actual 2^s. Its bit width is cubic in the iterated logarithm. Exact advice and round accounting bounds the affine seed width and the growing matched depth without replacing this candidate count by a fixed power of the original logarithm.

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_clog_tampering (b : ℕ) : Nat.clog 2 (sourceReductionTamperingCount b + 1) = sourceReductionCandidateBits b + 2

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_phaseOneBase_eq (n b : ℕ) : affinePhaseOneBase n (sourceReductionTamperingCount b) (sourceReductionAdviceLength b) (affineIterationTarget (sourceReductionTamperingCount b) (sourceReductionTarget b)) = 62 * b + 4 * sourceReductionCandidateBits b + Nat.clog 2 (n + 1) + 271

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_candidateBits_le (L : ℕ) : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ 2 ^ 41 * (Nat.clog 2 (L + 1) + 1) ^ 3

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_advice_le {L : ℕ} (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : sourceReductionAdviceLength (matchedBlockSeedBits L) + 1 ≤ 2 ^ 29 * L

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_phaseOneBase_le {n L : ℕ} (length : Nat.clog 2 (n + 1) ≤ L) (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : affinePhaseOneBase n (sourceReductionTamperingCount (matchedBlockSeedBits L)) (sourceReductionAdviceLength (matchedBlockSeedBits L)) (affineIterationTarget (sourceReductionTamperingCount (matchedBlockSeedBits L)) (sourceReductionTarget (matchedBlockSeedBits L))) ≤ 2 ^ 31 * L

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionSeedBits_le_pow {n L : ℕ} (length : Nat.clog 2 (n + 1) ≤ L) (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : sourceReductionSeedBits n L ≤ 2 ^ (304 + sourceReductionCandidateBits (matchedBlockSeedBits L) + 4 * Nat.clog 2 (L + 1))

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_depth_le {n L : ℕ} (length : Nat.clog 2 (n + 1) ≤ L) (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : growingMatchedBlockDepth (sourceReductionSeedBits n L) ≤ 369 + sourceReductionCandidateBits (matchedBlockSeedBits L) + 4 * Nat.clog 2 (L + 1)

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_depth_le_cubic {n L : ℕ} (length : Nat.clog 2 (n + 1) ≤ L) (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : growingMatchedBlockDepth (sourceReductionSeedBits n L) ≤ 2 ^ 42 * (Nat.clog 2 (L + 1) + 1) ^ 3

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_error_overhead_le {n L : ℕ} (length : Nat.clog 2 (n + 1) ≤ L) (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : 4 + growingMatchedBlockDepth (sourceReductionSeedBits n L) + 2 ≤ 2 ^ 43 * (Nat.clog 2 (L + 1) + 1) ^ 3

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_growing_overhead_le {n L : ℕ} (length : Nat.clog 2 (n + 1) ≤ L) (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : (growingMatchedBlockDepth (sourceReductionSeedBits n L) + 1) * (4 + 2 * growingMatchedBlockDepth (sourceReductionSeedBits n L) + Nat.clog 2 (L + 1) + 4) ≤ 2 ^ 90 * (Nat.clog 2 (L + 1) + 1) ^ 6

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionEntropy_le_pow {n L : ℕ} (length : Nat.clog 2 (n + 1) ≤ L) (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : sourceReductionEntropy n L ≤ 2 ^ (753 + 2 * sourceReductionCandidateBits (matchedBlockSeedBits L) + 9 * Nat.clog 2 (L + 1))

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionEntropy_le_cubic_exp {n L : ℕ} (length : Nat.clog 2 (n + 1) ≤ L) (positive : 0 < L) (candidates : sourceReductionCandidateBits (matchedBlockSeedBits L) ≤ L) : sourceReductionEntropy n L ≤ 2 ^ (2 ^ 44 * (Nat.clog 2 (L + 1) + 1) ^ 3)