Explicit entropy accounting for leakage-resilient affine calls

The complete source reserve is polynomial in the tampering count, advice length, target exponent, and logarithm of the original input length. The extra leakage cost is paid for every honest and tampered seed.

theorem Algebraic.Cutwidth.Extractor.affineLeakageSourceEntropy_le (n t a target : ℕ) : affineLeakageSourceEntropy n t a target ≤ 2 ^ 258 * (t + 1) ^ 2 * (a + 1) * affinePhaseOneBase n t a (affineIterationTarget t target) ^ 3

The actual complete source reserve, including leakage, obeys a finite cubic-base bound.