Strict Beck–Fiala rounding for incidence matrices

A rational fractional selection in a finite zero-one incidence matrix can be rounded to zero-one integers with row discrepancy strictly below the maximum column degree bound, assumed positive. Initially integral coordinates are fixed.

This is the integer-making form, not the discrepancy bound derived from Komlós. The proof uses floating coordinates and preserves the sums of tight rows along a nonzero kernel direction until a coordinate reaches a boundary.

Ported from the separate Paper IV contribution working copy. The paper freeze is unchanged. This candidate introduces no dependency on the paper library.

def BeckFialaMatrix.floatingCoordinates {N : ℕ} (x : Fin N → ℚ) : Finset (Fin N)

The set of floating coordinates of x: those strictly between 0 and 1.

Equations

• BeckFialaMatrix.floatingCoordinates x = {i : Fin N | 0 < x i ∧ x i < 1}

def BeckFialaMatrix.floatingDegree {m N : ℕ} (A : Fin m → Fin N → ℤ) (x : Fin N → ℚ) (j : Fin m) : ℕ

The floating degree of row j: the number of floating coordinates in that row.

Equations

• BeckFialaMatrix.floatingDegree A x j = {i ∈ BeckFialaMatrix.floatingCoordinates x | A j i = 1}.card

theorem BeckFialaMatrix.mem_floatingCoordinates {N : ℕ} {x : Fin N → ℚ} {i : Fin N} : i ∈ floatingCoordinates x ↔ 0 < x i ∧ x i < 1

theorem BeckFialaMatrix.eq_zero_or_one_of_not_floating {N : ℕ} {x : Fin N → ℚ} {i : Fin N} (hx : 0 ≤ x i ∧ x i ≤ 1) (h : i ∉ floatingCoordinates x) : x i = 0 ∨ x i = 1

A coordinate that is not floating and lies in [0,1] is 0 or 1.

Slack rows: the direct discrepancy bound

theorem BeckFialaMatrix.slack_row_bound {m N t : ℕ} (ht : 1 ≤ t) (A : Fin m → Fin N → ℤ) (hA : ∀ (j : Fin m) (i : Fin N), A j i = 0 ∨ A j i = 1) (x : Fin N → ℚ) (y : Fin N → ℤ) (hy01 : ∀ (i : Fin N), y i = 0 ∨ y i = 1) (hagree : ∀ i ∉ floatingCoordinates x, ↑(y i) = x i) (j : Fin m) (hj : floatingDegree A x j ≤ t) : |∑ i : Fin N, ↑(A j i) * (↑(y i) - x i)| < ↑t

If y is a 0/1 vector agreeing with x off the floating set, then on a row whose floating degree is at most t (a slack row) the discrepancy is < t.

The counting lemma: #tight < #floating

theorem BeckFialaMatrix.tight_card_mul_le {m N t : ℕ} (A : Fin m → Fin N → ℤ) (hdeg : ∀ (i : Fin N), {j : Fin m | A j i = 1}.card ≤ t) (x : Fin N → ℚ) : {j : Fin m | t < floatingDegree A x j}.card * (t + 1) ≤ (floatingCoordinates x).card * t

Double counting: (t+1) * #tight ≤ t * #floating.

theorem BeckFialaMatrix.tight_card_lt {m N t : ℕ} (A : Fin m → Fin N → ℤ) (hdeg : ∀ (i : Fin N), {j : Fin m | A j i = 1}.card ≤ t) (x : Fin N → ℚ) (hne : (floatingCoordinates x).Nonempty) : {j : Fin m | t < floatingDegree A x j}.card < (floatingCoordinates x).card

The number of tight rows is strictly smaller than the number of floating variables.

The null-space step

theorem BeckFialaMatrix.exists_null_vector {m N : ℕ} (A : Fin m → Fin N → ℤ) (F : Finset (Fin N)) (T : Finset (Fin m)) (hcard : T.card < F.card) : ∃ (v : Fin N → ℚ), (∀ i ∉ F, v i = 0) ∧ (∃ i ∈ F, v i ≠ 0) ∧ ∀ j ∈ T, ∑ i : Fin N, ↑(A j i) * v i = 0

An underdetermined homogeneous system has a nonzero solution supported on F.

theorem BeckFialaMatrix.exists_step_along {N : ℕ} (x : Fin N → ℚ) (hx : ∀ (i : Fin N), 0 ≤ x i ∧ x i ≤ 1) (F : Finset (Fin N)) (hF : ∀ i ∈ F, 0 < x i ∧ x i < 1) (v : Fin N → ℚ) (hv0 : ∀ i ∉ F, v i = 0) (i0 : Fin N) (hi0 : i0 ∈ F) (hvi0 : v i0 ≠ 0) : ∃ (s : ℚ), 0 < s ∧ (∀ (i : Fin N), 0 ≤ x i + s * v i ∧ x i + s * v i ≤ 1) ∧ ∃ i ∈ F, x i + s * v i = 0 ∨ x i + s * v i = 1

Walking along a direction v supported on the floating set until a coordinate hits 0 or 1.

theorem BeckFialaMatrix.exists_rounding_step {m N t : ℕ} (A : Fin m → Fin N → ℤ) (hdeg : ∀ (i : Fin N), {j : Fin m | A j i = 1}.card ≤ t) (x : Fin N → ℚ) (hx : ∀ (i : Fin N), 0 ≤ x i ∧ x i ≤ 1) (j0 : Fin m) (hj0 : t < floatingDegree A x j0) : ∃ (x' : Fin N → ℚ), (∀ (i : Fin N), 0 ≤ x' i ∧ x' i ≤ 1) ∧ (∀ i ∉ floatingCoordinates x, x' i = x i) ∧ (floatingCoordinates x').card < (floatingCoordinates x).card ∧ ∀ (j : Fin m), t < floatingDegree A x j → ∑ i : Fin N, ↑(A j i) * x' i = ∑ i : Fin N, ↑(A j i) * x i

One rounding step: if some row is tight, we can strictly decrease the number of floating coordinates while keeping the frozen coordinates and all tight-row sums fixed.

theorem BeckFialaMatrix.exists_round_all_slack {m N t : ℕ} (ht : 1 ≤ t) (A : Fin m → Fin N → ℤ) (hA : ∀ (j : Fin m) (i : Fin N), A j i = 0 ∨ A j i = 1) (x : Fin N → ℚ) (hx : ∀ (i : Fin N), 0 ≤ x i ∧ x i ≤ 1) (hall : ∀ (j : Fin m), floatingDegree A x j ≤ t) : ∃ (y : Fin N → ℤ), (∀ (i : Fin N), y i = 0 ∨ y i = 1) ∧ (∀ i ∉ floatingCoordinates x, ↑(y i) = x i) ∧ ∀ (j : Fin m), |∑ i : Fin N, ↑(A j i) * (↑(y i) - x i)| < ↑t

If every row is slack, rounding all floating coordinates down already works.

The main induction

theorem BeckFialaMatrix.exists_rounding_induction {m N t : ℕ} (ht : 1 ≤ t) (A : Fin m → Fin N → ℤ) (hA : ∀ (j : Fin m) (i : Fin N), A j i = 0 ∨ A j i = 1) (hdeg : ∀ (i : Fin N), {j : Fin m | A j i = 1}.card ≤ t) (n : ℕ) (x : Fin N → ℚ) : (floatingCoordinates x).card ≤ n → (∀ (i : Fin N), 0 ≤ x i ∧ x i ≤ 1) → ∃ (y : Fin N → ℤ), (∀ (i : Fin N), y i = 0 ∨ y i = 1) ∧ (∀ i ∉ floatingCoordinates x, ↑(y i) = x i) ∧ ∀ (j : Fin m), |∑ i : Fin N, ↑(A j i) * (↑(y i) - x i)| < ↑t

The induction on the number of floating coordinates.

theorem BeckFialaMatrix.exists_rounding_preserving_integral {m N t : ℕ} (ht : 1 ≤ t) (A : Fin m → Fin N → ℤ) (hA : ∀ (j : Fin m) (i : Fin N), A j i = 0 ∨ A j i = 1) (hdeg : ∀ (i : Fin N), {j : Fin m | A j i = 1}.card ≤ t) (x : Fin N → ℚ) (hx : ∀ (i : Fin N), 0 ≤ x i ∧ x i ≤ 1) : ∃ (y : Fin N → ℤ), (∀ (i : Fin N), y i = 0 ∨ y i = 1) ∧ (∀ i ∉ floatingCoordinates x, ↑(y i) = x i) ∧ ∀ (j : Fin m), |∑ i : Fin N, ↑(A j i) * (↑(y i) - x i)| < ↑t

Strengthened Beck–Fiala statement: the rounding can be chosen to fix all coordinates that are already integral.

theorem BeckFialaMatrix.exists_rounding {m N t : ℕ} (ht : 1 ≤ t) (A : Fin m → Fin N → ℤ) (hA : ∀ (j : Fin m) (i : Fin N), A j i = 0 ∨ A j i = 1) (hdeg : ∀ (i : Fin N), {j : Fin m | A j i = 1}.card ≤ t) (x : Fin N → ℚ) (hx : ∀ (i : Fin N), 0 ≤ x i ∧ x i ≤ 1) : ∃ (y : Fin N → ℤ), (∀ (i : Fin N), y i = 0 ∨ y i = 1) ∧ ∀ (j : Fin m), |∑ i : Fin N, ↑(A j i) * (↑(y i) - x i)| < ↑t

Beck–Fiala integer-making theorem. If every element lies in at most t sets of a set system (i.e. every column of the 0/1 incidence matrix A has at most t ones) and x ∈ [0,1]^N is fractional, then x can be rounded to an integral y ∈ {0,1}^N whose discrepancy on every row is < t.

(The extra hypothesis 1 ≤ t is necessary; see zero_bound_counterexample below.)

theorem BeckFialaMatrix.zero_bound_counterexample : ¬∀ (m N t : ℕ) (A : Fin m → Fin N → ℤ), (∀ (j : Fin m) (i : Fin N), A j i = 0 ∨ A j i = 1) → (∀ (i : Fin N), {j : Fin m | A j i = 1}.card ≤ t) → ∀ (x : Fin N → ℚ), (∀ (i : Fin N), 0 ≤ x i ∧ x i ≤ 1) → ∃ (y : Fin N → ℤ), (∀ (i : Fin N), y i = 0 ∨ y i = 1) ∧ ∀ (j : Fin m), |∑ i : Fin N, ↑(A j i) * (↑(y i) - x i)| < ↑t

The hypothesis 1 ≤ t cannot be dropped: for t = 0 the conclusion would read |0| < 0.