We introduce the zero-incoherence capacity for interactive multi-location encoding systems: the maximum encoding rate that guarantees exactly zero probability of disagreement among replicated encodings. Our main information-theoretic results are compact and self-contained: an exact capacity theorem ($C_0=1$), a tight side-information lower bound for resolution ($\geq\log_2 k$ bits for $k$-way incoherence), and a rate--complexity separation (modification cost $O(1)$ at capacity vs $Ω(n)$ above). The paper frames encoding locations as terminals in a multi-terminal source-coding model. Derivation (automatic deterministic dependence) is interpreted as perfect correlation that reduces effective rate; only complete derivation (one independent source) achieves zero incoherence. We give concise achievability and converse proofs in IT style, formalize the confusability/incoherence graph connection, and present an explicit mutual-information argument for the side-information bound. Theoretical contributions are supplemented by constructive instantiations (programming-language patterns and a software case study). For TIT submission we move detailed language evaluation, extended code examples, and the full Lean proof corpus to supplementary material; the main text contains brief instantiations only. Core theorems (capacity, realizability, bounds) are machine-checked in Lean 4; entropy arguments apply standard Fano-inequality techniques.

翻译：本文引入交互式多位置编码系统的零非相干容量概念：即在编码副本间保证完全零分歧概率的最大编码速率。我们的主要信息论结果具有紧凑且自洽的特性：一个精确的容量定理（$C_0=1$）、关于分辨率的紧致边信息下界（$k$ 路非相干需 $\geq\log_2 k$ 比特），以及速率-复杂度分离现象（容量下修改代价为 $O(1)$，而超容量时需 $Ω(n)$）。本文将编码位置建模为多终端信源编码模型中的终端。推导过程（自动确定性依赖）被解释为能降低有效速率的完美相关性；仅当完全推导（单一独立信源）时方能实现零非相干性。我们以信息论风格给出简洁的可达性证明与逆定理证明，形式化混淆性/非相干图的关联性，并为边信息界提出显式的互信息论证。理论贡献辅以构造性实例（编程语言模式与软件案例研究）。为适应 TIT 投稿要求，详细的语言评估、扩展代码示例及完整 Lean 证明库已移至补充材料；正文仅保留简要实例。核心定理（容量、可实现性、界）均通过 Lean 4 进行机器验证；熵论证采用标准 Fano 不等式技术。