The "Harmony Lemma", as formulated by Sangiorgi & Walker, establishes the equivalence between the labelled transition semantics and the reduction semantics in the $\pi$-calculus. Despite being a widely known and accepted result for the standard $\pi$-calculus, this assertion has never been rigorously proven, formally or informally. Hence, its validity may not be immediately apparent when considering extensions of the $\pi$-calculus. Contributing to the second challenge of the Concurrent Calculi Formalization Benchmark -- a set of challenges tackling the main issues related to the mechanization of concurrent systems -- we present a formalization of this result for the fragment of the $\pi$-calculus examined in the Benchmark. Our formalization is implemented in Beluga and draws inspiration from the HOAS formalization of the LTS semantics popularized by Honsell et al. In passing, we introduce a couple of useful encoding techniques for handling telescopes and lexicographic induction.

翻译：Sangiorgi与Walker提出的"和谐引理"确立了π演算中标号转移语义与归约语义的等价性。尽管这一结论在标准π演算中被广泛认知与接受，但无论是通过形式化还是非形式化方法，该论断从未得到严格证明。因此，当考虑π演算的扩展体系时，其有效性可能并不显而易见。针对"并发演算形式化基准测试"的第二项挑战——该系列挑战旨在解决并发系统机械化相关核心问题——我们针对基准测试所考察的π演算片段，给出了该结论的形式化证明。我们的形式化工作基于Beluga实现，并受到Honsell等人推广的LTS语义高阶抽象语法形式化方法的启发。在此过程中，我们引入了若干处理望远镜结构与字典序归纳的有效编码技术。