Weighted strong condensation from flat lossless witnesses

Lossless injection witnesses for every exact-size flat source imply strong condensation of every normalized source with the same point-mass cap. The ideal conditional output at each seed is a genuine normalized capped distribution, obtained by mixing the images of the flat components. The total variation error is unchanged, and the seed remains uniform.

A weighted strong extractor is also a condenser at full output entropy: its ideal conditional law is uniform on the whole output type at each seed.

The transfer uses the exact Birkhoff-based decomposition in Strong.FlatMixture, followed by finite mixture identities and the equal-mass characterization of total variation by tests. It asserts no algorithm for computing arbitrary real mixture weights or ideal witnesses.

theorem Algebraic.Cutwidth.Extractor.weightedSeededOutput_eq_mapWeight {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (p : α → ℝ) (C : α → Seed → Ω) : weightedSeededOutput p C = mapWeight (fun (xy : α × Seed) => (xy.2, C xy.1 xy.2)) fun (xy : α × Seed) => p xy.1 / ↑(Fintype.card Seed)

The joint output counts each source and seed occurrence through its deterministic image.

theorem Algebraic.Cutwidth.Extractor.isProbabilityWeight_seedFamilyWeight {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] [Nonempty Seed] (q : Seed → Ω → ℝ) (probability : ∀ (y : Seed), IsProbabilityWeight (q y)) : IsProbabilityWeight (seedFamilyWeight q)

Normalized conditional distributions and a nonempty uniform seed give a probability law.

theorem Algebraic.Cutwidth.Extractor.IsProbabilityWeight.weightedSeededOutput {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty Seed] {p : α → ℝ} (probability : IsProbabilityWeight p) (C : α → Seed → Ω) : IsProbabilityWeight (Extractor.weightedSeededOutput p C)

A probability source with a nonempty independent uniform seed stays normalized after mapping.

theorem Algebraic.Cutwidth.Extractor.weightTestProb_weightedSeededOutput {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (p : α → ℝ) (C : α → Seed → Ω) (T : Finset (Seed × Ω)) : weightTestProb (weightedSeededOutput p C) T = weightedSeededTestProb p C T

Testing joint output weights is exactly the existing weighted seeded-test probability.

theorem Algebraic.Cutwidth.Extractor.weightTestProb_seedFamilyWeight {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] (q : Seed → Ω → ℝ) (T : Finset (Seed × Ω)) : weightTestProb (seedFamilyWeight q) T = (∑ yz ∈ T, q yz.1 yz.2) / ↑(Fintype.card Seed)

A conditional output family uses the uniform seed denominator in every joint test.

theorem Algebraic.Cutwidth.Extractor.weightTestProb_seedFamilyWeight_uniform {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] (T : Finset (Seed × Ω)) : weightTestProb (seedFamilyWeight fun (x : Seed) => uniformWeight Ω) T = uniformSeededTestProb T

Uniform conditional outputs give exactly the independent uniform seed-output law.

theorem Algebraic.Cutwidth.Extractor.weightTestProb_seedFamilyWeight_mixture {ι : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype ι] [Fintype Seed] (w : ι → ℝ) (q : ι → Seed → Ω → ℝ) (T : Finset (Seed × Ω)) : weightTestProb (seedFamilyWeight fun (y : Seed) (z : Ω) => ∑ i : ι, w i * q i y z) T = ∑ i : ι, w i * weightTestProb (seedFamilyWeight (q i)) T

Joint tests are linear in a supplied finite mixture of conditional output families.

theorem Algebraic.Cutwidth.Extractor.CappedWeight.map_injective {α : Type u_1} {β : Type u_2} [Fintype α] {p : α → ℝ} {K : ℕ} (cap : CappedWeight p K) (f : α → β) (injective : Function.Injective f) : CappedWeight (mapWeight f p) K

An injective deterministic map preserves every point-mass cap.

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

Strong extraction is strong condensation at full output entropy with the same error.

theorem Algebraic.Cutwidth.Extractor.weightedStrongSeededCondenser_of_flat_injections {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty Seed] (C : α → Seed → Ω) {K : ℕ} (positive : 0 < K) {ε : ℝ} (flat : ∀ (P : Finset α), P.card = K → ∃ (g : Seed → ↥P ↪ Ω), ∀ (T : Finset (Seed × Ω)), |seededTestProb (fun (x : ↥P) => C ↑x) T - seededTestProb (fun (x : ↥P) (y : Seed) => (g y) x) T| ≤ ε) : WeightedStrongSeededCondenser C K K ε

Exact-size flat lossless witnesses extend to arbitrary capped sources with the same error. The resulting conditional witness is normalized and capped at every retained seed.