{"id":"palomar/PALOMAR-2026-11-01-000030","url":"https://github.com/igor-kortchemski/uniform-attachment-with-freezing/tree/48410b254fbc5d8c1a483acb8309338baa479a6f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000030-v1.json","repo":"https://github.com/igor-kortchemski/uniform-attachment-with-freezing","tags":["math.PR","math.CO","msc:60C05","msc:05C80","msc:60F05"],"score":0,"title":"Uniform attachment with freezing: equivalence in law of the forward and reversed constructions","trust":"high","domain":"math.PR","source":"palomar","authors":["Igor Kortchemski"],"reviews":0,"subject":"math.PR","summary":"Lean proof that the forward uniform-attachment/freezing construction and the reversed growth-coalescent construction give the same distribution of labelled rooted trees, after the prescribed erasure of active reverse labels. The equality includes the extinction endpoint. It is stated on a canonical encoding that retains the complete graph and relevant labels. The dictionary to literal isomorphism-class language is mathematically reviewed but is not an additional Lean quotient-law equivalence theorem. This entry covers T05 and shares its proof repository with the companion asymptotic and SIR…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Uniform attachment with freezing","identifier":"sha256:88953dd87165a14b0e643c5b3d0075d8ce5ec39cdcfc0c25d313570fc3ab00df","relationship":"formalizes"}]}