ORRW-Lower-Bound
A Lean formalization of the paper "Once-reinforced random walk on Z^d has range exponent at least d/(d+1)" by Bou-Rabee and Peres: for d >= 2 and reinforcement beta >= 1, the expected range of once-reinforced random walk is at least c beta^(-d/(d+1)) n^(d/(d+1)) (Theorem 1.1), with a stretched-exponential lower tail (Theorem 1.2), the almost-sure bound it implies, and a bound on the occupation measure (Theorem 1.3). Every lemma and proposition behind them is formalized as well, and nothing is assumed. The four main theorems are independently checked using the ORRWAudit/ comparator pairs.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-27-000011
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000011/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000011/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'