{"id":"palomar/PALOMAR-2026-09-15-000006","url":"https://github.com/scottnarmstrong/CoarseGraining/tree/28ca42c02fd286c8f63a45be3344f6f82d026db3","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-15-000006-v1.json","repo":"https://github.com/scottnarmstrong/CoarseGraining","tags":["math.AP","msc:35B27","msc:60K37","msc:35J15","homogenization","elliptic-pdes","stochastic-analysis","lean-formalization"],"score":0,"title":"CoarseGraining","trust":"high","domain":"math.AP","source":"palomar","authors":["Scott Armstrong","Tuomo Kuusi"],"reviews":0,"subject":"math.AP","summary":"A Lean formalization of the coarse-graining approach to quantitative stochastic homogenization of divergence-form elliptic equations: function-space, deterministic, probabilistic, and homogenization-scale theory up to the quenched minimal-scale theorem. The public main result is a uniformly elliptic, isotropic specialization of the quenched homogenization comparison estimate in Armstrong-Kuusi, \"Renormalization Group and Elliptic Homogenization in High Contrast\" (Inventiones Mathematicae, 2025), independently checked using Audit/QuenchedComparison/comparator.json, together with four further…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-15","reactions":{},"formalized":true,"formalizes":[{"title":"Coarse-Graining Theory for Elliptic Equations","identifier":"","relationship":"formalizes"},{"title":"Renormalization Group and Elliptic Homogenization in High Contrast","identifier":"doi:10.1007/s00222-025-01370-9","relationship":"formalizes"}]}