Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


slug: ayyer-mallick-2010-annihilation-maximal-degeneracy bibkey: ayyermallick2010annihilation doi: 10.1088/1751-8113/43/4/045003 url: https://arxiv.org/abs/0910.0693v2 triage: theorem motivation_gids:

  • D5/S3/StatisticalMechanics/ParticleProcesses/AnnihilationMaximalDegeneracyRefutation.result

Ayyer–Mallick maximal degeneracy of the annihilation-process generator

Problem

A. Ayyer and K. Mallick, Exact results for an asymmetric annihilation process with open boundaries, J. Phys. A 43, 045003 (2010), arXiv:0910.0693v2, after Eq. (79), p. 14:

We also conjecture that the Markov matrices are maximally undiagonalizable in the sense that each eigenvalue seems to have exactly one eigenvector independent of the number of times the eigenvalue appears (this implies that the Jordan blocks are of the maximum possible size). In other words, the degeneracy seems to be so strong that the Markov matrix M_L which is of size 2^L has only 2L eigenvectors.

A. Ayyer and V. Strehl, The spectrum of an asymmetric annihilation process, arXiv:1008.2134v1, FPSAC 2010, DMTCS Proc. AN, 461–472, DOI 10.46298/dmtcs.2884, Conjecture 1, p. 466:

The matrix M_L is maximally degenerate in the sense that it has exactly 2L eigenvectors.

The model has Boolean sites, bulk transitions and at rate , a symmetric left-site flip at rate , and right-site removal at rate . This is the papers’ specialization . The matrix entry is the rate from to off the diagonal; each diagonal entry is the negative sum of the other entries in its column.

Statement echo

Source clauseLean counterpartScope
sites, empty or occupiedFin L → Booltrue denotes a particle; index is site .
, , rate bulkMove, bulkCountClear the occupied site and toggle its right neighbour; sum over all bonds.
Left-site , rate leftCount, offRateBoth directions have the same rate at .
Right-site , rate rightCount, offRateRemoval requires an occupied last site.
Target-row/source-column matrix, columns sum to zerogenMatDiagonal is the negative sum of all off-diagonal outgoing rates.
One independent eigenvector at each eigenvalueclaimEvery , positive real , and real has .
Negative answerresult : ¬ claim, , , .

The source assertion includes eigenvalues without restricting their scalar field. A two-dimensional real eigenspace already refutes it. Quantifying over all real also includes numbers outside the spectrum, whose kernels have dimension zero. The definitions at are total extensions; claim requires . The extension of bulkMove to coinciding indices is never used by a bulk transition. None of these conventions weakens the counterexample.

Motivation

The settling declaration is D5/S3/StatisticalMechanics/ParticleProcesses/AnnihilationMaximalDegeneracyRefutation.result. It refutes the geometric-multiplicity conjecture using positive rates and a real eigenvalue. The source’s characteristic-polynomial theorem concerns algebraic multiplicity, which does not determine the number of eigenvectors.

Gap

Preregistration #16707 classifies the published conjecture as Tier 1 and records source and literature checks. The Ayyer–Strehl paper proves its characteristic-polynomial result but explicitly leaves Conjecture 1 unexplained. The citation screen reported in that issue found no settlement in the checked works. These source and citation readings are orchestrator-reported; they do not prove literature completeness.

Route

The proof constructs two integer-valued functions on the configurations. For prefix signs in zero-based indexing, they are

Exact rational evaluation proves that both lie in the left kernel of . Casting transfers the equalities to the real matrix. At the empty state their values are ; at the state occupied only at index they are . The determinant of this evaluation minor is , so they are independent. Rank equality with the transpose and rank–nullity transfer the left-nullity bound to the right eigenspace. These are the mathematical steps in the proof of result; the uniform family below is a separate prose proof.

Falsifier

The settled claim is the literal geometric-multiplicity statement of #16707. The kernel-checked negation has no additional hypotheses. The witness satisfies , , and , with . Changing the transition rates, matrix orientation or source claim would change the question. The result does not assert an exact multiplicity or a general classification of Jordan blocks.

Evidence

Kernel-checked. AnnihilationMaximalDegeneracyRefutation.result proves . Its consumed private proof components qkernel1, qkernel2, vectors_independent, left_nullity, and right_nullity establish the two-vector witness and the lower bound at the stated parameters. The axiom closure of every public declaration is contained in .

Experiment. Pinned experiment directory contains check.py, SHA-256 9e1372b44346fc2fd3b639eb16745510836ba3b1a7c691371569f88b853d13d0. The commands python3 /Users/auric/trureturing-experiments/docs/reports/ayyer-mallick-2010-annihilation-maximal-degeneracy/check.py and the same command with --exact-totals both return exit , ALL_OK. The local script bytes equal the script at the cited commit.

At each , the default run checks exact rational eigenfunction equations and independence for , and checks that is distinct from the other roots in Theorem 4. The --exact-totals run computes rational ranks at every root for :

Total eigenspace dimension

These readings have exactly the listed lengths and three parameter pairs. Float SVD totals at overcount near large Jordan blocks and are not used as exact multiplicities. The float control at does not settle the resonant case.

Triage

What the settlement shows

Kernel-checked at the witness: the mechanism. Two independent left eigenvectors at exist for , , ; the consumed private declarations named in Evidence establish this within the proof of result. The vectors are quadratic polynomials in prefix signs. The two-dimensional eigenspace prevents one Jordan block from accounting for this eigenvalue. The general Walsh-action identities in the following paragraph are proved in prose, not formalized in this module.

Proved in prose: the uniform family. For , , , and , set and , with . For , the backward generator satisfies

The left flip changes the sign, contributing . Only the bulk bond changes the prefix product; its contribution is . Right-boundary removal has no effect for . For , the left flip changes both signs and cancels; only bonds and contribute, giving

For , define

The adjacent terms telescope, using :

Thus

The prefix-sign transformation is a bijection of the Boolean cube: each original sign is . Its distinct Walsh monomials are linearly independent. The monomial occurs in with nonzero coefficient and in no other , proving independence. Transpose-rank equality then gives . At , the formal vectors are and . This uniform argument is not a Lean theorem in the delivery.

Computed: sampled family and exact totals. The experiment entry verifies the equations and their ranks for at the three listed rate pairs, and computes the exact totals for at each pair. These totals exceed from in this tested scope.

Literature result: what survives. Ayyer–Strehl Theorem 4 proves the characteristic polynomial independently of Conjecture 1. Its eigenvalues and algebraic multiplicities are unaffected by this geometric-multiplicity refutation. Neither paper’s proved eigenvalue or stationary-state results are refuted by this witness.

Computed: the length-four special case. At and each of the three listed rate pairs, all distinct roots have geometric multiplicity . The conjecture holds at those instances. A uniform statement over all positive rates at is open here; the finite computation is not that statement.

Open: remaining degeneracy questions. The resonant case has and the displayed independence argument does not apply. Exact geometric multiplicities of all eigenvalues for general , including colliding roots, remain open here. The lower-bound family does not supply an exact classification.

Literature reading. Strehl’s 2020 Sém. Lothar. Combin. B81a concerns eigenvalues and partition functions, not an eigenvector-count settlement; this is a reported literature reading from the source checks accompanying #16707. The subscription chapter DOI 10.1007/978-3-030-44559-1_17 is unread. No settlement was found in the checked scope; completeness is ASSUMED-UNVERIFIED.

The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

ASSUMED-UNVERIFIED

Literature completeness is ASSUMED-UNVERIFIED, including the unread subscription chapter. The source and citation screen is attributed to the orchestrator in #16707. The uniform family is proved in prose above and is not kernel-checked. The exact-total computation settles only its stated lengths and rate pairs. General multiplicities and the resonant case are open.