What was already known
The lamplighter–percolation representation and spectral-radius factor were known from Lehner, Neuhauser and Woess. This paper identifies the sharp constant in the logarithmic correction to the return-probability decay.
AI involvement
The authors state that their QED multi-agent system generated the complete proof without human mathematical guidance after they specified the problem; they independently checked and edited the resulting proof.
Importance
Gives a sharp asymptotic beyond the previously available spectral representation for this walk.
Limitations
The paper reports the two human authors independently checked and revised the proof; no machine formalization or third-party proof review is documented. The human checking is reported by the authors.
Technical verification
The paper explicitly says its two authors independently checked the QED-generated proof of the sharp return asymptotic and revised the exposition. This is a reported completed human proof check, without a machine check. This is source-reported; AIProofWatch did not reproduce the check.
Independent checking
The paper explicitly states that both authors independently checked the QED-generated proof and revised its exposition. This is a source-reported human check of Theorem 1.
- Checker
- Chenyang An and Minghao Pan, human paper authors
- Scope
- For the switch–walk–switch lamplighter walk with Z₂ lamps over the infinite d-regular tree (d≥3), p₂ₙ(e,e)=ρ_d^{2n} exp[−(π²(log(d−1))²+o(1))n/(log n)²], where ρ_d=2√(d−1)/d.
- Basis
- Reported by the linked checker
Human understanding
The authors report independent checking and revision of the proof, and their paper explains the full spectral and percolation argument.
Correction and publication history
Primary paper, contribution attribution, prior baseline and checking scope reviewed for non-notifying local inclusion.
Read this published revision