Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


slug: camargo-nishida-2026-gaussian-multientropy bibkey: camargo2026gaussianmultientropy doi: 10.48550/arXiv.2609.30754 url: https://arxiv.org/abs/2609.30754v1 triage: theorem motivation_gids:

  • D5/S3/Quantum/Entanglement/GaussianMultiEntropyAsymptotic.result

The large-squeezing law of the genuine multi-entropy of fully symmetric Gaussian states

Problem

H. A. Camargo and M. Nishida, Genuine Multi-Entropy of Fully Symmetric Gaussian States, arXiv:2609.30754v1, compute the tripartite genuine Rényi multi-entropy of the fully symmetric pure Gaussian state of bosonic modes (diagonal , off-diagonal of their Eq. (3.1)) for and , observe as (Eq. (3.8)), and write “we \emph{conjecture} that the asymptotic behavior \eqref{AsymB} is valid for the fully symmetric Gaussian states with any and .” The verbatim definitions are in the literature note.

Issue #13990 reads the conjecture for every replica order and every tripartition with positive party sizes , with the replica partition functions as the literal Lebesgue integrals of products of the real Gaussian density kernels under the twists , and asymptotic equivalence in the sense of Asymptotics.IsEquivalent (for both sides are the zero function).

Motivation

At infinite squeezing the fully symmetric states approach the continuous-variable GHZ state, whose genuine multi-entropy has the same leading term; the conjecture asserts that the finite- computations of the paper extend to every number of modes and every replica order.

Gap

Issue #13990 records the literature check before any Lean: one arXiv version; arXiv abstract searches for multi-entropy with Gaussian states and for genuine multi-entropy found no proof of Eq. (3.8); Zenodo had no record; the repository had no result on Gaussian multi-entropy. not-found-in-searched-scope.

Route

  1. The replica integral of the Gaussian kernels is a Gaussian integral (transplanted into GaussianReplicaReduction), and with , the projection onto constant mode vectors, it equals with .
  2. Writing , with orthonormal columns, Sylvester’s identity and the Schur complement reduce to the replica-level determinant , where .
  3. is symmetric and row stochastic. If one twist is the identity and the twists act transitively, a vector fixed by a stochastic matrix with positive twist entries is constant (a maximal coordinate propagates along twist paths), so the eigenvalue is simple and with continuous and .
  4. , hence , and the four replica determinants give for .
  5. For , the squared non-trivial eigenvalues of the tripartite and the three bipartite replica matrices coincide, which gives and for all .

Falsifier

The settlement concerns the fully symmetric states of the paper and the asymptotic regime ; other Gaussian families, finite- values and other replica conventions are outside the claim.

Evidence

The canonical sources are D5/S3/Quantum/Entanglement/GaussianMultiEntropyAsymptotic.lean (the definitions of the replica integrals Z, Z3, Z2, the entropies S3, S2, GM3, claim, result, and the bridges from the integrals to the replica determinants) and its helper module D5/S3/Quantum/Entanglement/GaussianReplicaReduction.lean (the transplanted Gaussian integral, see its source note, the block-determinant reduction, the kernel of stochastic twist averages, the determinant factorization and the asymptotic lemmas; Mathlib only). The axiom closure of result is exactly propext, Classical.choice and Quot.sound; there is no sorry, native_decide, or new axiom. The settlement module statement is sha256:1e9e370f3b4f550a2b6d8038fd7afaf11ea9965043eb15f5187d2d08c77a487e, the result statement sha256:a34bff0157a712c7a0e0a93aa692ecfe0e0e123ae890c7a188268cd72c0abe89 and the claim statement sha256:5a42c12a9865413553ec0317926bcfb6cbcacbbe473f27e7135ab7270beccff2; its Freeze event is sha256:2021168bd5dce175bf113ddcdb3306504b22694ad0d2e77e857e38bc205fc6dd, with the helper module as project-level prerequisite. The helper GaussianReplicaReduction has module statement sha256:767695a861b18eb09b63f64a115f6056e9fba1a35e6d43cbe03f4b5aed88419c and Freeze event sha256:842cb437647dc94fe8b162ab98569ad2838eea347014873987534dc6f047964e, with no project-level prerequisite.

Triage

Tier 1 conjecture of a September 2026 paper, preregistered in issue #13990 before any Lean and run as a research line. theorem; resolution proved.

declarationproof_shapeescape_witnessadmission_basis
resultcontentthe kernel of stochastic twist averages (stochastic_twist_kernel, permutation_average_kernel) on its proof pathopen-problem-resolution

The other public declarations of the two modules carry free parameters and lie on the proof path of result. Utility is none. There is no digestion atom.

What the settlement shows

Proved by result: for every and all positive , as ; for the multi-entropy is eventually zero.

Proved on the way, for general data:

  • Replica determinant. For any finite replica type and any twists, the replica integral of the fully symmetric state is , and equals the replica-level determinant .
  • Simple eigenvalue. For twists that contain the identity and act transitively, the only vectors fixed by are the constants, and the determinant is with continuous and .
  • Exact identity. For every tripartition, at , which is the fully symmetric case of the paper’s §4 theorem .

Argued, not formalized.

  • Mechanism. The coefficient of is fixed by the replica counts alone ( for the tripartite term, for each bipartite term), because the eigenvalue is simple in every term; the remaining spectrum contributes only the constant .
  • The subleading constant. converges to ; numerically the limits lie between and for the configurations of #13990.

Open. A closed form of in terms of and the party fractions, and the corresponding statement for the multi-entropy, are not settled here.

Effect on the paper. Eq. (3.8) holds for every and every tripartition with positive party sizes.

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent proof.