{"id":"9b45a170-1206-4a47-94ff-e44b0fcded35","arxiv_id":"2603.06678","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A comprehensive survey plus new theorems systematically comparing PID redundancy measures and their axioms, with a Z3-checked map of property implications and incompatibilities.","lead":"This paper maps the mathematical landscape of partial information decomposition (PID), a method for splitting shared information into redundant, unique, and synergistic parts. It compiles a large comparison table of 19 PID measures against 20 properties and adds new theorems about which properties conflict.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Table 5's completeness claim is undermined: several entries rest on 'empirical tests' rather than the promised proof/counterexample, and Theorem 2 silently assumes (S0).","rationale":"The paper has genuine strengths: a broad systematization of PID measures and axioms, many explicit proofs in Appendix E.2, a Z3-based consistency check, and useful historical context. But the headline contribution is explicitly the systematic verification table, and the claim 'For all results not already known in the literature, we provide either a proof or a counterexample' is load-bearing. The appendix undercuts that claim by using 'empirical tests' as justification for several entries. Numerically checking a finite set of distributions may be evidence, but it is not the promised proof or counterexample, especially when no distribution is actually reported. This is not a disagreement with the consensus; it is a correctness-risk gap in the paper's own standard. The Theorem 2 issue is a second instance of the same pattern: a result presented as proved from stated hypotheses, but with an unstated symmetry assumption. Neither flaw is necessarily fatal — the entries may be correct and Theorem 2 may be repairable by adding (S0) — but both must be fixed before the map can be treated as a rigorous reference. Therefore the reader's CONDITIONAL verdict is appropriate, and I do not recommend changing it.","tokens_in":59209,"tokens_out":6277,"duration_ms":58611,"concrete_test":"Audit Appendix E.1 for every Table 5 entry whose justification contains 'empirical tests' or 'observed', and require each to be replaced by either an explicit probability distribution with computed values or an analytic proof. Start with I_CT '(AD) does not hold': instantiate Eq. (41) with two independent subsystems and evaluate both sides analytically; if the inequality is not demonstrated, the entry fails the §3.1 promise. The completeness claim stands only if every audited entry is formally supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim of §3.1 is that every non-known Table 5 entry is backed by a proof or an explicit counterexample. Appendix E.1 does not deliver this for a nontrivial set of entries. For example: I_IG '(TM) holds from empirical tests'; I_DEP '(S1) is violated as observed from empirical tests'; I_MES '(LP0) is violated, as synergy can be negative as seen from empirical tests'; I_CT '(AD) does not hold as observed from empirical tests'; I_CCS '(TM),(TC),(S1) are violated as observed from empirical tests'. No distribution or parameter values are supplied, and numerical observation is not a proof or a located counterexample. If any of these entries is wrong, the map is wrong, and the promised systematic verification is not delivered. In addition, Theorem 2 is stated with hypotheses (SR),(TC),(TE), but its proof silently reorders source labels — that is exactly (S0), which is not stated. The theorem may be true, but it is under-specified as written, and Theorem 4 inherits this fragility because it relies on Theorem 2.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper is a systematic review and original-research resource for Partial Information Decomposition (PID). It standardizes notation for 19 PID measures and 20 properties, presents a property–measure classification table (Table 5), compiles a theorem web relating properties (Tables 3–4, Fig. 2), and uses the Z3 SMT solver to verify compatibility claims. The core promise, stated in §1.1 and §3.1, is that every entry in Table 5 not already known in the literature is accompanied by a proof or an explicit counterexample in the appendix. The paper also contributes new theorems (e.g., Theorems 2, 4, 6, 7, 10, 11) and corrects earlier claims in the literature.","tokens_in":59507,"tokens_out":15233,"duration_ms":127920,"significance":"If the completeness claim can be substantiated, this would be the standard reference map of the PID measure/property landscape: it organizes a dispersed literature, makes the property/measure satisfaction structure explicit, and provides machine-checked compatibility results via an open-source Z3 implementation. The inclusion of unpublished measures (I_RAV) and corrections to prior proofs (e.g., Lemma 3 of Ref. [41]) are useful scholarly contributions. However, the central verification claim is currently not met to the letter: a non-negligible set of Table 5 entries rests on \"empirical tests\" rather than proofs or located counterexamples, so a reader cannot independently certify those entries. The contribution is therefore significant but requires completion before it can serve as a trustworthy map.","major_comments":[{"comment":"The promise that every non-known Table 5 entry has a proof or counterexample is not fulfilled. Appendix E.1 contains several entries justified only by \"empirical tests\" without specifying distributions or parameter values: I_IG \"(TM) holds from empirical tests\"; I_DEP \"(S1) is violated as observed from empirical tests\"; I_MES \"(LP0) is violated... as seen from empirical tests\" and \"(TM) is violated as observed from empirical tests\"; I_CT \"(AD) does not hold as observed from empirical tests\"; I_CCS \"(TM),(TC),(S1) are violated as observed from empirical tests\"; plus similar entries for I_SX, I_do, I_RAV, I_RDR, and a conditional example for I_RR. Numerical observation is not the promised proof/counterexample; if any of these entries is wrong, Table 5 is wrong. Either supply proofs/counterexamples or explicitly downgrade these to empirical claims and revise the §3.1 promise.","section":"§3.1, Table 5, Appendix E.1"},{"comment":"The proof of Theorem 2 (Eq. 49) passes from I∩(X1,X2;X1) to I∩(X2;X1). This requires permuting the sources (S0) together with (TE); the text attributes the step only to (TE). Since Theorem 2 is stated with hypotheses (SR),(TC),(TE) (Table 3), it is under-specified. Theorem 4 inherits this because it relies on Theorem 2. Add (S0) to the hypotheses or state explicitly that S0 is assumed throughout the implication table.","section":"§C.2, Theorem 2"}],"minor_comments":[{"comment":"The proof uses (TM) to justify I∩(X1,X2;f(X1,X2)) ≤ I∩(X1,X2;X1,X2), but the (TM) defined by Eq. (32) only concerns adding a target variable, not replacing the target by a deterministic coarsening f(X1,X2). As written, the proof does not follow from the stated axiom; either supply a correct proof or add the needed target-coarsening version of TM.","section":"§C.2, Proposition 6"},{"comment":"The closing remark that Theorem 12 \"can also be derived by combining Theo. 1 and Theo. 11\" is misleading: that derivation would require (EI), which is not among the hypotheses of Theorem 12. The direct citation to Ref. [19] is sufficient.","section":"§C.2, Theorem 12"},{"comment":"The intended distinction between multivariate and multiple arguments via comma versus semicolon is not visible in the typeset text: \"I(X1, X2, X3;Y)\" and \"I(X1, X2, X3;Y)\" appear identical. Please fix the notation so the two quantities are distinguishable.","section":"Appendix A"},{"comment":"The footnote apparatus is incomplete: only the I_IG/(TM) entry carries the asterisk for \"supported by empirical simulations,\" yet several other entries in Appendix E.1 also rely on empirical tests. Either flag all such entries or remove the special status of the I_IG entry.","section":"Table 5"}],"recommendation":"major_revision","confidential_remarks":"The paper is a review with an original classification layer. The main blocker is the mismatch between the promised proof/counterexample standard and the actual use of \"empirical tests\" for several Table 5 entries. This is fixable but requires real work: either producing the missing proofs/counterexamples or transparently reclassifying those entries and adjusting the central claim. The Z3 verification and open-source code are genuine strengths, and the overall organization is valuable. No concerns about citation practices: self-citations are contextual rather than load-bearing."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This paper is worth engaging with, but not on its own terms yet. The systematic measure-by-property table (Table 5), the hypergraph of implications and incompatibilities, the historical overview, and the open-sourced Z3 consistency checker are all real contributions. For anyone working in PID, this is the first place to look for a bird's-eye view of which axioms each measure satisfies, and the clustering analysis is a nice way to see the major philosophical divides. The new theorems (2, 6, 7, 10, 11) are interesting even if some proofs need tightening.\n\nNow the soft spots, and they are load-bearing. Section 3.1 promises that every non-known entry in Table 5 is backed by a proof or counterexample. The appendix doesn't deliver that. Several entries are justified by phrases like \"holds from empirical tests\" or \"violated as observed from empirical tests\" — I_IG (TM), I_DEP (S1), I_MES (LP0), I_CT (AD), I_CCS (TM/TC/S1), and others. No distributions or parameter values are given, and numerical observation is not a proof or a located counterexample. If any of those entries is wrong, the map is wrong. This is exactly the kind of gap that matters in review.\n\nTheorem 2 is a smaller but related issue. It states hypotheses (SR),(TC),(TE), but the proof silently uses (S0) to argue that I∩(X1,X2;X1) equals I∩(X2;X1). The theorem may be true, but as written it's under-specified, and Theorem 4 inherits the fragility. The Z3 tool is a consistency check on property combinations, not a verification of actual measure-specific entries, so it doesn't fill the gap.\n\nWho gets value from this? Researchers choosing a PID measure for empirical work, or anyone wanting a compact map of the axiom landscape. It is a serious survey with a testable central claim, so it deserves peer review — send it to referees, but with a clear request: either supply full proofs/counterexamples for the empirical entries or explicitly demote those entries to conjectures and weaken the completeness statement. With that revision, this could become a standard reference. Right now, treat it as an excellent draft with a pointed asterisk.\n\nI'd take it to the reading group: the gap between promise and delivery is a good teaching moment about what counts as a proof in a review paper.","headline":"The PID map is genuinely useful but the central completeness claim is over-promised: several Table 5 entries rest on 'empirical tests' rather than proof/counterexample, and Theorem 2 silently uses (S0).","tokens_in":59948,"tokens_out":2408,"would_cite":true,"duration_ms":25535,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["94A15","94A17","62B10"],"pacs":[],"model":"deepseek-v4-flash","headline":"Partial information decomposition has many competing definitions; this paper claims to map every measure to every proposed axiom with proofs or counterexamples, and to chart which axioms can coexist.","keywords":["partial information decomposition","redundancy","synergy","unique information","axiomatic properties","incompatibility theorems","redundancy lattice","information theory"],"falsifier":"Search small probability distributions with exact arithmetic for each of the four empirically tested entries — Target Monotonicity for the information-geometric measure, Strong Symmetry for the dependency-constraint measure, Local Positivity for the maximum-entropy-star measure, Additivity for the causal-tensor measure — and check whether the claimed satisfiability or violation holds; separately, check whether Theorem 2's conclusion (Identity) follows from (Self-Redundancy, Target Chain rule, Target Equality) without Weak Symmetry, since the given proof silently uses it.","tokens_in":59135,"feed_emoji":"🗺️","tokens_out":9628,"duration_ms":88411,"temperature":0.7,"pith_summary":"Partial information decomposition (PID) tries to split the mutual information between several sources and a target into redundancy, unique information, and synergy. Since its introduction, at least nineteen competing definitions and a long list of proposed axioms have appeared, and nobody knew for certain which measure satisfies which property, or even which properties can be true at the same time. This paper attempts to close that gap: it gathers the definitions in a common language, and for every measure–property pair that was not already settled it provides a proof or a counterexample in the appendix. It also assembles the web of implications and no-go theorems, adds several new ones, and uses an automatic theorem prover to find the largest sets of mutually compatible axioms. If the table is right, the field gets a single reference: a researcher can look up any measure's axiomatic profile, and any future measure can be tested against the known constraints.","feed_headline":"Proved: which information-decomposition axioms can coexist","feed_subtitle":"The full verification table and theorem web show which redundancy, synergy, and uniqueness axioms can coexist.","key_machinery":"The load-bearing machinery is the measure–property table (Table 5): each of the nineteen redundancy measures is defined in a standard notation, and every property is verified or refuted for each measure. The proofs and counterexamples live in the appendix; the table itself supports the hierarchically clustered taxonomy of measures and the hypergraph of implications and incompatibilities. Around the table, the paper places an automatic theorem prover encoding of the axioms, which checks compatibility of property combinations and identifies maximal coherent sets. The underlying objects — the redundancy lattice and the Möbius-inversion step that yields the PID atoms — are the shared skeleton th","core_discovery":"The paper's central claim is that it supplies the first systematic, verified classification of PID measures by their axioms: for every measure in the literature and every property — symmetry, monotonicity, target chain rule, identity, Blackwell property, additivity, continuity, and the rest — the paper states whether the property holds, and for every combination not previously settled it gives either a proof or an explicit counterexample. On this basis it derives new relationships among the axioms, most notably that Self-Redundancy (a single source's redundancy equals its mutual information), Target Chain rule (the chain rule for redundancy in the target), and Target Equality (adding the tar","pith_inferences":["If the table is correct, the practical lesson is that PID choice is a matter of axiomatic commitment, not a single best measure; the paper's clustering suggests only about a quarter of the axioms distinguish the existing measures, so the real design choices are few.","Since no existing measure attains the maximal 20-property set, the framework poses a concrete open problem: construct a measure satisfying all 20 (by dropping Strong Local Positivity and accepting negative atoms), or prove it impossible.","The equivalence (Weak Monotonicity + Target Equality) ⇔ Strong Monotonicity implies the axiom catalog can be slimmed, potentially changing how future measures are presented and compared.","The encoding of the property web as a computable constraint system means the entire body of PID compatibility knowledge becomes executable, which may accelerate testing of both new measures and new axioms."],"forward_implications":["A practitioner can look up any measure's axiomatic profile in one table, rather than tracing original papers.","The new incompatibility result (Self-Redundancy, Equivalence-class Invariance, Local Positivity, Target Equality, Target Chain rule) shows that even without the controversial Independent-Identity axiom, target chain rule and target equality cannot be combined with local positivity.","The implication (Self-Redundancy, Target Chain rule, Target Equality) ⇒ Identity means any measure that satisfies the chain rule and target equality will also satisfy the contested Identity property.","The maximal compatible sets give future measure designers explicit targets: 20 properties are achievable by giving up either Strong Local Positivity or Equivalence-class Invariance; keeping both caps the set at 17.","The theorem prover turns the web of axioms into a computable constraint system, so a newly proposed measure can be automatically checked against all known implications and incompatibilities."],"fun_headline_variants":["The complete proof map for information decomposition axioms","Every PID measure's axioms, proven or disproven","New theorems on redundancy and synergy in PID","Information decomposition: axiom relations fully mapped"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The load-bearing premise is that every entry of the verification table is correct, including the few justified only by 'empirical tests' rather than proofs or counterexamples — and, separately, that Theorem 2's proof, which silently uses Weak Symmetry, is valid as stated.","fun_headline_variants_meta":{"raw":{"variants":["The complete proof map for information decomposition axioms","Every PID measure's axioms, proven or disproven","New theorems on redundancy and synergy in PID","Information decomposition: axiom relations fully mapped"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000326,"raw_usage":{"total_tokens":1630,"prompt_tokens":677,"completion_tokens":953,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":421,"completion_tokens_details":{"reasoning_tokens":897}},"tokens_in":421,"tokens_out":953,"duration_ms":9935,"temperature":1.0,"reasoning_tokens":897,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T19:07:38.989431+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Search small probability distributions with exact arithmetic for each of the four empirically tested entries — Target Monotonicity for the information-geometric measure, Strong Symmetry for the dependency-constraint measure, Local Positivity for the maximum-entropy-star measure, Additivity for the causal-tensor measure — and check whether the claimed satisfiability or violation holds; separately, check whether Theorem 2's conclusion (Identity) follows from (Self-Redundancy, Target Chain rule, Target Equality) without Weak Symmetry, since the given proof silently uses it.","supporting_citations":[],"review_version":1}