Sweeps and the frontier counting lemma

A sweep of a set of inputs S ⊆ U^ι reveals the coordinates of an input a few at a time: ∅ = X 0, X 1, ..., X T = ι. At each time t an input has a message μ t x, which may depend on the whole input. The defining property is that messages permit splicing: if two inputs of S send the same message at time t, then the revealed part of one may be spliced onto the unrevealed part of the other without leaving S. The last message, sent once everything is revealed, is the same for all inputs of S.

Between times t and t + 1 an input x takes the transition (μ t x, μ (t + 1) x, x|_{X (t + 1) \ X t}): the message before the step, the message after it, and the coordinates revealed during it.

The frontier counting lemma (Sweep.ncard_le). If S is K-rectangle-free and has at least K elements, then |S| ≤ (K - 1) ^ 2 · ∑ₜ #{transitions taken at step t}.

The proof charges each input x to the first time t + 1 at which the inputs sharing its message (its peers) have at least K distinct revealed parts. The rectangular hull of the peers lies inside S, so they have fewer than K distinct unrevealed parts. At time t the peers of x still had fewer than K distinct revealed parts. An input charged to a step is determined by its transition, its part revealed by time t and its part unrevealed at time t + 1; hence at most (K - 1) ^ 2 inputs share a charged step and a transition.

Nothing here mentions graphs or circuits: a sweep is an abstract family of splicing messages, and its charging argument is shared by everything swept along a layout. The chosen accepting paths of a read-once branching program form a sweep of its accepted set, which gives the rectangle bound for such programs (Cslib.Circuits.Frontier.ReadOnceNBP.ncard_accepted_le), and through them the counting lemma for constraint networks. Constraint networks swept along a layout with extra messages, such as a ledger, produce sweeps whose messages are the extra messages and the values on the edges of the frontier (Cslib.Circuits.Frontier.Network.frontierSweep).

Main definitions

• Cslib.Circuits.Frontier.Sweep S M: a sweep of S with messages in M.
• Cslib.Circuits.Frontier.Sweep.transition: the transition taken by an input at a step.
• Cslib.Circuits.Frontier.Sweep.transitionCount: the number of transitions taken by inputs of S, summed over the steps.

Main results

• Cslib.Circuits.Frontier.Sweep.ncard_le_mul_transitionCount: the charging argument, for any two thresholds that bound the two sides of every message class.
• Cslib.Circuits.Frontier.Sweep.ncard_le: the frontier counting lemma.

structure Cslib.Circuits.Frontier.Sweep {ι : Type u_1} {U : Type u_2} (S : Set (ι → U)) (M : Type u_3) : Type (max (max u_1 u_2) u_3)

A sweep of a set of inputs S: coordinates revealed over time, starting from none and ending with all, and a message at each time such that inputs of S sending the same message can exchange their unrevealed parts.

• length : ℕ

  The number of steps.

• revealed : ℕ → Set ι

  The coordinates revealed by time t.

• revealed_zero : self.revealed 0 = ∅

  Nothing is revealed at the start.

• revealed_length : self.revealed self.length = Set.univ

  Everything is revealed at the end.

• message : ℕ → (ι → U) → M

  The message at time t, possibly depending on the whole input.

• message_length (x : ι → U) : x ∈ S → ∀ y ∈ S, self.message self.length x = self.message self.length y

  The final message is the same for all inputs of S.

• splice (t : ℕ) (x : ι → U) : x ∈ S → ∀ y ∈ S, self.message t x = self.message t y → ∀ (z : ι → U), Set.EqOn z x (self.revealed t) → Set.EqOn z y (self.revealed t)ᶜ → z ∈ S

  Messages permit splicing: if two inputs of S send the same message at time t, the revealed part of one and the unrevealed part of the other form an input of S.

def Cslib.Circuits.Frontier.Sweep.newly {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) (t : ℕ) : Set ι

The coordinates revealed during step t, between times t and t + 1.

def Cslib.Circuits.Frontier.Sweep.transition {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) (t : ℕ) (x : ι → U) : M × M × (↑(P.newly t) → U)

The transition taken by x at step t: its messages before and after the step, and its part revealed during the step.

noncomputable def Cslib.Circuits.Frontier.Sweep.transitionCount {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) : ℕ

The number of transitions taken by inputs of S, summed over the steps of the sweep.

theorem Cslib.Circuits.Frontier.Sweep.ncard_transition_le_of_factorsThrough {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] {t : ℕ} {R : Type u_4} {D : Type u_5} [Finite D] (h : (ι → U) → R) (g : (ι → U) → D) (hg : ∀ x ∈ S, ∀ y ∈ S, h x = h y → g x = g y → P.transition t x = P.transition t y) : (P.transition t '' S).ncard ≤ (h '' S).ncard * Nat.card D

Counting transitions by what determines them: if on S the transition at step t is a function of h and of a quantity g with values in a finite type D, then there are at most #(values of h on S) * |D| transitions at step t.

The charging argument

def Cslib.Circuits.Frontier.Sweep.peers {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) (t : ℕ) (x : ι → U) : Set (ι → U)

The peers of x at time t: the inputs of S that send the same message as x.

def Cslib.Circuits.Frontier.Sweep.pastSide {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) (t : ℕ) (x : ι → U) : Set (↑(P.revealed t) → U)

The distinct parts revealed by time t among the peers of x.

def Cslib.Circuits.Frontier.Sweep.futureSide {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) (t : ℕ) (x : ι → U) : Set (↑(P.revealed t)ᶜ → U)

The distinct parts unrevealed at time t among the peers of x.

theorem Cslib.Circuits.Frontier.Sweep.pastSide_lt_or_futureSide_lt {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) {K : ℕ} (hS : RectangleFree S K) (t : ℕ) (x : ι → U) : (P.pastSide t x).ncard < K ∨ (P.futureSide t x).ncard < K

The rectangular hull of the peers of x lies inside S, so in a rectangle-free set one of its sides is small.

theorem Cslib.Circuits.Frontier.Sweep.one_le_ncard_pastSide {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] {x : ι → U} (hx : x ∈ S) (t : ℕ) : 1 ≤ (P.pastSide t x).ncard

An input of S is among its own peers, so its past side is nonempty.

theorem Cslib.Circuits.Frontier.Sweep.one_le_ncard_futureSide {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] {x : ι → U} (hx : x ∈ S) (t : ℕ) : 1 ≤ (P.futureSide t x).ncard

An input of S is among its own peers, so its future side is nonempty.

theorem Cslib.Circuits.Frontier.Sweep.ncard_pastSide_zero_le {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) (x : ι → U) : (P.pastSide 0 x).ncard ≤ 1

At the start nothing is revealed, so there is at most one revealed part.

theorem Cslib.Circuits.Frontier.Sweep.ncard_pastSide_length {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) {x : ι → U} (hx : x ∈ S) : (P.pastSide P.length x).ncard = S.ncard

At the end everything is revealed and every input of S is a peer, so the revealed parts are as numerous as S.

noncomputable def Cslib.Circuits.Frontier.Sweep.chargeTime {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) (K : ℕ) (x : ι → U) : ℕ

The time at which x is charged: the first time its peers have at least K distinct revealed parts.

theorem Cslib.Circuits.Frontier.Sweep.ncard_le_mul_transitionCount {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] {KL KR : ℕ} (hKL : 1 < KL) (hK : KL ≤ S.ncard) (hsides : ∀ t ≤ P.length, ∀ x ∈ S, (P.pastSide t x).ncard < KL ∨ (P.futureSide t x).ncard < KR) : S.ncard ≤ (KL - 1) * (KR - 1) * P.transitionCount

The charging argument. If at every time up to the end each input of S has fewer than KL distinct revealed parts or fewer than KR distinct unrevealed parts among its peers, then |S| ≤ (KL - 1) (KR - 1) · #transitions, provided 1 < KL ≤ |S|.

theorem Cslib.Circuits.Frontier.Sweep.ncard_le {ι : Type u_1} {U : Type u_2} {M : Type u_3} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] {K : ℕ} (hS : RectangleFree S K) (hK : K ≤ S.ncard) : S.ncard ≤ (K - 1) ^ 2 * P.transitionCount

The frontier counting lemma. A K-rectangle-free set with at least K elements has at most (K - 1) ^ 2 elements per transition of any of its sweeps.