Open Research Index

The quasi-isometry classes of Galton–Watson trees: Lean formalisation

Jayadev S. Athreya, Sascha Troscheit

Palomar Registrypalomar/PALOMAR-2026-09-25-000002Sep 30, 2026math.PRscore 0

Lean 4 formalisation of the automorphism-matching theorems and the quasi-isometry classification of Galton–Watson trees from the paper "The quasi-isometry classes of Galton–Watson trees" by Jayadev S. Athreya and Sascha Troscheit (arXiv:2609.23882). The audited statements are: the i.i.d. matching theorem on the binary tree (Theorem 5.1), the general Markov matching theorem for typed label processes on the binary tree, in its finite-type and zero-compatible forms (Theorem 6.1), the complete classification, up to quasi-isometry, of Galton–Watson trees with finitely supported offspring law…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-25-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-25-000002/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-09-25-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'