The red-blue pebble game: when the FFT graph can be pebbled at all

Support module of MiscMath.Computability.RedBluePebbleGame, where the results are stated and where the reader should start. Nothing here is a result on its own.

With three red pebbles the 2^k-point FFT graph can be computed level by level: load a vertex's two predecessors, compute it, store it, clear the red pebbles (Run.block), and finally delete the blue pebbles off the outputs (fft_hasCompleteCalculation). With fewer it cannot: the move that computes an output has its two predecessors red and places a third pebble (three_le_of_fft_hasCompleteCalculation). A computed pebble is placed, not slid from a predecessor; with sliding, two would do.

theorem MiscMath.Computability.RedBluePebbleGame.Run.deleteReds {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (B R : Finset V) : R.card ≤ S → Run E I S (R, B) 0 (∅, B)

Deleting red pebbles, one at a time, at no charge.

theorem MiscMath.Computability.RedBluePebbleGame.Run.deleteBlues {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (B Y : Finset V) : Y ⊆ B → Run E I S (∅, B) 0 (∅, B \ Y)

Deleting blue pebbles, one at a time, at no charge.

theorem MiscMath.Computability.RedBluePebbleGame.Run.block {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} {B : Finset V} {v p₁ p₂ : V} (hvI : v ∉ I) (hvB : v ∉ B) (hpred : ∀ (u : V), E u v → u = p₁ ∨ u = p₂) (hp₁ : p₁ ∈ B) (hp₂ : p₂ ∈ B) (h₁₂ : p₁ ≠ p₂) (hv₁ : v ≠ p₁) (hv₂ : v ≠ p₂) (hS : 3 ≤ S) : Run E I S (∅, B) 3 (∅, insert v B)

One block: from a configuration with no red pebbles, a vertex whose two (distinct) predecessors both hold blue pebbles is computed and stored at a charge of 3, leaving no red pebble behind.

theorem MiscMath.Computability.RedBluePebbleGame.fftEdge_preds {k : ℕ} (v : Fin (k + 1) × Fin (2 ^ k)) (hv : ↑v.1 ≠ 0) : ∃ (p₁ : Fin (k + 1) × Fin (2 ^ k)) (p₂ : Fin (k + 1) × Fin (2 ^ k)), p₁ ≠ p₂ ∧ fftEdge k p₁ v ∧ fftEdge k p₂ v ∧ ∀ (u : Fin (k + 1) × Fin (2 ^ k)), fftEdge k u v → u = p₁ ∨ u = p₂

In the FFT graph, a vertex off level 0 has exactly two predecessors, and they are distinct.

theorem MiscMath.Computability.RedBluePebbleGame.fftEdge.level {k : ℕ} {u v : Fin (k + 1) × Fin (2 ^ k)} (h : fftEdge k u v) : ↑v.1 = ↑u.1 + 1

The level of a predecessor, in the FFT graph.

theorem MiscMath.Computability.RedBluePebbleGame.fft_run_union {k S : ℕ} {I : Finset (Fin (k + 1) × Fin (2 ^ k))} (hI : ∀ (v : Fin (k + 1) × Fin (2 ^ k)), v ∈ I ↔ ↑v.1 = 0) (hS : 3 ≤ S) (X : Finset (Fin (k + 1) × Fin (2 ^ k))) : (∀ v ∈ X, ↑v.1 ≠ 0) → (∀ v ∈ X, ∀ (u : Fin (k + 1) × Fin (2 ^ k)), fftEdge k u v → u ∈ I ∨ u ∈ X) → ∃ (q : ℕ), Run (fftEdge k) I S (∅, I) q (∅, I ∪ X)

Every predecessor-closed set of non-inputs of the FFT graph can be computed and stored.

theorem MiscMath.Computability.RedBluePebbleGame.fft_hasCompleteCalculation {k S : ℕ} (hS : 3 ≤ S) : ∃ (q : ℕ), HasCompleteCalculation (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = Fin.last k} S q

The FFT graph has a complete calculation for every budget S ≥ 3, k = 0 included.

theorem MiscMath.Computability.RedBluePebbleGame.three_le_of_fft_hasCompleteCalculation {k S q : ℕ} (hk : 1 ≤ k) (h : HasCompleteCalculation (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = Fin.last k} S q) : 3 ≤ S

For k ≥ 1, every complete calculation of the FFT graph needs at least 3 red pebbles.