Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: arias-di-giulio-keski-vakkuri-tonni-2023-charge-sector-majorization
bibkey: ariasdigiuliokeskivakkuritonni2023capacity
doi: 10.1007/JHEP03(2023)175
url: https://arxiv.org/abs/2301.02117v1
triage: theorem
motivation_gids:
  - D5/S3/Entropy/ChargeSectorMajorizationRefutation.result

Majorization need not survive normalization in a common charge sector

Problem

R. Arias, G. Di Giulio, E. Keski-Vakkuri and E. Tonni, Probing RG flows, symmetry resolution and quench dynamics through the capacity of entanglement, arXiv:2301.02117v1, JHEP 03 (2023) 175, Section 7, “Symmetry-resolved related issues”, ask (CDraft-Final.tex, line 4140):

For instance, given two density matrices such that , we may ask whether this majorization order survives once we decompose and according to (\ref{eq:decompositionrho}). One can try to diagnose this aspect using in (\ref{SR-M_n}), given that these quantities are entanglement monotones also in a fixed charge sector. We leave this analysis for future investigations.

The referenced equation is the normalized charge-block decomposition of Section 6, equation (6.1), TeX lines 3550–3569: , with and . Section 6 obtains this decomposition for a reduced state commuting with its subsystem charge; the registered comparison uses one common subsystem charge operator. See the literature note.

Issue #22533 fixes the sectorwise reading: does imply for every charge whose weight is positive in both states? This implication is refuted already for finite diagonal states.

The formal claim quantifies over every , charge map and real vectors with nonnegative entries and . Put , the module’s reused pushforward, and let be the descending list of for all indices with , the module’s sectorSpectrum. Zero eigenvalues retain their multiplicities. The claim says that implies for every integer with and .

For equal-length descending lists , the reused Majorizes requires every prefix sum of to be at least the corresponding prefix sum of for , and equal total sums. This is the direction used in the source’s definition of majorization (TeX line 830).

Motivation

The question connects a comparison of whole entanglement spectra to comparisons conditioned on a measured charge. An affirmative answer would let global majorization supply the ordering needed to compare Schur-concave quantities inside each normalized block. A negative answer identifies information about charge labels that a global spectral comparison does not control.

Gap

Issue #22533 records a bounded literature check: the search reported no settlement among the 19 citing works listed by INSPIRE, two targeted arXiv searches, MathDB and formal-conjectures. It also records no pre-existing repository reference to the paper. The arXiv version listing and retention of the question in the journal version are reported there. These search findings are preregistration-reported; the direct source reading here covers arXiv v1.

not-found-in-searched-scope.

Route

All the following private lemmas concern the fixed four-level data , and ; none asserts a conclusion for arbitrary vectors or charges.

  1. State hypotheses. r_state and s_state establish nonnegativity of every entry and total mass one for these respective vectors.
  2. Global order. full_spectra identifies their descending lists as and . global_majorizes proves majorization in the proposed direction for these lists; their prefix sums are and .
  3. Positive normalized sector. At charge zero, sector_weights proves , so both positivity hypotheses hold. For these same vectors, charge map and charge zero, sector_spectra identifies the normalized descending lists as and .
  4. Contradiction. sector_failure refutes majorization between these charge-zero lists: its first prefix inequality would require . result instantiates claim with the four-level data and charge zero, supplying both state hypotheses, global_majorizes and the two strictly positive sector weights, to obtain this contradiction.

Falsifier

The refutation answers the source question under the registered sectorwise reading. Faithfulness requires the same charge operator for both states, normalization by each state’s own positive sector weight, and the source’s direction of majorization. The formal definitions use a shared charge map, divide by the corresponding pushforward, retain all indices in the charge eigenspace, and sort in descending order. Thus the compared sector lists have the same length even when some eigenvalues vanish; zero-weight sectors are outside the claimed implication.

For the matrix interpretation take , and . These diagonal states commute with the same and their spectra and normalized blocks are precisely the lists above. Their realization as reductions of total-charge eigenstates is argued below; this matrix and purification bridge is not formalized in the module.

Evidence

The canonical source is D5/S3/Entropy/ChargeSectorMajorizationRefutation.lean.

  • Proof. It proves result : ¬ claim.
  • Reuse. It uses Majorizes from LinDTIMajorizationRefutation, desc from PositiveSimplexGeometryAndMixing, and pushforward from CapacityMonotone.
  • Axioms. It uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.
  • Escape registrations. result is the designated refutation result of the utility header and is exempt. The module has no other public theorem.

Frozen state: Golden/Frozen/state/D5/S3/Entropy/ChargeSectorMajorizationRefutation.lean.json.

Declaration statements:

  • result: sha256:14131ed0450d463729355d24c3942ae06046c4dba86450ac729b918f900348a2;
  • claim: sha256:426437ee97955ca012af67eba04352ffb19a55a650d6e6ee51b46b97783fe930.

Triage

Tier 1 question of a 2023 JHEP paper, preregistered in issue #22533 before any Lean. theorem; resolution refuted.

declarationproof_shapeescape_witnessadmission_basis
resultbind-onlynone: the fixed spectra, sector weights and failed prefix inequality reduce to rational arithmetic and the imported definitionsopen-problem-resolution
sectorSpectrum, claimbind-onlynonedefinitions used by result
the fixed-data definitions and private witness lemmasbind-only (consumed on the proof path of result)noneconsumed helpers

Every declaration is bind-only. The bind-only form is admitted under the open-problem-resolution basis of CLAUDE.md §3.2; no escape witness is claimed. The refutation is a certified instance with basis refutes. There is no digestion atom.

What the settlement shows

Proved by result: it is false that, for every natural , integer charge map on , and pair of nonnegative real unit-mass vectors , majorization of their descending full spectra implies majorization of their normalized sector spectra for every integer charge with positive weight in both vectors.

Computed, not formalized (exact rational arithmetic): for the four-level witness, the charge-one blocks have equal positive weight and the normalized charge-one spectrum of majorizes that of .

Argued, not formalized.

  • Failure mechanism. Global sorting discards charge labels. In the fixed witness of full_spectra, the largest weight of lies at charge one, while the largest weight of lies at charge zero. The charge-zero blocks in sector_spectra, with the common positive weight established by sector_weights, instead compare a uniform pair to a nonuniform pair in the direction ruled out by sector_failure. The computed equality of the charge-one weights, together with sector_weights at charge zero, shows that requiring equal probabilities for every charge does not repair this witness. A global spectral order does not specify how spectral weight is assigned to the charge eigenspaces.
  • Physical realization. For either fixed probability vector or , set and . The norm squared is . Every occupied basis pair has charge plus charge equal to one, so is a charge-one eigenstate of . Taking the partial trace over removes terms with unequal basis indices and gives , realizing both counterexample states in the source’s pure-state setting.
  • Sufficient extra structure. Suppose are nonnegative unit-mass vectors on the same finite charge-labelled basis and , where is nonnegative, every row and column sums to one, and whenever . Each charge block of is then doubly stochastic and preserves that sector’s total mass. For a sector with positive mass, division by this common mass gives for the two normalized block vectors. For any set of output indices, with , and . Sort decreasingly. Subtracting from each entry gives for . Choose to contain the largest entries of ; column sums give equality of totals. Hence sectorwise majorization follows under this additional mixing constraint. This supplies a sufficient condition, not a characterization of all pairs with sectorwise order.
  • Surviving special cases. If every basis index has the same charge, the unique positive sector has mass one and its spectrum is the full spectrum, so the implication reduces to its premise. If a charge eigenspace has one basis index and both weights there are positive, both normalized block spectra are , so majorization in that sector is automatic. Neither observation supplies a general classification for degenerate charge eigenspaces.
  • Effect on the source. Section 7 poses preservation as a question. The trace decomposition in Section 6 is obtained by substituting the direct-sum decomposition into a trace; this does not require a majorization comparison between two states. The refutation therefore removes no premise of that calculation. It excludes inferring every sector’s Schur-concave comparison from global majorization alone; when sectorwise majorization is supplied independently, such comparisons remain its defining consequence. The separate questions about RG-flow ordering, quench ordering and the general moment-decomposition formula are not settled by result.

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty or priority. The 19-work INSPIRE search, two targeted arXiv searches, MathDB and formal-conjectures checks, arXiv version-list reading, journal-version reading and pre-existing repository search are reported in #22533 and have not been independently reproduced. The direct paper reading is arXiv:2301.02117v1, CDraft-Final.tex, MD5 5739b2bdf5eab61756172c2a3f55d9e0.

The statements in “Computed, not formalized” and “Argued, not formalized”, including the matrix and pure-state interpretation, the sufficient mixing condition, the special cases and the assessment of effects on the source, are not formalized by result. A necessary and sufficient structural condition for inferring sectorwise preservation from global order is not supplied here. No conclusion is drawn about preservation restricted to a particular field theory, RG flow or quench family, or about the source’s other open questions.