Return Probability for the Switch--Walk--Switch Lamplighter Walk on a Regular Tree

Chenyang An; Minghao Pan

arxiv: 2605.21744 · v1 · pith:5ZYVASFUnew · submitted 2026-05-20 · 🧮 math.PR

Return Probability for the Switch--Walk--Switch Lamplighter Walk on a Regular Tree

Chenyang An , Minghao Pan This is my paper

Pith reviewed 2026-05-22 07:49 UTC · model grok-4.3

classification 🧮 math.PR

keywords lamplighter walkregular treereturn probabilityasymptotic analysisrandom walk on graphprobability on groupsAI-generated proof

0 comments

The pith

The return probability p_{2n}(e,e) for the switch-walk-switch lamplighter walk on the d-regular tree equals rho_d^{2n} times exp[-(pi^2 (log(d-1))^2 + o(1)) n / log^2 n].

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper derives the exact large-n decay rate of the probability that this lamplighter random walk returns to the root after 2n steps on an infinite d-regular tree. The main term is the spectral radius rho_d to the power 2n, while a slower correction exp(-c n / log^2 n) with c = pi^2 (log(d-1))^2 governs the sub-exponential factor. A reader cares because the precise rate controls recurrence, transience, and mixing behavior for walks that combine lamp toggling with movement on a tree. The derivation was produced entirely by an automated multi-agent system from a problem statement alone, supplying a concrete test of whether such systems can output full rigorous proofs in probability on graphs.

Core claim

We derive the sharp return-probability asymptotic for the switch--walk--switch lamplighter walk with lamp group Z_2 over the infinite d-regular tree: p_{2n}(e,e) = rho_d^{2n} exp[ -(pi^2 (log(d-1))^2 + o(1)) n / log^2 n ]. The proofs were generated by QED, a multi-agent system co-developed by the authors, without human intervention beyond the specification of the problem.

What carries the argument

The switch-walk-switch lamplighter walk, which toggles the current lamp state, moves along an edge of the tree, and toggles again, with each lamp taking values in Z_2.

If this is right

The dominant exponential decay is governed exactly by the spectral radius rho_d of the underlying walk.
The sub-exponential factor exp(-c n / log^2 n) supplies the sharp correction that determines finer recurrence properties.
The same asymptotic form holds uniformly for all even times 2n as n tends to infinity.
The result applies specifically to the binary lamp group Z_2 on any fixed degree d >= 3.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

If the AI-generated proof is accepted, the same automated approach could be applied to return probabilities for lamplighter walks with other finite lamp groups.
The form of the correction term suggests a connection to large-deviation principles or embedding the walk into a continuous-space limit on the tree.
Verification of the asymptotic on finite trees of increasing size would provide an independent check independent of the formal proof.

Load-bearing premise

The multi-agent QED system produces a complete, error-free rigorous proof from the problem specification alone, with no hidden human corrections or post-generation edits required for correctness.

What would settle it

An exact or high-precision numerical computation of the return probability on a large finite truncation of the d-regular tree for n around 10^4 or larger, checking whether log(log(1/p_{2n})) * (log n)^2 / n converges to pi^2 (log(d-1))^2.

read the original abstract

We derive the sharp return-probability asymptotic for the switch--walk--switch lamplighter walk with lamp group $\mathbb Z_2$ over the infinite $d$-regular tree: \[ p_{2n}(e,e) = \rho_d^{2n} \exp\left[ -\left(\pi^2(\log(d-1))^2+o(1)\right) \frac{n}{\log^2 n} \right]. \] The proofs were generated by QED, a multi-agent system co-developed by the authors, without human intervention beyond the specification of the problem. This provides a test case for the ability of AI systems to produce rigorous mathematical proofs.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a new explicit asymptotic for return probabilities of this lamplighter walk on regular trees, but the entire proof comes from an uninspectable AI system.

read the letter

The main point is that they derive a sharp form for p_{2n}(e,e) on the d-regular tree for the switch-walk-switch lamplighter with Z_2 lamps, specifically with the coefficient π² (log(d-1))² in the exponent of the sub-exponential term. That level of precision for this exact variant does not seem to be in the earlier literature they reference, so the formula itself is a concrete addition to the asymptotics of these walks. They also frame the work as a test case for their QED multi-agent system producing a full rigorous proof from the problem statement alone, which is a straightforward way to document what the system can handle on a structured probability question. The claim is stated cleanly and the constants look like they come from standard singularity or Tauberian analysis rather than any fitting. The obvious limitation is that the proof steps are not included. Without seeing how the recurrence relations for the lamp states and tree positions were set up, or how the generating functions led to the precise log n in the denominator, there is no way to verify the coefficient or rule out a gap in the branching-factor handling. The result therefore rests on trusting that the AI output was complete and error-free, which is a heavy assumption for a sharp asymptotic. This is aimed at people who work on random walks on trees and lamplighter groups and want the latest precise rates, or at those tracking AI-assisted proofs in probability. A reader in either group could get something useful from it if the derivation checks out. I would send it to peer review so that experts can attempt to reconstruct the key analytic steps or run simulations for small d to test the predicted decay.

Referee Report

1 major / 0 minor

Summary. The paper claims to derive the sharp asymptotic return probability for the switch-walk-switch lamplighter walk with lamp group Z_2 on the infinite d-regular tree: p_{2n}(e,e) = ρ_d^{2n} exp[−(π² (log(d−1))² + o(1)) n / log² n]. It states that the proofs were generated entirely by the QED multi-agent AI system from the problem specification alone, with no human intervention or post-edits, and presents this as a test case for AI-generated rigorous proofs.

Significance. If correct, the explicit asymptotic would provide a precise quantitative description of return probabilities for this lamplighter walk, building on existing work on random walks on trees and wreath products. The paper's use of an AI system to produce the derivation is a strength worth noting, as it supplies a concrete, reproducible example of automated proof generation in probability on groups.

major comments (1)

[Abstract] Abstract, displayed equation: the claimed sharpness of the asymptotic, including the precise coefficient π²(log(d-1))², rests on a derivation (recurrence relations, generating functions, and Tauberian extraction) that is stated to have been produced by the QED system but is not supplied in inspectable form. This prevents verification of the steps and is load-bearing for the central claim.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for identifying the need to make the derivation inspectable. We address the major comment below and will revise the manuscript to resolve the verification issue.

read point-by-point responses

Referee: [Abstract] Abstract, displayed equation: the claimed sharpness of the asymptotic, including the precise coefficient π²(log(d-1))², rests on a derivation (recurrence relations, generating functions, and Tauberian extraction) that is stated to have been produced by the QED system but is not supplied in inspectable form. This prevents verification of the steps and is load-bearing for the central claim.

Authors: We agree that the absence of the explicit derivation steps prevents verification of the central claim. The manuscript states that the proofs were generated by the QED system from the problem specification with no human intervention or post-edits. To address this, the revised version will include the complete, unedited output of the QED multi-agent system as an appendix. This appendix will contain the full recurrence relations, generating functions, and Tauberian extraction that yield the stated asymptotic, allowing direct inspection of each step while preserving the paper's emphasis on automated proof generation. revision: yes

Circularity Check

0 steps flagged

No circularity: asymptotic derived from standard lamplighter and tree structures with independent constants

full rationale

The paper presents a claimed derivation of the return probability asymptotic p_{2n}(e,e) = ρ_d^{2n} exp[−(π²(log(d−1))² + o(1)) n / log² n] directly from the switch-walk-switch lamplighter group action on the d-regular tree. The leading constants π² and log(d−1) are standard in the literature on random walks and lamplighter processes on trees and are not obtained by fitting to the target quantity or by redefinition. The mention of QED as the proof-generation tool is a statement about the production method rather than a load-bearing mathematical premise that reduces the result to prior self-authored theorems. No equations are shown to be equivalent by construction, no parameters are fitted then renamed as predictions, and no uniqueness theorem is imported from overlapping prior work. The derivation chain therefore remains self-contained against external benchmarks such as known generating-function techniques for tree walks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The abstract provides no explicit list of free parameters or invented entities. The derivation is described as relying on standard facts about regular trees, generating functions for random walks, and asymptotic analysis techniques that are treated as background knowledge.

axioms (2)

domain assumption Standard properties of the infinite d-regular tree and the definition of the switch-walk-switch lamplighter walk with Z_2 lamps hold.
Invoked implicitly when stating the model whose return probability is analyzed.
standard math Classical Tauberian theorems or singularity analysis apply to the generating function of the walk.
Required to extract the precise sub-exponential correction from the return probability generating function.

pith-pipeline@v0.9.0 · 5647 in / 1644 out tokens · 51831 ms · 2026-05-22T07:49:19.120408+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AlexanderDuality.lean alexander_duality_circle_linking unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

p_{2n}(e,e)=ρ_d^{2n} exp[−(π²(log(d−1))²+o(1)) n / log² n] via killed operator P_ω and sparse-ball estimate sup |T∩B(v,r_δ)|<a_η b^{r_δ} ⇒ sup σ(P_T)<ρ_d(1−δ)
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

ν_d spectral measure on [−ρ_d,ρ_d] and trace τ on equivariant random operators

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

8 extracted references · 8 canonical work pages · 1 internal anchor

[1]

C. An, Q. Ye, M. Pan, and J. Zhang,QED: An open-source multi-agent system for generating mathematical proofs on open problems, arXiv:2604.24021 (2026)

work page internal anchor Pith review Pith/arXiv arXiv 2026
[2]

Dicks and T

W. Dicks and T. Schick,The spectral measure of certain elements of the complex group ring of a wreath product, Geometriae Dedicata93(2002), 121–137

work page 2002
[3]

W. Ehm, T. Gneiting, and D. Richards,Convolution roots of radial positive definite functions with compact support, Transactions of the American Mathematical Society356 (2004), 4655–4685

work page 2004
[4]

R. I. Grigorchuk and A. ˙Zuk,The lamplighter group as a group generated by a 2-state automaton, and its spectrum, Geometriae Dedicata87(2001), 209–244

work page 2001
[5]

Khorunzhiy, W

O. Khorunzhiy, W. Kirsch, and P. M¨ uller,Lifshitz tails for spectra of Erd˝ os–R´ enyi random graphs, The Annals of Applied Probability16(2006), 295–309. 20

work page 2006
[6]

Kirsch and P

W. Kirsch and P. M¨ uller,Spectral properties of the Laplacian on bond-percolation graphs, Mathematische Zeitschrift252(2006), 899–916

work page 2006
[7]

Lehner, M

F. Lehner, M. Neuhauser, and W. Woess,On the spectrum of lamplighter groups and percolation clusters, Mathematische Annalen342(2008), 69–89

work page 2008
[8]

M¨ uller and P

P. M¨ uller and P. Stollmann,Spectral asymptotics of the Laplacian on supercritical bond- percolation graphs, Journal of Functional Analysis252(2007), 233–246. 21

work page 2007

[1] [1]

C. An, Q. Ye, M. Pan, and J. Zhang,QED: An open-source multi-agent system for generating mathematical proofs on open problems, arXiv:2604.24021 (2026)

work page internal anchor Pith review Pith/arXiv arXiv 2026

[2] [2]

Dicks and T

W. Dicks and T. Schick,The spectral measure of certain elements of the complex group ring of a wreath product, Geometriae Dedicata93(2002), 121–137

work page 2002

[3] [3]

W. Ehm, T. Gneiting, and D. Richards,Convolution roots of radial positive definite functions with compact support, Transactions of the American Mathematical Society356 (2004), 4655–4685

work page 2004

[4] [4]

R. I. Grigorchuk and A. ˙Zuk,The lamplighter group as a group generated by a 2-state automaton, and its spectrum, Geometriae Dedicata87(2001), 209–244

work page 2001

[5] [5]

Khorunzhiy, W

O. Khorunzhiy, W. Kirsch, and P. M¨ uller,Lifshitz tails for spectra of Erd˝ os–R´ enyi random graphs, The Annals of Applied Probability16(2006), 295–309. 20

work page 2006

[6] [6]

Kirsch and P

W. Kirsch and P. M¨ uller,Spectral properties of the Laplacian on bond-percolation graphs, Mathematische Zeitschrift252(2006), 899–916

work page 2006

[7] [7]

Lehner, M

F. Lehner, M. Neuhauser, and W. Woess,On the spectrum of lamplighter groups and percolation clusters, Mathematische Annalen342(2008), 69–89

work page 2008

[8] [8]

M¨ uller and P

P. M¨ uller and P. Stollmann,Spectral asymptotics of the Laplacian on supercritical bond- percolation graphs, Journal of Functional Analysis252(2007), 233–246. 21

work page 2007