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 clause | Lean counterpart | Scope |
|---|---|---|
| sites, empty or occupied | Fin L → Bool | true denotes a particle; index is site . |
| , , rate | bulkMove, bulkCount | Clear the occupied site and toggle its right neighbour; sum over all bonds. |
| Left-site , rate | leftCount, offRate | Both directions have the same rate at . |
| Right-site , rate | rightCount, offRate | Removal requires an occupied last site. |
| Target-row/source-column matrix, columns sum to zero | genMat | Diagonal is the negative sum of all off-diagonal outgoing rates. |
| One independent eigenvector at each eigenvalue | claim | Every , positive real , and real has . |
| Negative answer | result : ¬ 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.