Prefix identities and structural block-source proofs

Prefix caps are linear inequalities in the original weights. This gives closure under normalized nonnegative mixtures and weakening of the cap threshold, without conditional divisions or positive-prefix assumptions.

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefix_self {α : Type u_1} {t : ℕ} (x : Fin t → α) : blockPrefix ⋯ x = x

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefix_comp {α : Type u_1} {i j t : ℕ} (hij : i ≤ j) (hjt : j ≤ t) (x : Fin t → α) : blockPrefix hij (blockPrefix hjt x) = blockPrefix ⋯ x

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefixWeight_self {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin t → α) → ℝ) : blockPrefixWeight p ⋯ = p

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefixWeight_zero {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin t → α) → ℝ) (h : 0 ≤ t) (u : Fin 0 → α) : blockPrefixWeight p h u = ∑ x : Fin t → α, p x

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefixWeight_prefix {α : Type u_1} [Fintype α] {i j t : ℕ} (p : (Fin t → α) → ℝ) (hij : i ≤ j) (hjt : j ≤ t) : blockPrefixWeight (blockPrefixWeight p hjt) hij = blockPrefixWeight p ⋯

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefixWeight_mixture {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] {i t : ℕ} (p : ι → (Fin t → α) → ℝ) (w : ι → ℝ) (h : i ≤ t) (u : Fin i → α) : blockPrefixWeight (fun (x : Fin t → α) => ∑ j : ι, w j * p j x) h u = ∑ j : ι, w j * blockPrefixWeight (p j) h u

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_zero_iff {α : Type u_1} [Fintype α] (p : (Fin 0 → α) → ℝ) (K : ℕ) : IsBlockSource p K ↔ IsProbabilityWeight p

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_one_iff {α : Type u_1} [Fintype α] (p : (Fin 1 → α) → ℝ) (K : ℕ) : IsBlockSource p K ↔ IsProbabilityWeight p ∧ CappedWeight p K

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_mono {α : Type u_1} [Fintype α] {t K L : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p K) (threshold : L ≤ K) : IsBlockSource p L

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_prefix {α : Type u_1} [Fintype α] {j t K : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p K) (h : j ≤ t) : IsBlockSource (blockPrefixWeight p h) K

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_prefix_capped {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p K) (i : ℕ) (h : i ≤ t) : CappedWeight (blockPrefixWeight p h) (K ^ i)

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_capped {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p K) : CappedWeight p (K ^ t)

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_eq_uniform {α : Type u_1} [Fintype α] {t : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p (Fintype.card α)) : p = uniformWeight (Fin t → α)

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_mixture {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] {t K : ℕ} (p : ι → (Fin t → α) → ℝ) (w : ι → ℝ) (weights : IsProbabilityWeight w) (sources : ∀ (j : ι), IsBlockSource (p j) K) : IsBlockSource (fun (x : Fin t → α) => ∑ j : ι, w j * p j x) K