Universal recovery menus

Let K be a field with q = 2 ^ b elements and let L = ℓ * b, so that a point of K ^ ℓ takes L bits. A state of the scheduler consists of at most g occupied lines, each given by an anchor and a direction, and a tuple of k ≤ g targets; there are at most 2 ^ (g * (1 + 3 * L)) states. Under the budget 512 * g * q ≤ q ^ (ℓ - 1), a uniformly random tuple of nonzero directions leaves fewer than half of the requests clean with probability at most 2 ^ (-k) in every state (card_filter_two_mul_card_isClean_lt_mul_two_pow_le). A list of menuLength g k L independent tuples therefore fails some state with probability less than one (exists_coveringMenu), so a universal menu of that length exists.

For k > 0, menuLength g k L = ⌊g * (1 + 3 * L) / k⌋ + 1; evaluating every entry of such a menu examines k * menuLength g k L ≤ g * (1 + 3 * L) + k candidate lines.

Main definitions

• Cslib.LineCode.menuLength: the length of the universal menus.

Main results

• Cslib.LineCode.lt_mul_menuLength, Cslib.LineCode.mul_menuLength_le: bounds on the number k * menuLength g k L of candidate lines.
• Cslib.LineCode.exists_isUniversalMenu: universal menus exist under the budget.

References

• Adapted, with nonzero vectors in place of projective directions, from MassProduction/Nonuniform/PhaseMenu.lean, MassProduction/Nonuniform/BinaryPhaseMenu.lean and MassProduction/Nonuniform/Menu.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.LineCode.menuLength (g k L : ℕ) : ℕ

The length of the universal menus for k pending requests, g occupied lines and points of L bits: ⌊g * (1 + 3 * L) / k⌋ + 1, the least r with g * (1 + 3 * L) < k * r when 0 < k.

theorem Cslib.LineCode.lt_mul_menuLength (g L : ℕ) {k : ℕ} (hk : 0 < k) : g * (1 + 3 * L) < k * menuLength g k L

A menu of length menuLength g k L has more than g * (1 + 3 * L) candidate lines.

theorem Cslib.LineCode.mul_menuLength_le (g k L : ℕ) : k * menuLength g k L ≤ g * (1 + 3 * L) + k

A menu of length menuLength g k L has at most g * (1 + 3 * L) + k candidate lines.

theorem Cslib.LineCode.exists_isUniversalMenu {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b g k : ℕ} (hK : Fintype.card K = 2 ^ b) (hbudget : 512 * g * Fintype.card K ≤ Fintype.card K ^ (ℓ - 1)) (hk : 0 < k) (hkg : k ≤ g) : ∃ (menu : Fin (menuLength g k (ℓ * b)) → Fin k → Fin ℓ → K), IsUniversalMenu g menu

Universal menus. Let K have q = 2 ^ b elements, let 0 < k ≤ g, and suppose 512 * g * q ≤ q ^ (ℓ - 1). Then some menu of menuLength g k (ℓ * b) tuples of nonzero directions for k requests is universal for g occupied lines: for every list of at most g occupied lines and every tuple of k targets, possibly repeated or occupied, some entry leaves at least half of the requests clean.