Zero-Error Recovery under Deterministic Partial Views: Matroid Bounds and Verifiable Realizability

TL;DR

This paper investigates zero-error graph recovery from partial views, establishing matroid bounds and verifiable realizability conditions, with formal mechanization in Lean 4.

Contribution

It introduces matroid-based bounds and verifiable criteria for realizability in zero-error graph recovery under partial views, extending to formal proof verification.

Findings

Polynomial-time upper bounds on confusability and capacity for affine state families.

Exact characterization of realizable confusability relations as upward-closed families.

Host architectures enabling verifiable rate-1 realizability with zero-delay synchronization.

Abstract

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.