Coordinate-View Confusability Graphs and Matroid Rank Certificates
Tristan Simas
cs.IT
Feb 26, 2026 · v10
cs.PL
TL;DR
Core theorems on zero-incoherence capacity, realizability and rate-complexity bounds are machine-checked in Lean 4 (3378 lines, no sorry), released as supplementary material.
Abstract
A coordinate-view presentation specifies a large confusability graph by coordinates rather than by an edge list. The problem is to certify zero-error recovery and Shannon capacity from the succinct presentation, before the exponentially large graph is materialized. For affine presentations over $\mathbb F_q$, Gaussian elimination gives a polynomial-time rank upper certificate from $O(rd\log q+Ld)$ input bits for a graph with $q^r$ vertices. Exactness of that certificate is equivalent to positivity of a Grassmannian avoidance count $N_{t^*}$. Positivity of $N_k$ is NP-complete for every fixed $k$, already over $\mathbb F_2$, while the ambient-rank parameter gives a fixed-parameter algorithm. The rank-one reduction is parsimonious for $\#SAT$. For arbitrary $t$, the finite decoder for $N_t$ reads the signed rank profile of the represented forbidden-point matroid; the kernel-intersection lattice alone does not determine the count. On the positive side, kernel sections give the exact formula $Θ(G)=\logα(G)=\min_{S\in\mathcal V}t(S)\log q$, with a projection-equality matrix optimal for Haemers minrank. A finite-field blocking theorem gives exactness when $q\ge L$, and Reed-Solomon/MDS codes give exact all-$k$-view families beyond that regime. Full-tuple coordinate-view graphs also have a polynomial-time cofinal-antichain normal form; transitive confusability is exactly intersection closure.
Problem
The paper asks what encoding rate guarantees exactly zero probability of disagreement among replicated encodings of a fact stored at multiple locations under modification. It defines a zero-incoherence capacity by analogy with Shannon zero-error capacity.
Approach
Encoding systems are modeled with degrees of freedom (DOF), the number of independent locations for a fact. Achievability and converse theorems are proved, along with realizability conditions (causal propagation and provenance observability) and rate-complexity bounds. Side-information requirements are argued with confusability graphs and Fano-style bounds. Core theorem chains are mechanized in Lean 4, while entropy arguments are treated as explicit classical assumptions.
Results
The zero-incoherence capacity is C_0 = 1: DOF = 1 achieves zero incoherence and DOF > 1 does not. Resolving k-way incoherence requires at least log2 k bits of side information. The Lean development reports 3378 lines, 176 theorem/lemma statements and 0 sorry placeholders.
| Encoding Rate | Zero Incoherence? | Interpretation |
|---|
| DOF = 0 | N/A | Fact not encoded |
| DOF = 1 | Yes | Capacity-achieving |
| DOF > 1 | No | Above capacity |
Encoding rate vs. zero incoherence