Threshold charging for additive generators

A path can describe an input by adding its edge labels, without assigning each coordinate a unique read position. Prefix and suffix sums through the same state can be combined. A sumset disperser, unlike a coordinate-rectangle disperser, forbids a large sumset formed this way.

The transition threshold proof uses only reconstruction from the old prefix, the emitted label, and the new suffix. It does not require unique paths, disjoint coordinate scopes, or injectivity of addition on arbitrary prefix/suffix sets. The program-to-sweep direction is sound; no converse for arbitrary sweeps is claimed.

def Complexity.Frontier.SumsetFree {G : Type u_1} [Add G] (S : Set G) (K : ℕ) : Prop

S contains no sumset whose two summand sets both have cardinality at least K. This is a threshold property, not the usual additive-combinatorial term "sum-free".

Equations

• Complexity.Frontier.SumsetFree S K = ∀ (A B : Set G), (∀ a ∈ A, ∀ b ∈ B, a + b ∈ S) → A.ncard < K ∨ B.ncard < K

theorem Complexity.Frontier.SumsetFree.ncard_lt_of_stable {G : Type u_1} [Add G] {S H : Set G} {K : ℕ} (hS : SumsetFree S K) (hK : K ≤ S.ncard) (hstable : ∀ x ∈ S, ∀ y ∈ H, x + y ∈ S) : H.ncard < K

A large sumset-free set cannot be invariant under a large set of translations. For a function of a linear image, this bounds the size of the image map's kernel.

theorem Complexity.Frontier.SumsetDisperser.sumsetFree {ι : Type u_3} {U : Type u_4} [Add U] {f : (ι → U) → Bool} {K : ℕ} (hf : SumsetDisperser f K) (b : Bool) : SumsetFree {x : ι → U | f x = b} K

structure Complexity.Frontier.AdditiveSweep {G : Type u_1} [AddMonoid G] (S : Set G) (M : Type u_3) : Type (max u_1 u_3)

Splicing by addition of prefix and suffix contributions. The input itself is an element of the additive monoid; its coordinates need not be revealed separately.

• length : ℕ

  The number of steps.

• past : ℕ → G → G

  The contribution of the steps before t.

• future : ℕ → G → G

  The contribution of the steps from t on.

• emit : ℕ → G → G

  The label emitted at step t.

• message : ℕ → G → M

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

• past_zero (x : G) : x ∈ S → self.past 0 x = 0
• past_length (x : G) : x ∈ S → self.past self.length x = x
• message_length (x : G) : x ∈ S → ∀ y ∈ S, self.message self.length x = self.message self.length y
• reconstruct (t : ℕ) (x : G) : x ∈ S → self.past t x + self.future t x = x
• step (t : ℕ) (x : G) : x ∈ S → self.past (t + 1) x = self.past t x + self.emit t x
• splice (t : ℕ) (x : G) : x ∈ S → ∀ y ∈ S, self.message t x = self.message t y → self.past t x + self.future t y ∈ S

def Complexity.Frontier.AdditiveSweep.peers {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) (t : ℕ) (x : G) : Set G

The inputs of S sending the same message at time t as x.

Equations

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

def Complexity.Frontier.AdditiveSweep.pastSide {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) (t : ℕ) (x : G) : Set G

The past contributions of the peers of x at time t.

Equations

• P.pastSide t x = P.past t '' P.peers t x

def Complexity.Frontier.AdditiveSweep.futureSide {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) (t : ℕ) (x : G) : Set G

The future contributions of the peers of x at time t.

Equations

• P.futureSide t x = P.future t '' P.peers t x

def Complexity.Frontier.AdditiveSweep.transition {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) (t : ℕ) (x : G) : M × M × G

The step from time t: the old message, the new message, and the emitted label.

Equations

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

noncomputable def Complexity.Frontier.AdditiveSweep.transitionCount {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) : ℕ

The number of distinct transitions realized by S, summed over all steps.

Equations

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

theorem Complexity.Frontier.AdditiveSweep.transitionCount_le_codes {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) [Finite G] {D : ℕ → Type u_3} (code : (t : ℕ) → G → D t) (C : (t : ℕ) → Set (D t)) (hC : ∀ t < P.length, (C t).Finite) (hmem : ∀ t < P.length, ∀ x ∈ S, code t x ∈ C t) (hdet : ∀ t < P.length, ∀ x ∈ S, ∀ y ∈ S, code t x = code t y → P.transition t x = P.transition t y) : P.transitionCount ≤ ∑ t ∈ Finset.range P.length, (C t).ncard

Any finite encoding that determines the old state, new state, and emitted label can replace the raw transition count. In particular, only one old syndrome is needed when the new syndrome is determined by the current read value.

theorem Complexity.Frontier.AdditiveSweep.pastSide_lt_or_futureSide_lt {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) {K : ℕ} (hS : SumsetFree S K) (t : ℕ) (x : G) : (P.pastSide t x).ncard < K ∨ (P.futureSide t x).ncard < K

theorem Complexity.Frontier.AdditiveSweep.ncard_pastSide_zero_le {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) [Finite G] (x : G) : (P.pastSide 0 x).ncard ≤ 1

theorem Complexity.Frontier.AdditiveSweep.ncard_pastSide_length {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) {x : G} (hx : x ∈ S) : (P.pastSide P.length x).ncard = S.ncard

noncomputable def Complexity.Frontier.AdditiveSweep.chargeTime {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) (K : ℕ) (x : G) : ℕ

The first time at which the past contributions of the peers of x number at least K.

Equations

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

theorem Complexity.Frontier.AdditiveSweep.ncard_le {G : Type u_1} {M : Type u_2} [AddMonoid G] {S : Set G} (P : AdditiveSweep S M) [Finite G] {K : ℕ} (hS : SumsetFree S K) (hK1 : 1 < K) (hK : K ≤ S.ncard) : S.ncard ≤ (K - 1) ^ 2 * P.transitionCount

Additive frontier bound. Dense sumset-free sets require almost as many transitions as elements, even when different paths can describe the same element.