Identity strong condensation

Ignoring a finite seed and retaining the source is an exact strong condenser at the original source cap. A singleton seed therefore supplies a seed-free initialization for block condensation. Empty seed alphabets and threshold zero are also covered by the existing total finite-weight definitions.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededCondenser.id {X : Type u_1} {Seed : Type u_2} [Fintype X] [Fintype Seed] {K : ℕ} {ε : ℝ} (nonnegative : 0 ≤ ε) : WeightedStrongSeededCondenser (fun (x : X) (x_1 : Seed) => x) K K ε

Retaining the source preserves every cap with zero error, hence with any nonnegative error.