Structural laws for finite block sources

A block source satisfies a mass cap for each coordinate after fixing every earlier coordinate. The caps survive taking prefixes, weakening the entropy threshold, and mixing sources with normalized nonnegative weights. Zero blocks impose only normalization; one block gives the usual point-mass cap. For two blocks the definition is equivalent to the marginal and conditional caps established by the separate Splitting module. A source with t blocks and threshold K satisfies (K^t)*p x ≤ 1 at every tuple. Using the alphabet cardinality as the threshold forces the entire tuple to be uniform.

These are finite structural ingredients for the block-source arguments in Chattopadhyay--Goodman--Liao, Section 5 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. Block.Condenser uses these laws to condense all blocks with a shared seed.

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

Taking all coordinates leaves a tuple unchanged.

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

Successive restrictions agree with a direct prefix restriction.

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

The full prefix retains each original point weight.

theorem Algebraic.Cutwidth.Extractor.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

The unique empty prefix has the source's total mass.

theorem Algebraic.Cutwidth.Extractor.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 ⋯

Marginalizing a prefix again agrees with marginalizing the original source.

theorem Algebraic.Cutwidth.Extractor.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

Prefix weights commute with arbitrary finite linear combinations.

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

A block source is a normalized nonnegative weighting.

theorem Algebraic.Cutwidth.Extractor.IsBlockSource.cap {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p K) (i : Fin t) (u : Fin (↑i + 1) → α) : ↑K * blockPrefixWeight p ⋯ u ≤ blockPrefixWeight p ⋯ (blockPrefix ⋯ u)

Every one-block prefix extension obeys the conditional mass cap.

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

With no blocks, there are no conditional caps to check.

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

A single block is a probability source with the ordinary point-mass cap.

theorem Algebraic.Cutwidth.Extractor.isBlockSource_two_iff {α : Type u_1} [Fintype α] (p : α × α → ℝ) (K : ℕ) : IsBlockSource (fun (x : Fin 2 → α) => p (x 0, x 1)) K ↔ IsProbabilityWeight p ∧ CappedWeight (firstWeight p) K ∧ ∀ (a b : α), ↑K * p (a, b) ≤ firstWeight p a

Pair weights form a two-block source exactly when the first marginal and every second-coordinate conditional satisfy the same threshold.

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

A smaller threshold weakens every conditional cap.

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

Every initial sequence of blocks retains the block-source threshold.

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

Conditional caps multiply to give the full tuple a threshold of K^t.

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

Full conditional entropy in every block forces the full tuple to be uniform.

theorem Algebraic.Cutwidth.Extractor.IsBlockSource.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

Normalized nonnegative mixtures preserve all conditional prefix caps.