Statistical certificates for the specified recursive components

Recombining the initial pair is injective, each internal map is the actual rate-three condenser, and a leaf reserve above the one-shot threshold suffices by monotonicity of the normalized source cap.

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockInitial_weighted (n h Q E : ℕ) [Fintype (ScheduledInitialSeed n h Q E)] : WeightedStrongSeededCondenser (scheduledBlockInitial n h Q E) (2 ^ recursiveBlockEntropy h Q 0) (2 ^ recursiveBlockEntropy h Q 0) (2 ^ E)⁻¹

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockStep_weighted (n h Q E i : ℕ) [Fintype (ScheduledLevelSeed n h Q E i)] : WeightedStrongSeededCondenser (scheduledBlockStep n h Q E i) (2 ^ recursiveBlockEntropy h Q i) (2 ^ recursiveBlockEntropy h Q i) (2 ^ E)⁻¹

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockLeaf_weighted (width h Q E ell : ℕ) [Fintype (AdjoinRoot (binaryModulus (oneShotCondenserExponent width ell E)))] [Fintype (AdjoinRoot (binaryModulus (oneShotHashExponent width ell E)))] (reserve : ell + 2 * E ≤ Q) : WeightedStrongSeededExtractor (fun (x : Fin width → Bool) => decodedOneShotExtractor width ell E (List.ofFn x)) (2 ^ recursiveBlockEntropy h Q h) (2 ^ E)⁻¹