{"id":"palomar/PALOMAR-2026-09-14-000001","url":"https://github.com/JD-Jones-ASES/md-lean/tree/b7f9f9deb5f5e520c99fd0d48893808d6ad082d6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-14-000001-v1.json","repo":"https://github.com/JD-Jones-ASES/md-lean","tags":["math.CO","math.MG","msc:05C10","msc:05C62","graph-theory","planar-graphs","combinatorics"],"score":0,"title":"md-lean: exact height span, dart mass, and adjugate scaling for Mazur's greedy construction","trust":"high","domain":"math.CO","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.CO","summary":"Exact height-span of Mazur's scheme grammar, a local dart-mass bound, and an adjugate identity for the Dirichlet matrix of that construction; not a proof of the strong Papadimitriou–Ratajczak conjecture and not a theorem that every 3-connected plane graph attains the scheme maximum. Mazur builds injective integer heights by inductive recurrences on rooted pieces (edge, cycle, binary series, two-range join) and then forms a weighted Dirichlet matrix for the horizontal coordinate; the paper does not bound the height span or the bit length of the coordinates. For a well-formed scheme on n >= 2…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-14","reactions":{},"formalized":true,"formalizes":[{"title":"A Proof of the Strong Papadimitriou–Ratajczak Conjecture","identifier":"https://proofatlas.ai/formalizations/strong-papadimitriou-ratajczak-conjecture/","relationship":"adapts"}]}