Instantiating two-round extraction with the actual matched-width programs

The actual look-ahead pushforward agrees definitionally with the generic three-call law. Both required strong extractors are the proved scheduled programs, with their full padded Boolean seeds. Cardinalities stay symbolic; no finite alphabet is enumerated to justify the statistical bound.

theorem Algebraic.Cutwidth.Extractor.Internal.flipFlopLookAheadWeight_eq (n L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) : flipFlopLookAheadWeight n L e w l r x x' q q' = lookAheadExtractionWeight w l r x x' q q' (flipFlopSeedPrefix L) (matchedBlockExtractor n 24 L e) (matchedBlockExtractor (matchedBlockOutputBits 64 L) 24 L e)

theorem Algebraic.Cutwidth.Extractor.Internal.flipFlopLookAheadWeight_probability (n L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (flipFlopLookAheadWeight n L e w l r x x' q q')

theorem Algebraic.Cutwidth.Extractor.Internal.flipFlopLookAhead_dist_le (n L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (length : Nat.clog 2 (n + 1) ≤ L) (right_length : Nat.clog 2 (matchedBlockOutputBits 64 L + 1) ≤ L) (room : 64 ≤ L) (error : e + 24 + 2 ≤ L) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (μ ν : Z → ℝ) {δ : ℝ} (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (left_nonnegative : ∀ (z : Z), 0 ≤ μ z) (right_nonnegative : ∀ (z : Z), 0 ≤ ν z) (left_cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (right_cap : ∀ (z : Z) (q₀ : Fin (matchedBlockOutputBits 64 L) → Bool), w z * mapWeight (q z) (r z) q₀ ≤ ν z) (seed : weightDist (retainedSeedWeight w r fun (z : Z) (b : B) => flipFlopSeedPrefix L (q z b)) (uniformSecondWeight (retainedSeedWeight w r fun (z : Z) (b : B) => flipFlopSeedPrefix L (q z b))) ≤ δ) : have K := 2 ^ (2 ^ 62 * L); have M := Fintype.card ((Fin (matchedBlockSeedBits L) → Bool) × (Fin (matchedBlockSeedBits L) → Bool)); weightDist (flipFlopLookAheadWeight n L e w l r x x' q q') (uniformSecondWeight (flipFlopLookAheadWeight n L e w l r x x' q q')) ≤ 3 * (2 ^ e)⁻¹ + δ + ↑K * (1 + ↑M) * ∑ z : Z, μ z + ↑K * ↑M * ∑ z : Z, ν z