slug: datta-dorlas-jozsa-benatti-2014-conditional-subentropy-conjecture-2
bibkey: datta2014conditionalsubentropy
doi: 10.48550/arXiv.1310.1312
url: https://arxiv.org/abs/1310.1312v1
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.result

Conditional subentropy and guessing min-entropy

Problem

Datta, Dorlas, Jozsa and Benatti, Properties of subentropy, arXiv:1310.1312v1, §2.5.1, Conjecture 2:

For a c-q state ρ_XB, the conditional subentropy Q(X|B) satisfies the following bound: Q(X|B) ≤ H_min(X|B) = − ln p_guess(X|B).

For every finite family of positive semidefinite complex matrices $A_x$ of total trace one, the joint state is ${⨁}_x{A}_x$ and its marginal is ${\sum }_x{A}_x$. The claim uses equation (4), with normalized simplex measure from equation (3), for subentropy. Natural logarithms are used. Zero blocks, zero eigenvalues and repeated eigenvalues remain in scope.

Statement echo

Motivation

Preregistration #18776 identifies this as a tier-1 explicit published conjecture. The resolving declaration is D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.result.

Gap

The source’s literal simplex integral must agree with the repository’s determinant-integral subentropy on every positive semidefinite trace-one matrix, including singular and repeated-spectrum matrices. The private source_eq_determinant bridge supplies this correspondence. The existing POVMGram.cq_conditional_subentropy_guessing is reused for the operational estimate. The settling result is classified bind-only after expansion of same-delivery helpers; its admission basis is open-problem-resolution (#18776; Proved).

Route

Radial decomposition of the exponential law and its Gamma moments express the normalized simplex integral as a Gaussian quadratic expectation. Spectral transport identifies that expression with determinant-integral subentropy. Normalize every nonzero positive block to a density state, using a harmless density state at zero weights. The canonical record and mixture states then have the same subentropy values as the block diagonal and summed matrices. The frozen conditional guessing theorem gives the conclusion.

All six public definitions retain the preregistered source expressions; the existing chart and Real.negMulLog are used directly. The private simplex measure uses RenewalMinorantMaximalityRefutation.Ak through the consumed simplexCoords_eq_Ak correspondence. No owner is published or re-pinned.

Falsifier

A positive semidefinite finite block family of total trace one with $Q(X\mid B)>-\ln p_{\mathrm{guess}}(X\mid B)$ would contradict the formal statement. A discrepancy between the source integral and determinant-integral convention would invalidate the proposed transfer. The compiled result and its correspondence cover both obligations within the stated finite-dimensional model.

Evidence

Kernel evidence: D5.S3.Quantum.Measurement.ConditionalSubentropyGuessingBound.result : claim. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

The four-slot escape audit is unfinished under issue #20025. The sole public theorem is result; no Reg mirror or declared_validated registration is delivered. The issue identifies the failed template attempt and missing compiled realization, source selection and binding evidence.

Declaration judgement

Helpers and consumers

Numerical evidence

The experiment is the pinned directory in trureturing-experiments.

Command: /Users/auric/.sshx/43196ccfd59b1d204c3f3897/attempt-1/experiment-env/bin/python /Users/auric/trureturing-experiments/docs/reports/datta-dorlas-jozsa-benatti-2013-conjecture-2-conditional-subentropy/check.py; exit 0, RESULT PASS. The committed check.py SHA-256 is 72c037123411fbde7853e64d3349ec84843b2dbb0706eb5ab06e7a1887d0acd6; commit membership and local bytes were checked.

Computed scope: equation (4) agrees with equation (1) on spectra $(0.7,0.3)$, $(0.5,0.3,0.2)$ and $(0.61,0.27,0.12)$, with maximum difference $4.93\times 10^{-32}$. Across 120 sampled c-q ensembles, the maximum of $Q(X\mid B)-(1-P_{\mathrm{up}})$ is $-0.0019293938015541088$ and the maximum primal–dual gap is $2.2579642044995296\times 10^{-8}$. Here the script repairs a dual-feasible upper bound on guessing probability numerically. Across 400 sampled probability vectors, the largest tangent-bound residual is $-6.165877369270764\times 10^{-9}$. The derivative check gives $1.0$ for $m=2,3,5,8$. The pinching gap is $0.01702$, compared with Monte Carlo relative entropy $0.01752\pm 0.00029$. The solver emits an accuracy warning; these finite numerical readings are distinct from kernel evidence and establish no uniform numerical theorem.

Triage

What the settlement shows

Mechanism, kernel-checked in result and its private live dependencies. The normalized simplex integral and determinant-integral subentropy agree through Gaussian radial decomposition. The finite c-q block family then fits the existing ensemble estimate. No positive-spectrum or nonzero-prior assumption is added.

Stronger bound, proved in prose. Set $p_x=\mathrm{tr}(A_x)$ and write $A_x=p_x{\rho }_x$, assigning any fixed density state when $p_x=0$; positivity makes a trace-zero block zero. The private normalization and record/marginal correspondences identify the two subentropy differences and the two guessing suprema. The first component of the consumed frozen POVMGram.cq_conditional_subentropy_guessing gives $Q(X\mid B)\le 1-p_{\mathrm{guess}}$. Its second component gives $1-p_{\mathrm{guess}}\le -\ln p_{\mathrm{guess}}$. The public result states only their composite logarithmic inequality.

Tightness, proved in prose within the perfectly distinguishable case. Orthogonal signal supports admit a POVM with success one; total trace bounds every success score by one. Thus $p_{\mathrm{guess}}=1$. The block joint state and summed marginal have the same nonzero spectrum; the Gaussian/determinant correspondence preserves zero padding. Their subentropies agree, so both bounds are zero. No classification of all equality cases is asserted.

Scope of source consequences. Every finite c-q use of the source’s conjectured guessing estimate now has the formal logarithmic inequality under its stated convention, and Proposition 6 is contained in this finite-family scope. This module makes no claim about infinite-dimensional states or a complete equality classification. Conjecture 1 and alternative smaller operational bounds are separate questions.

ASSUMED-UNVERIFIED

The external literature screen recorded in #18776 reads the source and searches conditional subentropy with guessing probability/min-entropy. The additional papers listed there are attributed to the GPT Pro search seat, rather than presented as implementation-seat readings. Completeness remains ASSUMED-UNVERIFIED; the formal result does not certify literature novelty. Numerical solver and Monte Carlo outputs are finite computations, not proof of the uniform statement. The four-slot escape audit remains unfinished under #20025.