The Number-On-the-Forehead model

structure NOF.Protocol (G : Type u_2) (d : ℕ) : Type u_2

• nextBit (i : ZMod d) : ({ j : ZMod d // j ≠ i } → G) → List Bool → Bool
• guess (i : ZMod d) : ({ j : ZMod d // j ≠ i } → G) → List Bool → Bool

def NOF.Protocol.broadcast {G : Type u_2} {d : ℕ} (P : Protocol G d) (x : ZMod d → G) : ℕ → List Bool

Equations

• P.broadcast x 0 = []
• P.broadcast x t.succ = P.nextBit (↑t) (NOF.forget (↑t) x) (P.broadcast x t) :: P.broadcast x t

@[simp]

theorem NOF.Protocol.broadcast_zero {G : Type u_2} {d : ℕ} (P : Protocol G d) (x : ZMod d → G) : P.broadcast x 0 = []

theorem NOF.Protocol.broadcast_succ {G : Type u_2} {d : ℕ} (P : Protocol G d) (x : ZMod d → G) (t : ℕ) : P.broadcast x (t + 1) = P.nextBit (↑t) (forget (↑t) x) (P.broadcast x t) :: P.broadcast x t

def NOF.Protocol.IsValid {G : Type u_2} {d : ℕ} (P : Protocol G d) (F : (ZMod d → G) → Bool) (t : ℕ) : Prop

Equations

• P.IsValid F t = ∀ (x : ZMod d → G) (i : ZMod d), P.guess i (NOF.forget i x) (P.broadcast x t) = F x

@[simp]

theorem NOF.Protocol.length_broadcast {G : Type u_2} {d : ℕ} (P : Protocol G d) (x : ZMod d → G) (t : ℕ) : (P.broadcast x t).length = t

noncomputable def NOF.Protocol.complexity {G : Type u_2} {d : ℕ} (P : Protocol G d) (F : (ZMod d → G) → Bool) : ℕ∞

Equations

• P.complexity F = ⨅ (t : ℕ), ⨅ (_ : P.IsValid F t), ↑t

@[simp]

theorem NOF.Protocol.le_complexity {G : Type u_2} {d : ℕ} {F : (ZMod d → G) → Bool} {P : Protocol G d} {t : ℕ} : ↑t ≤ P.complexity F ↔ ∀ (r : ℕ), P.IsValid F r → t ≤ r

noncomputable def NOF.funComplexity {G : Type u_2} {d : ℕ} (F : (ZMod d → G) → Bool) : ℕ∞

Equations

• NOF.funComplexity F = ⨅ (P : NOF.Protocol G d), P.complexity F

@[simp]

theorem NOF.le_funComplexity {G : Type u_2} {d : ℕ} {F : (ZMod d → G) → Bool} {t : ℕ} : ↑t ≤ funComplexity F ↔ ∀ (P : Protocol G d), ↑t ≤ P.complexity F

theorem NOF.IsForbiddenPatternWithTip.broadcast_eq {G : Type u_2} {d : ℕ} {P : Protocol G d} {a : ZMod d → ZMod d → G} {v : ZMod d → G} {B : List Bool} {t : ℕ} (hF : IsForbiddenPatternWithTip a v) (hB : ∀ (i : ZMod d), P.broadcast (a i) t = B) : P.broadcast v t = B