{"id":"palomar/PALOMAR-2026-09-25-000016","url":"https://github.com/scottnarmstrong/HighContrastHomogenization/tree/7a13dbcd8d6609264a713373f5c69ceeac870472","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000016-v1.json","repo":"https://github.com/scottnarmstrong/HighContrastHomogenization","tags":["math.AP","math.PR","msc:35B27","msc:35J15","msc:60K37","homogenization","elliptic-pdes","lean-formalization"],"score":0,"title":"HighContrastHomogenization","trust":"high","domain":"math.AP","source":"palomar","authors":["Scott Armstrong","Tuomo Kuusi","Amélie Loher"],"reviews":0,"subject":"math.AP","summary":"A Lean formalization of \"Homogenization at a polynomial scale in high contrast\" by Armstrong, Kuusi and Loher. The paper studies elliptic equations in random media whose conductivity can vary greatly. It proves that their large-scale behavior becomes predictable at a length bounded by a polynomial in the parameters measuring contrast and randomness, improving earlier bounds. The formalization includes quantitative convergence estimates, approximation by an effective constant-coefficient equation, and large-scale regularity results. It builds on the CoarseGraining library.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"Homogenization at a polynomial scale in high contrast","identifier":"arxiv:2609.27647","relationship":"formalizes"}]}