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 fixes 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 inter-fact and intra-fact layers share the same clique-size bit-budget bound. All cited results are mechanized in Lean 4 against a shared formalization library.
翻译:确定性局部视图下的零错误恢复是针对诱导混淆关系的图恢复问题。潜在状态上的一个有限族坐标子集观测值确定了一个图结构;$T$元精确恢复对应图$T$可着色性,块组合对应强幂运算,渐近可恢复性对应香农容量。坐标结构在图语义框架内给出了可处理的认证机制。对于具有显式线性表示的仿射实现状态族,受限坐标秩构成可表示拟阵认证机制,可提供单次混淆性和渐近容量的多项式时间上界,其秩可加性与直和块组合相匹配。在全元组空间坐标模型中,可实现混淆关系恰为向上封闭的坐标一致族。传递混淆性等价于生成一致族的交闭性,由此得到聚类图结构,其容量由连通分量决定。宿主层可实现性界定了潜在状态族为正则形式时的固定性条件。结构事实的可验证速率$1$可实现性成立当且仅当宿主提供零延迟同步与结构边信息,11种代表性宿主架构实例化了该准则。事实间层与事实内层共享相同的团规模比特预算界。所有引证结果均在Lean 4中基于共享形式化库完成了机械化验证。