theorem CommunicationComplexity.Deterministic.Protocol.theorem_1_7_experiment {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : ∃ (q : Protocol X Y α), q.run = p.run ∧ 3 ^ q.complexity ≤ 2 ^ q.complexity * p.numLeaves ^ 2

Balanced simulation theorem (R&Y-style): every deterministic protocol can be simulated by another protocol with the same behavior and complexity obeying 3^c ≤ 2^c * (#leaves)^2.