Fixed menus covering every finite state

This module proves the finite counting step in the nonuniform scheduler. If a single candidate fails on only a small fraction of choices for each state, a short list of candidates covers every state simultaneously. The list is chosen once, before the runtime state is supplied.

The geometric failure estimate is a separate premise of this general lemma; no circuit or geometric scheduler bound is asserted in this module.

def Algebraic.MassProduction.Nonuniform.Covers {State : Type u_1} {Choice : Type u_2} {length : ℕ} (good : State → Choice → Prop) (menu : Fin length → Choice) : Prop

A menu covers all states if each state has a successful entry.

Equations

• Algebraic.MassProduction.Nonuniform.Covers good menu = ∀ (state : State), ∃ (entry : Fin length), good state (menu entry)

theorem Algebraic.MassProduction.Nonuniform.existsCoveringMenuOfCardBound {State : Type u_1} {Choice : Type u_2} [Fintype State] [Fintype Choice] (good : State → Choice → Prop) (length badBound : ℕ) (badSmall : ∀ (state : State), Nat.card { choice : Choice // ¬good state choice } ≤ badBound) (totalSmall : Fintype.card State * badBound ^ length < Fintype.card Choice ^ length) : ∃ (menu : Fin length → Choice), Covers good menu

Counting all-bad lists and then taking a union over states gives a fixed menu whenever the bad-list bound is smaller than the entire list space.

theorem Algebraic.MassProduction.Nonuniform.existsCoveringMenuOfExponentialBound {State : Type u_1} {Choice : Type u_2} [Fintype State] [Fintype Choice] [Nonempty Choice] (good : State → Choice → Prop) (descriptionBits exponent : ℕ) (exponentPositive : 0 < exponent) (statesSmall : Fintype.card State ≤ 2 ^ descriptionBits) (badSmall : ∀ (state : State), Nat.card { choice : Choice // ¬good state choice } * 2 ^ exponent ≤ Fintype.card Choice) : ∃ (menu : Fin (descriptionBits / exponent + 1) → Choice), Covers good menu

An exponential single-candidate failure bound and a state-description bound give a menu with descriptionBits / exponent + 1 entries.