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 have 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, carries no information.

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 · ∑_t #{transitions taken at step t}.

The proof charges each input x to the first time t + 1 at which the inputs sharing its message have at least K distinct revealed parts. Their rectangular hull lies inside S, so they have fewer than K distinct unrevealed parts. At time t the inputs sharing the message 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. Its transitions alone need not form a correct branching program. Constraint networks swept along a vertex ordering produce sweeps whose messages are the values on the edges of the frontier (Frontier.Network.sweep).

Main definitions

• Frontier.Sweep S M: a sweep of S with messages in M.
• Frontier.Sweep.transition: the transition taken by an input at a step.

Main results

• Frontier.Sweep.ncard_le: the frontier counting lemma.

structure Complexity.Frontier.Sweep {ι : Type u_1} {U : Type u_2} (S : Set (ι → U)) (M : Type u_4) : Type (max (max u_1 u_2) u_4)

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 are sufficient: two inputs of S with the same message at time t may be spliced, the revealed part of one with the unrevealed part of the other, inside S.

def Complexity.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.

Equations

• P.newly t = P.revealed (t + 1) \ P.revealed t

def Complexity.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.

Equations

• P.transition t x = (P.message t x, P.message (t + 1) x, (P.newly t).domRestrict x)

The proof of the counting lemma

def Complexity.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 inputs of S that send the same message as x at time t.

Equations

• P.peers t x = {y : ι → U | y ∈ S ∧ P.message t y = P.message t x}

def Complexity.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.

Equations

• P.pastSide t x = (P.revealed t).domRestrict '' P.peers t x

def Complexity.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.

Equations

• P.futureSide t x = (P.revealed t)ᶜ.domRestrict '' P.peers t x

theorem Complexity.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 lies inside S: one of its sides is small.

theorem Complexity.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 Complexity.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 Complexity.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.

Equations

• P.chargeTime K x = sInf {t : ℕ | K ≤ (P.pastSide t x).ncard}

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

The total number of transitions used by accepted inputs.

Equations

• P.transitionCount = ∑ t ∈ Finset.range P.length, (P.transition t '' S).ncard

theorem Complexity.Frontier.Sweep.ncard_le_of_small_sides {ι : 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) (hsmall : ∀ (t : ℕ), ∀ x ∈ S, (P.pastSide t x).ncard < KL ∨ (P.futureSide t x).ncard < KR) : S.ncard ≤ (KL - 1) * (KR - 1) * P.transitionCount

Threshold charging only needs thin message classes, with asymmetric thresholds.

theorem Complexity.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 * ∑ t ∈ Finset.range P.length, (P.transition t '' S).ncard

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