Verification of the explicit advice parameters

The logarithms of the two enlarged widths are bounded through powers of two, retaining the scale's ample fixed slack. The three entropy reserves follow from the previously checked finite error budget. No source distribution or capacity of the chosen reserve in the left input is asserted here.

theorem Algebraic.Cutwidth.Extractor.Internal.adviceParameters_error_le (n a target out : ℕ) : adviceErrorExponent a target ≤ adviceScale n a target out

theorem Algebraic.Cutwidth.Extractor.Internal.adviceParameters_sizeGuard (n a target out : ℕ) : FlipFlopSizeGuard n (adviceSourceEntropy n a target out) (adviceScale n a target out) (adviceErrorExponent a target)

theorem Algebraic.Cutwidth.Extractor.Internal.adviceParameters_stateWidth_le (n a target out : ℕ) : matchedBlockOutputBits 64 (adviceScale n a target out) ≤ adviceSourceEntropy n a target out

theorem Algebraic.Cutwidth.Extractor.Internal.adviceParameters_output_le (n a target out : ℕ) : out ≤ matchedBlockSeedBits (adviceScale n a target out)

theorem Algebraic.Cutwidth.Extractor.Internal.adviceParameters_state_reserve (n a target out : ℕ) : 2 ^ 62 * adviceScale n a target out + 2 * matchedBlockSeedBits (adviceScale n a target out) + adviceErrorExponent a target ≤ matchedBlockOutputBits 64 (adviceScale n a target out)

theorem Algebraic.Cutwidth.Extractor.Internal.adviceParameters_left_reserve (n a target out : ℕ) : 2 ^ 62 * adviceScale n a target out + (8 * a + 7) * matchedBlockSeedBits (adviceScale n a target out) + adviceErrorExponent a target ≤ adviceSourceEntropy n a target out

theorem Algebraic.Cutwidth.Extractor.Internal.adviceParameters_right_reserve (n a target out : ℕ) : 2 ^ 142 * adviceScale n a target out + (5 * a + 5) * matchedBlockOutputBits 64 (adviceScale n a target out) + adviceErrorExponent a target ≤ adviceSourceEntropy n a target out