Zero-error recovery under deterministic partial views is graph recovery for the induced confusability relation. A finite family of coordinate-subset observations determines a graph on latent states; $T$-ary exact recovery is graph $T$-colorability, block composition is strong powering, and asymptotic recoverability is Shannon capacity. Coordinate structure gives tractable certificates inside the graph semantics. For affine realized state families with explicit linear presentations, restricted coordinate ranks form a representable matroid certificate giving polynomial-time upper bounds on one-shot confusability and asymptotic capacity, with rank additivity matching direct-sum block composition. In the full tuple-space coordinate model, the realizable confusability relations are exactly the upward-closed coordinate-agreement families. Transitive confusability is equivalent to intersection closure of the generated agreement family, yielding a cluster graph whose capacity is determined by connected components. Host-level realizability determines when the latent state family is canonical. Verifiable rate-$1$ realizability for structural facts holds if and only if the host provides zero-delay synchronization and structural side-information; eleven representative host architectures instantiate the criterion. The same clique-size bit-budget bound governs both the graph-level and host-level layers. All cited results are mechanized in Lean 4 against a shared formalization library.
翻译:在确定性部分观测下的零误差恢复是针对诱导混淆关系进行的图恢复。一个由坐标子集观测构成的有限族决定了潜在状态上的图;$T$元精确恢复对应图的$T$可着色性,块组合对应强幂运算,渐近可恢复性对应香农容量。坐标结构在图语义内部提供了可处理的判定依据。对于具有显式线性表示的仿射实现状态族,受限坐标秩构成一个可表示的拟阵判定依据,可在多项式时间内给出一次性混淆性与渐近容量的上界,其秩可加性满足直接和块组合。在全元组空间坐标模型中,可实现的混淆关系恰好是上封闭的坐标一致族。传递性混淆等价于生成的一致族的交闭性,从而产生一个聚类图,其容量由连通分量决定。宿主层可实现性决定了潜在状态族何时为典范形式。结构事实的可验证率$1$可实现性成立当且仅当宿主提供零延迟同步与结构侧信息;十一种代表性宿主架构实例化了该准则。同一团规模比特预算界限同时支配图层级与宿主层级。所有引用的结果均在Lean 4中基于共享形式化库进行了机械化验证。