{"id":"palomar/PALOMAR-2026-10-30-000012","url":"https://github.com/igor-kortchemski/uniform-attachment-freezing-scaling-limits/tree/8bace72d36cdf7d250414f3d98acfaa415de23d9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000012-v1.json","repo":"https://github.com/igor-kortchemski/uniform-attachment-freezing-scaling-limits","tags":["math.PR","math.CO","msc:60C05","msc:05C80","msc:60F05","msc:60J80"],"score":0,"title":"Uniform attachment with freezing: Scaling limits — Lean formalization","trust":"high","domain":"math.PR","source":"palomar","authors":["Igor Kortchemski"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 and Mathlib formalization of arXiv:2308.00484, \"Uniform attachment with freezing: Scaling limits\", published in Ann. Inst. H. Poincaré Probab. Statist. 61(4) 2679–2708 (2025). It proves the Introduction's height theorem, the subcritical Gromov–Hausdorff–Prokhorov (GHP) limit to a measured segment, the critical GHP limit to a random compact measured real tree T(f) together with its geometric properties (leaves carry the mass; binary if and only if the reciprocal-square integral diverges; root condensation otherwise), and the supercritical distance-matrix limit in its corrected…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"Uniform attachment with freezing: Scaling limits","identifier":"doi:10.1214/24-AIHP1497","relationship":"formalizes"}]}