Strong finite seeded extraction and output-only tests

The strong contract compares every joint seed-output test with independent uniform sampling. Its finite probability identities include product tests, normalization, and the exact output-only seed-hit formula. Thus strong extraction implies the existing flat seeded extractor contract, with the same cardinality threshold and error.

Increasing the threshold or allowed error preserves the strong property. The conversion to the division-free contract treats empty sources directly, so it also applies at threshold zero. These are basic finite counting and normalization results, without an extractor construction or entropy loss.

@[simp]

theorem Algebraic.Cutwidth.Extractor.uniformSeededTestProb_empty {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] : uniformSeededTestProb ∅ = 0

The empty joint test has probability zero, including empty sampling types.

theorem Algebraic.Cutwidth.Extractor.uniformSeededTestProb_nonneg {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] (T : Finset (Seed × Ω)) : 0 ≤ uniformSeededTestProb T

Every uniform joint test has nonnegative probability.

theorem Algebraic.Cutwidth.Extractor.uniformSeededTestProb_le_one {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] (T : Finset (Seed × Ω)) : uniformSeededTestProb T ≤ 1

Every uniform joint test has probability at most one, including empty types.

theorem Algebraic.Cutwidth.Extractor.uniformSeededTestProb_product {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] (S : Finset Seed) (T : Finset Ω) : uniformSeededTestProb (S.product T) = ↑S.card / ↑(Fintype.card Seed) * (↑T.card / ↑(Fintype.card Ω))

Independent uniform sampling factors a rectangular joint test.

theorem Algebraic.Cutwidth.Extractor.uniformSeededTestProb_univ_product {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] [Nonempty Seed] (T : Finset Ω) : uniformSeededTestProb (Finset.univ.product T) = ↑T.card / ↑(Fintype.card Ω)

Ignoring a nonempty uniform seed leaves the usual uniform output probability.

@[simp]

theorem Algebraic.Cutwidth.Extractor.uniformSeededTestProb_univ {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] [Nonempty Seed] [Nonempty Ω] : uniformSeededTestProb Finset.univ = 1

The whole joint space has probability one when both sampling types are nonempty.

theorem Algebraic.Cutwidth.Extractor.seededTestProb_univ_product {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] (E : α → Seed → Ω) (P : Finset α) (T : Finset Ω) : seededTestProb (fun (x : ↥P) => E ↑x) (Finset.univ.product T) = (∑ x ∈ P, ↑(seedHits E T x)) / (↑P.card * ↑(Fintype.card Seed))

An output-only test counts every source and seed pair, even when outputs repeat. The identity also holds for an empty support or seed type.

theorem Algebraic.Cutwidth.Extractor.FlatStrongSeededExtractor.mono_threshold {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} {K L : ℕ} {ε : ℝ} (extract : FlatStrongSeededExtractor E K ε) (threshold : K ≤ L) : FlatStrongSeededExtractor E L ε

Raising the minimum source-support size preserves strong extraction.

theorem Algebraic.Cutwidth.Extractor.FlatStrongSeededExtractor.mono_error {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} {K : ℕ} {ε δ : ℝ} (extract : FlatStrongSeededExtractor E K ε) (error : ε ≤ δ) : FlatStrongSeededExtractor E K δ

Increasing the allowed discrepancy preserves strong extraction.

theorem Algebraic.Cutwidth.Extractor.FlatStrongSeededExtractor.mono {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} {K L : ℕ} {ε δ : ℝ} (extract : FlatStrongSeededExtractor E K ε) (threshold : K ≤ L) (error : ε ≤ δ) : FlatStrongSeededExtractor E L δ

Both the support threshold and permitted error may be increased.

theorem Algebraic.Cutwidth.Extractor.FlatStrongSeededExtractor.flatSeededExtractor {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] [Nonempty Seed] [Nonempty Ω] {E : α → Seed → Ω} {K : ℕ} {ε : ℝ} (extract : FlatStrongSeededExtractor E K ε) : FlatSeededExtractor E K ε

Forgetting the retained seed gives the existing flat seeded extractor property. The threshold may be zero; the empty-support inequality holds independently.