Self-composition and the product blocks

Section 14 of bs_lambda.txt composes the seed function with itself. For f : Input W → Bool and g : Input V → Bool the block composition comp f g takes one V-indexed input for each coordinate of W, applies g to each of them and feeds the resulting W-indexed bit string to f.

iterFun f m is the m-fold self-composition F_m = f^{∘ m}, whose coordinate set is the iterated product IterCoord V m ≃ V^m. The Cartesian-product blocks B_{i_1} × ⋯ × B_{i_m} are iterBlock blk m, indexed by IterCoord ι m ≃ ι^m; they are pairwise disjoint sensitive blocks of F_m at the all-zero input, whence bs (F_m) ≥ k^m (card_pow_le_bs_iterFun).

The spectral half of Section 14, the ABKRT multiplicativity theorem lambda (f ∘ g) = lambda f * lambda g, is imported by the document but proved here, in BSLambda/Spectral/Multiplicative.lean.

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

def BSLambda.comp {W : Type u_1} {V : Type u_2} (f : Input W → Bool) (g : Input V → Bool) : Input (W × V) → Bool

Block composition f ∘ g: N disjoint M-bit inputs, g applied to each, the N resulting bits fed to f (Section 14 of bs_lambda.txt).

Equations

• BSLambda.comp f g x = f fun (w : W) => g fun (v : V) => x (w, v)

theorem BSLambda.comp_apply {W : Type u_1} {V : Type u_2} (f : Input W → Bool) (g : Input V → Bool) (x : Input (W × V)) : comp f g x = f fun (w : W) => g fun (v : V) => x (w, v)

The defining equation of comp.

def BSLambda.IterCoord (V : Type u) : ℕ → Type u

The m-fold power V^m, realised as an iterated binary product so that IterCoord V (m + 1) = V × IterCoord V m holds definitionally (Section 14). It is used both as the coordinate set of iterFun f m and, at V := ι, as the index set of the product blocks iterBlock blk m.

Equations

• BSLambda.IterCoord V 0 = PUnit.{?u.1 + 1}
• BSLambda.IterCoord V m.succ = (V × BSLambda.IterCoord V m)

@[instance_reducible]

instance BSLambda.instFintypeIterCoord {V : Type u_1} [Fintype V] (m : ℕ) : Fintype (IterCoord V m)

IterCoord V m is a finite type (Section 14).

Equations

• BSLambda.instFintypeIterCoord 0 = { elems := BSLambda.instFintypeIterCoord._aux_1, complete := ⋯ }
• BSLambda.instFintypeIterCoord m.succ = { elems := BSLambda.instFintypeIterCoord._aux_4 m (BSLambda.instFintypeIterCoord m), complete := ⋯ }

@[instance_reducible]

instance BSLambda.instDecidableEqIterCoord {V : Type u_1} [DecidableEq V] (m : ℕ) : DecidableEq (IterCoord V m)

IterCoord V m has decidable equality (Section 14).

Equations

• BSLambda.instDecidableEqIterCoord 0 = BSLambda.instDecidableEqIterCoord._aux_1
• BSLambda.instDecidableEqIterCoord m.succ = BSLambda.instDecidableEqIterCoord._aux_3 m (BSLambda.instDecidableEqIterCoord m)

theorem BSLambda.card_iterCoord (V : Type u_1) [Fintype V] (m : ℕ) : Fintype.card (IterCoord V m) = Fintype.card V ^ m

There are exactly k^m tuples, where k = #V (Section 14).

def BSLambda.iterBlock {V : Type u_1} {ι : Type u_2} [DecidableEq V] (blk : ι → Finset V) (m : ℕ) : IterCoord ι m → Finset (IterCoord V m)

The Cartesian-product block B_{i_1} × ⋯ × B_{i_m} (Section 14).

Equations

• BSLambda.iterBlock blk 0 = fun (x : BSLambda.IterCoord ι 0) => Finset.univ
• BSLambda.iterBlock blk m.succ = fun (t : BSLambda.IterCoord ι (m + 1)) => blk t.1 ×ˢ BSLambda.iterBlock blk m t.2

@[simp]

theorem BSLambda.iterBlock_zero {V : Type u_1} {ι : Type u_2} [DecidableEq V] (blk : ι → Finset V) (t : IterCoord ι 0) : iterBlock blk 0 t = Finset.univ

There is a single degenerate 0-fold product block, the whole (one-point) cube.

theorem BSLambda.iterBlock_succ {V : Type u_1} {ι : Type u_2} [DecidableEq V] (blk : ι → Finset V) (m : ℕ) (t : IterCoord ι (m + 1)) : iterBlock blk (m + 1) t = blk t.1 ×ˢ iterBlock blk m t.2

The recursion equation of iterBlock: the first index picks the outer factor.

def BSLambda.iterFun {V : Type u_1} (f : Input V → Bool) (m : ℕ) : Input (IterCoord V m) → Bool

F_m = f^{∘ m}, the m-fold self-composition (Section 14). F_0 is the one-bit identity function.

Equations

• BSLambda.iterFun f 0 = fun (x : BSLambda.Input (BSLambda.IterCoord V 0)) => x PUnit.unit
• BSLambda.iterFun f m.succ = BSLambda.comp f (BSLambda.iterFun f m)

@[simp]

theorem BSLambda.iterFun_zero {V : Type u_1} (f : Input V → Bool) (x : Input (IterCoord V 0)) : iterFun f 0 x = x PUnit.unit

F_0 is the one-bit identity function.

theorem BSLambda.iterFun_succ {V : Type u_1} (f : Input V → Bool) (m : ℕ) : iterFun f (m + 1) = comp f (iterFun f m)

The recursion equation of iterFun: F_{m+1} = f ∘ F_m.

theorem BSLambda.flipSet_zeroInput_product_slice {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] (A : Finset V) (B : Finset W) (v : V) : (fun (w : W) => flipSet (zeroInput (V × W)) (A ×ˢ B) (v, w)) = if v ∈ A then flipSet (zeroInput W) B else zeroInput W

Slicing the all-zero input flipped on a product block A ×ˢ B: the v-slice is the flip of B when v ∈ A, and the all-zero input otherwise (Section 14).

theorem BSLambda.comp_flipSet_product {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {f : Input V → Bool} {g : Input W → Bool} {A : Finset V} {B : Finset W} (hzero : g (zeroInput W) = false) (hflip : g (flipSet (zeroInput W) B) = true) : comp f g (flipSet (zeroInput (V × W)) (A ×ˢ B)) = f (flipSet (zeroInput V) A)

The key composition step of Section 14: if the inner function g is flipped from 0 to 1 by the block B, then comp f g on the product block A ×ˢ B feeds f exactly the all-zero input flipped on A.

theorem BSLambda.iterFun_zeroInput {V : Type u_1} {f : Input V → Bool} (hzero : f (zeroInput V) = false) (m : ℕ) : iterFun f m (zeroInput (IterCoord V m)) = false

The all-zero input of F_m evaluates to 0 whenever the seed does (Section 14).

theorem BSLambda.iterFun_flipSet_iterBlock {V : Type u_1} {ι : Type u_2} [DecidableEq V] {f : Input V → Bool} {blk : ι → Finset V} (hzero : f (zeroInput V) = false) (hflip : ∀ (i : ι), f (flipSet (zeroInput V) (blk i)) = true) (m : ℕ) (t : IterCoord ι m) : iterFun f m (flipSet (zeroInput (IterCoord V m)) (iterBlock blk m t)) = true

Flipping the Cartesian-product block B_{i_1} × ⋯ × B_{i_m} at the all-zero input turns the value of F_m from 0 to 1 (Section 14).

theorem BSLambda.iterBlock_nonempty {V : Type u_1} {ι : Type u_2} [DecidableEq V] {blk : ι → Finset V} (hne : ∀ (i : ι), (blk i).Nonempty) (m : ℕ) (t : IterCoord ι m) : (iterBlock blk m t).Nonempty

Cartesian products of nonempty blocks are nonempty (Section 14).

theorem BSLambda.iterBlock_disjoint {V : Type u_1} {ι : Type u_2} [DecidableEq V] {blk : ι → Finset V} (hdisj : Pairwise (Function.onFun Disjoint blk)) (m : ℕ) : Pairwise (Function.onFun Disjoint (iterBlock blk m))

Distinct index tuples give disjoint Cartesian-product blocks (Section 14).

theorem BSLambda.card_pow_le_bs_iterFun {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] {f : Input V → Bool} {blk : ι → Finset V} (hzero : f (zeroInput V) = false) (hflip : ∀ (i : ι), f (flipSet (zeroInput V) (blk i)) = true) (hne : ∀ (i : ι), (blk i).Nonempty) (hdisj : Pairwise (Function.onFun Disjoint blk)) (m : ℕ) : Fintype.card ι ^ m ≤ bs (iterFun f m)

Section 14: the k^m Cartesian-product blocks are pairwise disjoint sensitive blocks of F_m at the all-zero input, so bs(F_m) ≥ k^m.