pith. sign in

arxiv: 2602.23520 · v9 · pith:T47X4UDEnew · submitted 2026-02-26 · 💻 cs.IT · cs.PL· math.IT

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

Pith reviewed 2026-05-21 12:15 UTC · model grok-4.3

classification 💻 cs.IT cs.PLmath.IT
keywords zero-error recoverydeterministic partial viewsmatroid boundsconfusability graphsShannon capacitycoordinate observationsaffine presentationsrealizability
0
0 comments X

The pith

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 add

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that when latent states admit an explicit linear presentation over a finite field, the ranks of different coordinate subsets induce a representable matroid. This matroid acts as a certificate that supplies polynomial-time upper bounds on both the number of confusable states under one-shot partial views and the asymptotic rate at which reliable recovery remains possible. The same structure also characterizes exactly which confusability relations arise from coordinate observations and supplies verifiable conditions under which a host system can realize rate-one recovery. A reader would care because the results convert an intractable graph-coloring task into a computable rank problem whose additivity respects direct-sum block compositions.

Core claim

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

What carries the argument

Representable matroid induced by the rank function on restricted coordinate subsets in an explicit linear presentation of the state family

Load-bearing premise

The central bounds assume that the latent state family admits an explicit linear affine presentation over a finite field so that coordinate subsets induce a representable matroid whose rank function is computable and additive under direct sums.

What would settle it

An affine family in which the matroid rank bound is strictly larger than the true confusability number obtained by exhaustive graph coloring, or a direct-sum construction in which the ranks fail to add while the actual confusability does.

Figures

Figures reproduced from arXiv: 2602.23520 by Tristan Simas.

Figure 1
Figure 1. Figure 1: Two failure topologies. In (a), the observation provides no discrimination, [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper models zero-error recovery under deterministic partial views as graph recovery on the induced confusability graph, where T-ary exact recovery corresponds to T-colorability and asymptotic recoverability to Shannon capacity. For affine realized state families admitting explicit linear presentations over a finite field, it shows that restricted coordinate ranks induce a representable matroid whose rank function is polynomial-time computable and additive under direct sums, supplying explicit upper bounds on one-shot confusability and asymptotic capacity. The manuscript further characterizes realizable confusability relations as upward-closed coordinate-agreement families in the full tuple-space model, equates transitive confusability with intersection closure, and gives a verifiable rate-1 realizability criterion for host architectures based on zero-delay synchronization and structural side-information. All cited results, including matroid axioms, rank additivity, and capacity bounds, are stated to be mechanized in Lean 4 against a shared library.

Significance. If the central claims hold, the work supplies the first polynomial-time, matroid-based certificates for zero-error capacity bounds that are explicitly tied to linear state presentations and that respect direct-sum block composition. The machine-checked Lean 4 formalization of the matroid axioms, rank additivity, and bound derivations constitutes a concrete strength, removing derivation gaps inside the stated affine scope and enabling verifiable, parameter-free upper bounds rather than fitted estimates. This combination of algebraic structure and formal verification is potentially significant for information-theoretic analyses of partial-observation systems where explicit linear models are available.

major comments (1)
  1. [§4, Theorem 4.3] §4, Theorem 4.3: the claim that the restricted coordinate rank function is additive under direct sums and therefore matches block composition capacity is load-bearing for the asymptotic bound; while the Lean mechanization is cited, the manuscript should explicitly state the precise matroid axiom (e.g., the rank-submodularity or augmentation axiom) that is invoked to obtain additivity from the linear presentation, so that readers can verify the step without consulting the formal library.
minor comments (3)
  1. [Abstract, §2] Abstract and §2: the phrase 'restricted coordinate ranks form a representable matroid certificate' is used before the linear presentation is defined; a forward reference or brief inline definition of the coordinate-subset rank function would improve readability.
  2. [§5.2] §5.2: the eleven host architectures are listed but only three are given explicit linear presentations; adding a short table summarizing which architectures satisfy the zero-delay synchronization condition would make the realizability criterion easier to apply.
  3. [Notation] Notation: the symbol for the confusability graph is introduced in two places with slightly different subscripts; consistent use of a single symbol (e.g., G_𝒮) throughout would reduce ambiguity.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive comment on Theorem 4.3. We agree that an explicit reference to the relevant matroid axiom will improve accessibility and will revise the manuscript to include it.

read point-by-point responses
  1. Referee: [§4, Theorem 4.3] §4, Theorem 4.3: the claim that the restricted coordinate rank function is additive under direct sums and therefore matches block composition capacity is load-bearing for the asymptotic bound; while the Lean mechanization is cited, the manuscript should explicitly state the precise matroid axiom (e.g., the rank-submodularity or augmentation axiom) that is invoked to obtain additivity from the linear presentation, so that readers can verify the step without consulting the formal library.

    Authors: We agree that the manuscript would benefit from an explicit statement of the axiom. The restricted coordinate rank is the rank function of the representable matroid arising from the linear presentation over the finite field. Additivity under direct sums follows directly from the submodularity axiom of matroids (rank(A ∪ B) + rank(A ∩ B) ≤ rank(A) + rank(B)), which holds with equality for disjoint ground sets in the direct-sum construction because the underlying vector-space dimensions add when the coordinate subspaces are independent. In the revised manuscript we will insert a single sentence in the proof of Theorem 4.3 stating that the additivity is obtained from the submodularity property of the representable matroid induced by the linear dependencies; this makes the step verifiable from the text alone. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained via explicit linear structure and Lean mechanization

full rationale

The central bounds derive from the rank function of the representable matroid induced directly by the explicit linear (affine) presentation over a finite field, with additivity under direct sums following from standard matroid properties rather than any fit to capacity. The manuscript explicitly scopes the result to state families admitting such presentations and states that all cited results—including matroid axioms, rank additivity, and capacity derivations—have been mechanized in Lean 4 against a shared library. This machine-checked status constitutes independent external verification, so no load-bearing step reduces by construction to a fitted parameter, self-citation chain, or renamed input. The derivation remains self-contained within the stated algebraic scope.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard matroid axioms and the definition of representable matroids over finite fields; no free parameters are introduced and no new entities are postulated. The linear presentation of the state family is treated as an explicit modeling choice rather than an invented object.

axioms (2)
  • domain assumption Coordinate subsets of an affine space over a finite field induce a representable matroid whose rank function is additive under direct sums.
    Invoked when the paper states that restricted coordinate ranks form a representable matroid certificate.
  • standard math Deterministic partial views induce a confusability graph whose T-colorability equals exact T-ary recovery.
    Standard translation from zero-error information theory to graph coloring.

pith-pipeline@v0.9.0 · 5753 in / 1599 out tokens · 32024 ms · 2026-05-21T12:15:24.487266+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

56 extracted references · 56 canonical work pages

  1. [1]

    C. E. Shannon, Zero-Error capacity of a noisy channel, IRE Transactions on Information Theory 2 (3) (1956) 8–19.doi:10.1109/TIT.1956. 1056798

  2. [2]

    Lovász, On the Shannon capacity of a graph, IEEE Transactions on Information Theory 25 (1) (1979) 1–7.doi:10.1109/TIT.1979

    L. Lovász, On the Shannon capacity of a graph, IEEE Transactions on Information Theory 25 (1) (1979) 1–7.doi:10.1109/TIT.1979. 1055985

  3. [3]

    N. Alon, E. Lubetzky, The Shannon capacity of a graph and the in- dependence numbers of its powers, IEEE Transactions on Information Theory 52 (5) (2006) 2172–2176.doi:10.1109/TIT.2006.872856

  4. [4]

    de Boer, P

    D. de Boer, P. Buys, J. Zuiddam, The asymptotic spectrum distance, graph limits, and the Shannon capacity (2024).arXiv:2404.16763, doi:10.48550/arXiv.2404.16763

  5. [5]

    Grötschel, L

    M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (2) (1981) 169–197.doi:10.1007/BF02579276

  6. [6]

    Gilbert, N

    S. Gilbert, N. Lynch, Brewer’s conjecture and the feasibility of con- sistent, available, partition-tolerant web services, ACM SIGACT News 33 (2) (2002) 51–59, formal proof of CAP theorem.doi:10.1145/ 564585.564601

  7. [7]

    Herlihy, J

    M. Herlihy, J. M. Wing, Linearizability: A correctness condition for concurrent objects, in: Proceedings of the 11th ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, 1990, pp. 139–150. doi:10.1145/214548.214562

  8. [8]

    K. V. Rashmi, N. B. Shah, K. Ramchandran, D. Gu, Multi-version coding: An information-theoretic perspective of consistent distributed storage, IEEE Transactions on Information Theory 63 (6) (2017) 4111– 4128.doi:10.1109/TIT.2017.2695219

  9. [9]

    The lean 4 theorem prover and programming language

    L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in: Automated Deduction – CADE 28, Springer, 2021, pp. 625–635.doi:10.1007/978-3-030-79876-5_37. 33

  10. [10]

    367–381.doi:10.1145/3372885

    The mathlib Community, The Lean mathematical library, in: Proceed- ings of the 9th ACM SIGPLAN International Conference on Certi- fied Programs and Proofs, 2020, pp. 367–381.doi:10.1145/3372885. 3373824

  11. [11]

    R. M. Fano, Transmission of Information: A Statistical Theory of Com- munications, MIT Press, Cambridge, MA, 1961

  12. [12]

    H. S. Witsenhausen, A. D. Wyner, A conditional entropy bound for a pair of discrete random variables, IEEE Transactions on Information Theory 21 (5) (1975) 493–501

  13. [13]

    T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd Edi- tion, Wiley-Interscience, 2006.doi:10.1002/047174882X

  14. [14]

    B. G. Kelly, A. B. Wagner, Improved source coding exponents via Witsenhausen’s rate, IEEE Transactions on Information Theory 57 (9) (2011) 5615–5633.doi:10.1109/TIT.2011.2162178

  15. [15]

    D. B. West, Introduction to Graph Theory, 2nd Edition, Prentice Hall, 2001

  16. [16]

    Diestel, Graph Theory, 5th Edition, Springer, 2017.doi:10.1007/ 978-3-662-53622-3

    R. Diestel, Graph Theory, 5th Edition, Springer, 2017.doi:10.1007/ 978-3-662-53622-3

  17. [17]

    Oxley, Matroid Theory, 2nd Edition, Oxford University Press, 2011

    J. Oxley, Matroid Theory, 2nd Edition, Oxford University Press, 2011

  18. [18]

    D. J. A. Welsh, Matroid Theory, Academic Press, 1976

  19. [19]

    Recski, Matroid Theory and Its Applications in Electric Network Theory and in Statics, Springer, 1989

    A. Recski, Matroid Theory and Its Applications in Electric Network Theory and in Statics, Springer, 1989

  20. [20]

    M. Fekete, Über die Verteilung der Wurzeln bei gewissen algebraischen Gleichungen mit ganzzahligen Koeffizienten, Mathematische Zeitschrift 17 (1) (1923) 228–249.doi:10.1007/BF01204614

  21. [21]

    Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Vol

    A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Vol. A, Springer, 2003.doi:10.1007/978-3-642-27448-2

  22. [22]

    25, 1978, pp

    W.H.Haemers, AnupperboundfortheShannoncapacityofagraph, in: Algebraic Methods in Graph Theory, Colloquia Mathematica Societatis János Bolyai, Vol. 25, 1978, pp. 267–272. 34

  23. [23]

    Zuiddam, The asymptotic spectrum of graphs and the Shannon ca- pacity, Combinatorica 39 (5) (2019) 1173–1184.doi:10.1007/s00493- 019-3992-5

    J. Zuiddam, The asymptotic spectrum of graphs and the Shannon ca- pacity, Combinatorica 39 (5) (2019) 1173–1184.doi:10.1007/s00493- 019-3992-5

  24. [24]

    Körner, Coding of an information source having ambiguous alphabet and the entropy of graphs, Transactions of the 6th Prague Conference on Information Theory (1973) 411–425

    J. Körner, Coding of an information source having ambiguous alphabet and the entropy of graphs, Transactions of the 6th Prague Conference on Information Theory (1973) 411–425

  25. [25]

    Körner, A

    J. Körner, A. Orlitsky, Zero-Error information theory, IEEE Transac- tions on Information Theory 44 (6) (1998) 2207–2229.doi:10.1109/ 18.720537

  26. [26]

    H. S. Witsenhausen, The Zero-Error side information problem and chro- matic numbers, IEEE Transactions on Information Theory 22 (5) (1976) 592–593

  27. [27]

    Slepian, J

    D. Slepian, J. K. Wolf, Noiseless coding of correlated information sources, IEEE Transactions on Information Theory 19 (4) (1973) 471– 480.doi:10.1109/TIT.1973.1055037

  28. [28]

    Orlitsky, J

    A. Orlitsky, J. R. Roche, Coding for computing, IEEE Transactions on Information Theory 47 (3) (2001) 903–917.doi:10.1109/18.915643

  29. [29]

    N. Alon, A. Orlitsky, Source coding and graph entropies, IEEE Trans- actions on Information Theory 42 (5) (1996) 1329–1339.doi:10.1109/ 18.532875

  30. [30]

    Doshi, D

    V. Doshi, D. Shah, M. Médard, M. Effros, Functional compression through graph coloring, IEEE Transactions on Information Theory 56 (8) (2010) 3901–3917.doi:10.1109/TIT.2010.2050835

  31. [31]

    Simonyi, Graph entropy: A survey, in: Combinatorial Optimization, Vol

    G. Simonyi, Graph entropy: A survey, in: Combinatorial Optimization, Vol. 20 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, Providence, Rhode Island, 1995, pp. 399–441.doi:10.1090/dimacs/020/08

  32. [32]

    Guang, R.Zhang, Zero-Errordistributed compression ofbinary arith- metic sum, IEEE Transactions on Information Theory 70 (5) (2024) 3100–3117.doi:10.1109/TIT.2023.3319976

    X. Guang, R.Zhang, Zero-Errordistributed compression ofbinary arith- metic sum, IEEE Transactions on Information Theory 70 (5) (2024) 3100–3117.doi:10.1109/TIT.2023.3319976. 35

  33. [33]

    Y. Liu, L. Ong, S. Johnson, J. Kliewer, P. Sadeghi, P. L. Yeoh, Informa- tion leakage in Zero-Error source coding: A Graph-Theoretic perspec- tive, in: 2021 IEEE International Symposium on Information Theory (ISIT), 2021, pp. 2590–2595.doi:10.1109/ISIT45174.2021.9517778

  34. [34]

    Kiczales, J

    G. Kiczales, J. des Rivières, D. G. Bobrow, The Art of the Metaobject Protocol, MIT Press, 1991

  35. [35]

    B. C. Smith, Reflection and semantics in Lisp, in: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of program- ming languages, 1984, pp. 23–35.doi:10.1145/800017.800513

  36. [36]

    Communications of the ACM 52(7), pp

    X. Leroy, Formal verification of a realistic compiler, Communications of the ACM 52 (7) (2009) 107–115.doi:10.1145/1538788.1538814

  37. [37]

    T. Simas, Exact recovery under deterministic partial views: Confus- ability graphs, strong powers, and capacity, Zenodo, supplementary Lean 4 formalization, manuscript PDF, and source bundle. (2026). doi:10.5281/zenodo.19354075. URLhttps://doi.org/10.5281/zenodo.19354075

  38. [38]

    Teich, R

    M. Teich, R. Hettinger, Y. Selivanov, PEP 487 – simpler cus- tomisation of class creation, Python Enhancement Proposals, online: peps.python.org/pep-0487/ (2016)

  39. [39]

    Available: docs.python.org/3/reference/datamodel.html (2025)

    PythonSoftwareFoundation, Pythondatamodel, Python3Documenta- tion, [Online]. Available: docs.python.org/3/reference/datamodel.html (2025)

  40. [40]

    Available: www.postgresql.org/docs/current/rules-materializedviews.html (2025)

    The PostgreSQL Global Development Group, Material- ized views, PostgreSQL documentation, [Online]. Available: www.postgresql.org/docs/current/rules-materializedviews.html (2025)

  41. [41]

    Available: www.postgresql.org/docs/current/view-pg-matviews.html (2025)

    The PostgreSQL Global Development Group, pg_matviews, PostgreSQL system catalog documentation, [Online]. Available: www.postgresql.org/docs/current/view-pg-matviews.html (2025)

  42. [42]

    The Rust Team, The Rust reference, Language reference, online: doc.rust-lang.org/reference/ (2024). 36

  43. [43]

    Available: www.typescriptlang.org/docs/handbook/decorators.html (2025)

    Microsoft, Decorators, TypeScript Handbook, [Online]. Available: www.typescriptlang.org/docs/handbook/decorators.html (2025)

  44. [44]

    Available: developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Classes (2025)

    MDN Web Docs, Classes, JavaScript reference, [Online]. Available: developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Classes (2025)

  45. [45]

    Gosling, B

    J. Gosling, B. Joy, G. Steele, G. Bracha, A. Buckley, D. Smith, G. Bier- man, The Java Language Specification, Java SE 17 Edition, Oracle America, Inc., 2021, online: docs.oracle.com/javase/specs/

  46. [46]

    TheGoAuthors, TheGoprogramminglanguagespecification, Language specification, online: go.dev/ref/spec (2024)

  47. [47]

    Available: docs.npmjs.com/cli/v8/configuring-npm/package-lock-json/ (2026)

    npm, Inc., package-lock.json, npm CLI documentation, [Online]. Available: docs.npmjs.com/cli/v8/configuring-npm/package-lock-json/ (2026)

  48. [48]

    Available: docs.npmjs.com/cli/v7/commands/npm-explain/ (2026)

    npm, Inc., npm explain, npm CLI documentation, [Online]. Available: docs.npmjs.com/cli/v7/commands/npm-explain/ (2026)

  49. [49]

    Available: docs.npmjs.com/cli/v7/commands/npm-ls/ (2026)

    npm, Inc., npm ls, npm CLI documentation, [Online]. Available: docs.npmjs.com/cli/v7/commands/npm-ls/ (2026)

  50. [50]

    The Rust Project Developers, Cargo.toml vs cargo.lock, The Cargo Book, [Online].Available: doc.rust-lang.org/cargo/guide/cargo-toml-vs- cargo-lock.html (2026)

  51. [51]

    Available: doc.rust-lang.org/cargo/commands/cargo-tree.html (2026)

    The Rust Project Developers, cargo-tree, The Cargo Book, [Online]. Available: doc.rust-lang.org/cargo/commands/cargo-tree.html (2026)

  52. [52]

    Available: doc.rust-lang.org/cargo/commands/cargo- metadata.html (2026)

    The Rust Project Developers, cargo-metadata, The Cargo Book, [Online]. Available: doc.rust-lang.org/cargo/commands/cargo- metadata.html (2026)

  53. [53]

    Available: python-poetry.org/docs/cli/ (2026)

    Poetry Contributors, CLI, Poetry documentation, [Online]. Available: python-poetry.org/docs/cli/ (2026)

  54. [54]

    Avail- able: pnpm.io/cli/install (2026)

    pnpm Contributors, pnpm install, pnpm documentation, [Online]. Avail- able: pnpm.io/cli/install (2026). 37

  55. [55]

    Avail- able: pnpm.io/cli/why (2026)

    pnpm Contributors, pnpm why, pnpm documentation, [Online]. Avail- able: pnpm.io/cli/why (2026)

  56. [56]

    Avail- able: pnpm.io/cli/list (2026)

    pnpm Contributors, pnpm list, pnpm documentation, [Online]. Avail- able: pnpm.io/cli/list (2026). A. Boundary and Realizability Proofs A.1. Derived Views and the Unit-Rate Boundary An encoding system hasunit independent ratewhen DOF(C, F) = 1. By Corollary 2.7, this is exactly the regime in which every reachable state remains coherent, and any rate above1...