Counting tools for universal menus

Three finite counting principles replace probability in the construction of universal menus.

• Collision cut (exists_collisionCut). In a graph, let every vertex of a finite set bad either satisfy a property P or have a neighbor. Two-coloring a spanning forest gives a subset of at least half of bad whose vertices satisfy P or have a neighbor outside the subset.
• Conditional counting (card_filter_forall_mem_le). If the allowed values of each selected coordinate depend only on the unselected coordinates, then at most M ^ #S assignments of the #S selected coordinates are allowed for each assignment of the others.
• Covering menus (exists_coveringMenu). If for every state at most a 2 ^ (-m) fraction of the candidates fail, and there are fewer than 2 ^ (m * r) states, then some list of r candidates contains a successful candidate for every state.

Main results

• Cslib.LineCode.exists_collisionCut: the collision cut.
• Cslib.LineCode.card_filter_forall_mem_le: conditional counting.
• Cslib.LineCode.exists_coveringMenu: covering menus.

References

• Adapted from MassProduction/Nonuniform/CollisionCut.lean, MassProduction/Nonuniform/ConditionalCounting.lean and MassProduction/Nonuniform/Menu.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.LineCode.exists_collisionCut {V : Type u_1} (G : SimpleGraph V) (P : V → Prop) (bad : Finset V) (h : ∀ v ∈ bad, P v ∨ ∃ (w : V), G.Adj v w) : ∃ S ⊆ bad, bad.card ≤ 2 * S.card ∧ ∀ v ∈ S, P v ∨ ∃ w ∉ S, G.Adj v w

Collision cut. If every vertex of bad satisfies P or has a neighbor, then some S ⊆ bad with #bad ≤ 2 * #S has every vertex satisfying P or adjacent to a vertex outside S.

theorem Cslib.LineCode.card_filter_forall_mem_le {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype α] (S : Finset ι) (A : ({ i : ι // i ∉ S } → α) → ι → Finset α) (M : ℕ) (hA : ∀ (y : { i : ι // i ∉ S } → α), ∀ i ∈ S, (A y i).card ≤ M) [DecidablePred fun (x : ι → α) => ∀ i ∈ S, x i ∈ A (fun (j : { i : ι // i ∉ S }) => x ↑j) i] : {x : ι → α | ∀ i ∈ S, x i ∈ A (fun (j : { i : ι // i ∉ S }) => x ↑j) i}.card ≤ Fintype.card α ^ (Fintype.card ι - S.card) * M ^ S.card

Conditional counting. Suppose the allowed values A y i of each coordinate i ∈ S depend only on the values y of the coordinates outside S, and number at most M. Then at most Fintype.card α ^ (Fintype.card ι - #S) * M ^ #S assignments take allowed values on all of S.

theorem Cslib.LineCode.exists_coveringMenu {σ : Type u_1} {α : Type u_2} [Fintype σ] [Fintype α] [Nonempty α] (good : σ → α → Prop) [(s : σ) → DecidablePred (good s)] (m r : ℕ) (hgood : ∀ (s : σ), {a : α | ¬good s a}.card * 2 ^ m ≤ Fintype.card α) (hσ : Fintype.card σ < 2 ^ (m * r)) : ∃ (menu : Fin r → α), ∀ (s : σ), ∃ (e : Fin r), good s (menu e)

Covering menus. If for every state s at most a 2 ^ (-m) fraction of the candidates fail good s, and there are fewer than 2 ^ (m * r) states, then some list of r candidates contains, for every state, a candidate that is good for it.