Proof Dags
Proof dependency graphs mapping theorem relationships across papers.
Sphere Packing — Proof DAG (Cohn–Elkies linear programming, Viazovska's magic functions in $E_8$ and Leech, Radchenko–Viazovska Fourier interpolation, universal optimality, and the Lean formalization)
# Sphere Packing The proof that the $E_8$ and Leech lattices realize the densest sphere packings in $\mathbb{R}^8$ and $\mathbb{R}^{24}$. The program has a clean two-stage structure: **the LP framework** sets up the problem and conjectures the form of the answer; **the modular-form construction** then realizes the conjectured magic functions. ## The arc **Cohn–Elkies (`math/0110009`, 2003)** prove the linear-programming bound: any admissible radial Schwartz $f$ with $f(0)=\widehat{f}(0)$, $f(x)\le 0$ for $|x|\ge r$, and $\widehat{f}\ge 0$ everywhere bounds the sphere-packing center density by $f(0)/(2^n\widehat{f}(0))$. They conjecture (Conjecture 2 / Conjecture 4) that such a *magic function* exists and is sharp in dimensions 2, 8, 24, with roots exactly at the lattice vector lengths. **Viazovska (`1603.04246`, 2016)** constructs the magic function for $E_8$ from weight-3/2 weakly-holomorphic modular forms on the theta group: $g = \frac{\pi i}{8640}a + \frac{i}{240\pi}b$, where $a$ and $b$ are the $+1$ and $-1$ Fourier eigenfunctions built as contour integrals of quasi-modular forms. The Fields-medal result, resolving Cohn–Elkies Conjecture 2 for $n=8$. **CKMRV (`1603.06518`, 2016)** extends Viazovska's template to the Leech lattice in $\mathbb{R}^{24}$ with different modular forms — same eigenfunction architecture, different weights and group. **Cohn–Miller (`1603.04759`, 2016)** studies the structure of the magic functions: a polynomial-times-Gaussian numerical method, the value-and-derivative constraints at $\sqrt{2n}$, Taylor coefficients, and a conjectural energy-minimization reformulation that becomes the next stage of the program. **Radchenko–Viazovska (`1701.00265`, 2017)** abstracts the magic-function construction into a free-standing **Fourier interpolation theorem** on $\mathbb{R}$: even Schwartz functions are uniquely determined by their values at $\pm\sqrt n$ and the Fourier values at $\pm\sqrt n$, with an explicit interpolation basis from modular forms. **Cohn–Kumar (`math/0607446`, 2006)** had earlier developed the universal-optimality framework on spheres and compact two-point homogeneous spaces, and conjectured (Conjecture 32) universal optimality of $E_8$ and Leech. **CKMRV (`1902.05438`, 2019)** proves that conjecture — universal optimality of $E_8$ and Leech for every completely monotonic pairwise energy — via a higher-dimensional interpolation formula (now with derivative data $f'(\sqrt{2n})$), the modular-form annihilator-space machinery on $\mathbb{C}[\mathrm{PSL}_2(\mathbb{Z})]$, and a kernel-positivity reduction verified by computer. **Hariharan–Birkbeck–Lee (`2604.23468`, 2026)** close the loop with the Lean 4 formalization of Viazovska's $E_8$ proof — this DAG's blueprint-validation anchor, included as an arXiv node so the informal-to-formal correspondence is captured directly as an intra-DAG `imports_result` edge. ## Blueprint validation The Lean project `Sphere-Packing-Lean` (kickstarted at EPFL March 2024 by Viazovska and Hariharan; maintained by Birkbeck, Hariharan, Mehta, Lee; completed February 2026 with Math, Inc.'s Gauss autoformalization model assisting the final stages) is the **third blueprint-validation anchor** in the registry, after PFR and PNT+. Project URLs: dim-8 main project at [`thefundamentaltheor3m/Sphere-Packing-Lean`](https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean) with live blueprint at [`thefundamentaltheor3m.github.io/Sphere-Packing-Lean/blueprint/`](https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/blueprint/); ongoing dim-24 extension at [`math-inc/Sphere-Packing-Lean`](https://github.com/math-inc/Sphere-Packing-Lean). The blueprint formalizes Viazovska's $E_8$ proof at fine granularity — **139 nodes** (19 theorems, 17 propositions, 15 corollaries, 54 lemmas, 34 definitions), as verified by fetching the live dep-graph on 2026-05-26. Our extraction of `1603.04246` collapses these to 12 chapter-level theorem nodes (the same ~11× ratio as PFR: blueprint 218 nodes ↔ our 21). The blueprint's "Cohn–Elkies" theorems (Theorem 5.1 / Theorem 5.2) match `math/0110009:thm:2` and `1603.04246:thm:2` verbatim; a full label-by-label correspondence for the remaining Chapter-6 / Chapter-7 nodes (magic-function construction and eigenfunctions) is the analog of the open PFR 16-node audit, and is flagged as an open item. Unique here vs the other two anchors: (i) **the formalization paper is itself an arXiv node in this DAG**, so the informal/formal correspondence shows up directly as cross-paper edges (`2604.23468v2:thm:1` `imports_result` `1603.04246v2:thm:1`); (ii) **the formalization was partly AI-assisted** (Math, Inc.'s Gauss model finished the final verification stages) — directly relevant to AI for Math, since the validation anchor was itself produced by the kind of human–AI workflow this graph infrastructure is meant to support. ## Stats 8 papers extracted (98 theorem- and lemma-level nodes, 95 intra-paper edges), plus 22 cross-paper edges that lay out the program's structural arc (LP conjectures → realized → abstracted → universally generalized → formally verified). No cross-DAG edges: sphere packing is a standalone island in the registry, but the densest island — every paper contributes load-bearing structure (`imports_result`, `proves`, `extends`, `abstracts`, `generalizes`, `uses_mechanism`) into the same connected component. All arXiv IDs verified against the arXiv API (2026-05-26); every per-paper DAG passes the integrity gate.
The Prime Number Theorem: zero-free regions, equidistribution, and the modern frontier — Proof DAG
# The Prime Number Theorem: zero-free regions, equidistribution, and the modern frontier The dependency structure of prime distribution, anchored on the Prime Number Theorem. The classical spine — Riemann's explicit formula $\to$ a zero-free region for $\zeta$ $\to$ PNT with error term $\to$ primes in arithmetic progressions — is pre-arXiv and lives in `manifest.json` under `foundational`. It is the layer with a Lean blueprint (the **PNT+** project), so it doubles as the external ground truth for validating extracted nodes and edges. The arXiv-era spine carries the program in three directions. **Effective / explicit PNT.** Ford (`1910.08205`) builds the Vinogradov–Korobov zero-free region from a "zero detector" (a cotangent-integral identity localizing $-\Re\,\zeta'/\zeta$ over nearby zeros), giving the explicit region $1-\beta \le \frac{1}{57.54(\log|t|)^{2/3}(\log\log|t|)^{1/3}}$. Mossinghoff–Trudgian–Yang (`2212.06867`) re-run Ford's apparatus with sharpened constants — its lemmas *are* Ford's lemmas (the proofs cite "Ford Lemma 2.2", "Ford Lemma 5.1" verbatim) — improving the constant to $55.241$ and the classical-type region to $5.558691$. Platt–Trudgian (`1809.03134`) feed a zero-free region ($R=5.573412$), a verified Riemann Hypothesis up to height $3\times 10^{12}$, and a Pintz-type zero-density estimate into the truncated explicit formula to get a fully explicit bound on $|\psi(x)-x|$. **Equidistribution beyond Bombieri–Vinogradov.** Maynard's large-moduli programme pushes primes-in-APs past the $1/2$ barrier; part III (`2006.08250`, uniform residue classes) is extracted here, parts I & II are shared nodes from the `maynard-small-gaps` DAG. Shao–Teräväinen (`2006.05954`) prove a Bombieri–Vinogradov theorem for nilsequence twists (levels $1/4$, $1/3$, $1/2$) via the Green–Tao equidistribution machinery, with applications to bounded gaps and Chen primes in nil-Bohr sets and Green–Tao in progressions. **Short intervals.** Matomäki–Radziwiłł (`1501.04585`) prove that multiplicative functions have nearly constant average in almost all short intervals — a landmark whose engine is a Parseval bound on a Dirichlet polynomial (built from Halász's theorem and mean/large-value estimates), with corollaries on smooth numbers, Liouville correlations, and sign changes. Part II (`2007.04290`) extends the method to complex-valued functions with the sharp range $\rho<1/3-2/(3\pi)$ and applications to norm-forms. ## The keystone role This DAG joins the analytic-number-theory region. **Cross-DAG → `large-values-zero-density`:** zero-*free* regions (here) and zero-*density* estimates (there) are the two complementary controls on $\zeta$-zeros — Ford's VK region improves Ingham's qualitative region, and Platt–Trudgian's Pintz density estimate is the same Ingham–Pintz mechanism as Starichkova's zero-density route. **Cross-DAG → `maynard-small-gaps`:** Maynard III's equidistributed minorant `provides_input_to` the Maynard–Tao sieve (`1311.4600v3:prop:4.1`), the load-bearing level-of-distribution the sieve consumes; Maynard III is the `companion_result` of Maynard I; and Shao–Teräväinen's nil-Bohr bounded gaps `extends` the Maynard bounded-gaps theorem. ## Validation against the PNT+ blueprint The classical-core layer (PNT via Newman's Tauberian proof, PNT in APs) is formalized in the PNT+ Lean blueprint. As with the PFR cross-check, the blueprint's statement-level dependency graph is the external precision/recall yardstick for our extracted nodes on the PNT spine — and the contrast is the point: the blueprint maps the inside of the classical proof, while this DAG extends outward to the effective-PNT, equidistribution, and short-interval literature the blueprint does not reach. ## Stats 7 papers extracted (143 theorem- and lemma-level nodes, ~20.4/paper — matching the densest peer DAGs; 155 intra-paper edges), plus 17 cross-paper edges (6 cross-DAG). 2 shared nodes reused from `maynard-small-gaps`. All arXiv IDs verified against the arXiv API (2026-05-25); all edges resolve to real nodes; every per-paper DAG passes the integrity gate (node/edge resolution, connected critical path, full layer coverage, KaTeX-clean summaries).
Kakeya / Restriction — Proof DAG
# Kakeya and restriction The Kakeya set conjecture in $\mathbb{R}^3$, its 2025 resolution, and the restriction estimate it sits next to. **Resolution** — Wang–Zahl (`2502.17655`): every Kakeya set in $\mathbb{R}^3$ has Hausdorff and Minkowski dimension $3$. The engine is a two-parameter multiscale induction on assertions $\mathcal{D}(\sigma,\omega)$ / $\mathcal{E}(\sigma,\omega)$ for $\delta$-tube families under the Katz–Tao convex Wolff axioms: base case $\mathcal{D}(1/2,0)$, an equivalence $\mathcal{D}\Leftrightarrow\mathcal{E}$, and a strict-gain step $\mathcal{E}(\sigma,\omega)\Rightarrow\mathcal{D}(\sigma,\omega-g)$ with $g>0$, iterated to the endpoint $\mathcal{D}(0,0)$, which gives the near-extremal volume bound and hence full dimension. **The mechanism** — Guth's survey (`2604.03416`) isolates what powers the strict gain. The hard case is sticky (self-similar) configurations; stickiness forces a grain structure on $U(\mathbb{T})$, the grains give an approximate additive symmetry $A + s(x)y + \tilde s(y)x \approx A$, and that symmetry contradicts Bourgain's discretized sum-product theorem applied across scales (so $\beta_{\mathrm{sticky}}=0$). The non-sticky regime is closed by a high-density lemma that also reduces the general case to the sticky one. **Restriction** — the study guide (`2402.03470`) traces Guth's $L^p$ restriction estimate for the paraboloid in $\mathbb{R}^3$ ($p>3.25$) via polynomial partitioning: a broad–narrow reduction, then an induction on radius splitting into a cellular case (partition by $Z(P)$, polynomial partitioning) and a transverse case bounded by Wongkew's variety-neighborhood estimate. This exposition references multilinear Kakeya as method lineage but does not invoke it directly; Guth's original restriction papers (not yet parsed here) use multilinear restriction for the broad estimate. **Shared structure.** Multilinear Kakeya / restriction (Bennett–Carbery–Tao, `math/0509262`) is the hub of this region. The load-bearing edge into it sits on the decoupling side: the $\ell^2$ decoupling theorem is *proved from* multilinear restriction (recorded in the **decoupling** graph: `1403.5335` thm:6.1 `imports_result` BCT thm:1.16, with Guth's endpoint `0811.2251` improving it). Since multilinear Kakeya is itself a Kakeya-program theorem, that dependency is a genuine cross-program edge through the shared node. On this side the members cluster around the hub: Guth's short proof `1409.4683` `re_derives` it, Guth's restriction `2402.03470` `references` its method lineage, and Wang–Zahl `2502.17655` reach the full conjecture independently (`addresses_same_question`, not a dependency).
Local Langlands after Fargues–Scholze — Proof DAG
# Local Langlands after Fargues–Scholze Fargues–Scholze (`2102.13459`) attach to every reductive $G/\mathbb{Q}_p$ a semisimple $L$-parameter $\varphi_\pi^{\mathrm{FS}}$, via the spectral action of $\mathrm{Perf}(Z^1(W_E,\widehat{G}))$ on the category $D_{\mathrm{lis}}(\mathrm{Bun}_G)$ of $\ell$-adic sheaves on the stack of $G$-bundles, with the dual group produced by geometric Satake on the $B_{\mathrm{dR}}^+$-affine Grassmannian. The map is unconditional but a priori abstract: not known to equal the classical correspondence, and its categorical refinement (Fargues' conjecture) is open. This graph is the work that pins it down. **Compatibility** — Hamann (`2109.01210`): $\varphi^{\mathrm{FS}}$ agrees with Gan–Takeda for $\mathrm{GSp}_4$ and Gan–Tantono for the inner form $\mathrm{GU}_2(D)$; for supercuspidal parameters ($L/\mathbb{Q}_p$ unramified, $p>2$) the cohomology $R\Gamma_c(G,b,\mu)[\pi]$ is middle-degree concentrated. Route: basic uniformization of abelian-type Shimura varieties (Shen, Hansen) + a simple-trace-formula globalization, localized at a Hecke maximal ideal. **Endoscopy** — Kazhdan–Varshavsky (`2503.00621`): elliptic FS $L$-packets satisfy $\mathcal{E}$-stability, giving an endoscopic decomposition $\Theta(G(F)) = \bigoplus_{\mathcal{E}} \Theta_{\mathcal{E}}(G(F))$; the key input ($K_0$ of compact FS sheaves $\cong$ the packet character space) is the FS spectral action. Extended to arbitrary coefficient fields by Galois descent. **Categorical conjecture** — Fu (`2504.13869`) verifies the categorical equivalence for depth-zero regular supercuspidals via the spectral action on the Whittaker generator; Nguyen (`2505.10724`) decomposes $D_{\mathrm{lis}}^{[C_\varphi]}(\mathrm{Bun}_G)$ along $\mathrm{Irr}(S_\varphi)$, produces the predicted Hecke eigensheaves, and reads off torsion in $\mathrm{GL}_n$ Rapoport–Zink cohomology. **Independence of $\ell$** — Scholze (`2501.07944`): a motivic refinement ($\mathcal{D}_{\mathrm{mot}}(\mathrm{Bun}_G)$, motivic geometric Satake $\mathrm{Sat}_G^I \simeq \mathrm{Rep}(\widehat{G}^I)$) proves $\varphi_\pi^{\mathrm{FS}}$ is independent of $\ell$ and $\iota$ — FS Conjecture I.9.5. The root `2102.13459` is shared with the **perfectoid-spaces** graph, where it is the terminus of the diamonds / $p$-adic-Hodge machinery; here it is the root. Edges into it are recorded with the exact FS theorem each downstream result cites (e.g. Hamann's Thm 3.6 = FS I.9.6; Kazhdan–Varshavsky repeat FS IX.6.1 verbatim).
Large Values, Zero Density, and the Riemann Zeta Function — Proof DAG
# Large values of Dirichlet polynomials and zero density The classical pipeline of multiplicative number theory: exponent pairs / van der Corput bounds give the growth exponent $\mu(\sigma)$ of $\zeta(\sigma+it)$; $\mu(\sigma)$ feeds large-value estimates $\mathrm{LV}(\sigma,\tau)$ for Dirichlet polynomials; these give zero-density estimates $A(\sigma)$ (bounds on $N(\sigma,T)$); which yield primes in short intervals. **Two engines, same targets.** Bourgain (`1408.5794`) routes $\ell^2$ decoupling through the $\zeta$-curve to a new exponential-sum bound, giving $|\zeta(\tfrac12+it)| \ll t^{13/84+\varepsilon}$. Guth–Maynard (`2405.20552`) replace the Fourier input with a singular-value / trace inequality, proving large-value estimates that give $A(\sigma) \le \tfrac{15}{3+5\sigma}$ and primes in intervals of length $x^{17/30+\varepsilon}$ — the first improvement on Ingham–Huxley in the relevant range in decades. **Synthesis.** Tao–Trudgian–Yang (`2501.16779`) catalogue the whole web — new exponent pairs $\to \mu(\sigma) \to \mathrm{LV}(\sigma,\tau) \to A(\sigma) \to$ additive energy — recovering the classical bounds and Guth–Maynard and sharpening the Heath-Brown and Bourgain zero-density theorems. Guth's survey (`2503.07410`) places the large-value problem across number theory, restriction theory, and complexity (the Schatten/trace method, SOS and Kakeya barriers). **Converse and exits.** Matomäki–Teräväinen (`2403.13157`): zero-density bounds *imply* large-value estimates (the reverse implication), and a stronger density hypothesis gives primes in intervals of length $(\log X)^{2+\varepsilon}$. Starichkova (`2411.01845`) traces the zero-density $\to$ prime-gaps exit (Ingham, Huxley, Baker–Harman). **Cross-graph.** Shares the nodes `1408.5794` and `2405.20552` with the **bourgain-demeter-decoupling** graph: this is the decoupling $\to$ $\zeta$-growth descent — decoupling feeds the exponential-sum bounds here. A soft thematic adjacency to **maynard-small-gaps** (Maynard works in both the bounded-gaps sieve and the prime-distribution programs, which are logically disjoint).
Fourier Decoupling — Bourgain–Demeter ℓ² Decoupling Proof DAG
# Fourier decoupling The Bourgain–Demeter $\ell^2$ decoupling theorem, its roots in multilinear Kakeya, and its number-theoretic consequences. **Main theorem** — Bourgain–Demeter (`1403.5335`): for a compact hypersurface with nonzero Gaussian curvature, the $\ell^2$ decoupling inequality holds in the full conjectured range $2 \le p \le \tfrac{2(n+1)}{n-1}$. Proof structure: a wave-packet decomposition and parabolic rescaling reduce the linear inequality to a multilinear one (the linear-vs-multilinear reduction, thm:5.3), and the multilinear estimate is supplied by the Bennett–Carbery–Tao multilinear restriction/Kakeya inequality. **Kakeya foundation.** Bennett–Carbery–Tao (`math/0509262`) prove near-optimal multilinear Kakeya and restriction by heat-flow monotonicity (the Loomis–Whitney / induction-on-scales mechanism). Guth gives an endpoint version (`0811.2251`) and a short proof (`1409.4683`). This is the geometric input the decoupling theorem imports. **Vinogradov consequence.** Decoupling for the moment curve yields the main conjecture in Vinogradov's mean value theorem (`1512.01565` and downstream). The graph records the *parallel* proof: Wooley's efficient congruencing (`1401.3150`) proves the same theorem by a $p$-adic iteration, with no logical dependency on decoupling — a `parallel_result` edge between two structurally unrelated proofs of one theorem. **Cross-graph.** Shares `math/0509262` with the **kakeya-restriction** graph (multilinear Kakeya is foundational to both programs — and is also the input to Guth's restriction estimate there). Shares `1408.5794` (Bourgain's decoupling $\zeta$-bound) and `2405.20552` (Guth–Maynard) with the **large-values-zero-density** graph: decoupling feeds the exponential-sum bounds that drive zero-density estimates for $\zeta$.
Perfectoid Spaces — Scholze Program Proof DAG
# Perfectoid spaces and prismatic cohomology Scholze's perfectoid program and the $p$-adic Hodge / prismatic theory it grew into. **Foundations.** Scholze (`1111.4914`) defines perfectoid spaces and the tilting equivalence $X \leftrightarrow X^\flat$ between characteristic-$0$ and characteristic-$p$ perfectoid algebras, proving the weight-monodromy conjecture in new cases and the almost-purity theorem. Kedlaya–Liu (`1301.0792`) build relative $p$-adic Hodge theory on this base. **Integral $p$-adic Hodge theory.** Bhatt–Morrow–Scholze (`1602.03148`, then THH-theoretic `1802.03261`) construct the $A_{\inf}$-cohomology comparing étale, de Rham, and crystalline cohomology of a smooth formal scheme over $\mathcal{O}_{\mathbb{C}_p}$, controlling torsion. **Prismatic cohomology.** Bhatt–Scholze (`1905.08229`) introduce prisms and prismatic cohomology, unifying the integral $p$-adic cohomology theories; Bhatt–Lurie (`2201.06120`) give the absolute (Cartier–Witt-stack) version, Drinfeld (`2005.04746`) the prismatization, and Anschütz–Le Bras (`1907.10525`) prismatic Dieudonné theory for $p$-divisible groups. **Diamonds and the curve.** Scholze (`1709.07343`) develops the étale cohomology of diamonds and the six-functor formalism; with Weinstein (`1211.6357`) the moduli of $p$-divisible groups and the Fargues–Fontaine curve. These are the geometric substrate for `2102.13459`. **Terminus: local Langlands.** Fargues–Scholze (`2102.13459`) geometrize the local Langlands correspondence — importing étale cohomology of diamonds, the FF-classification, and the BMS/prism inputs. This node is **shared with the langlands-local graph**, where it is the root rather than the terminus: the handoff from $p$-adic geometry into the Langlands program.
Bounded Gaps Between Primes — Maynard-Tao Sieve Proof DAG
# Bounded gaps between primes The Goldston–Pintz–Yıldırım $\to$ Zhang $\to$ Maynard–Tao arc, built on the multidimensional Selberg sieve. **Sieve precursors.** GPY (`math/0508185`, and GPY-I `0710.2728`) prove $\liminf_n (p_{n+1}-p_n)/\log p_n = 0$ via a one-dimensional Selberg-sieve weight on admissible tuples, conditional on a level of distribution $\theta > 1/2$ for bounded gaps. **Maynard's sieve** — Maynard (`1311.4600`): a multidimensional sieve weight removes the level-of-distribution barrier and proves, *unconditionally*, $\liminf_n(p_{n+1}-p_n) \le 600$, and for every $m$, $\liminf_n(p_{n+m}-p_n) \ll m^3 e^{4m}$ — bounded gaps for arbitrarily long blocks, qualitatively new beyond GPY/Zhang. Critical path: the $k$-dimensional sieve optimization (`thm:1.3`) $\to$ the diagonalized quadratic forms $S_1, S_2$ (`prop:4.1/4.2`) $\to$ explicit eigenvalue bounds (`lem:5.1`, `lem:6.1/6.2`). **Polymath.** Polymath8b (`1407.4897`) pushes the unconditional bound to $246$ and optimizes the variational problem; Polymath8a (`1402.0811`) is the Zhang-side level-of-distribution improvement (Type I/II/III estimates via algebraic exponential sums). **Consequences.** Pintz (`1305.6289`): Polignac numbers have positive lower density, and the limit set of normalized gaps contains an interval. Related extensions to gaps in dense sequences and prime tuples. This program is logically disjoint from the prime-distribution / zero-density program (see **large-values-zero-density**) despite the shared Maynard authorship — a thematic, not load-bearing, adjacency.
Navier-Stokes Blowup and Non-Uniqueness Proof DAG
# Navier–Stokes: blowup and non-uniqueness Two intertwined programs on the 3D Navier–Stokes and Euler equations — finite-time singularity for model/averaged equations, and non-uniqueness of weak solutions by convex integration — plus the ill-posedness and conditional-regularity results around them. **Averaged / model blowup.** Tao (`1402.0290`) builds an averaged Euler bilinear operator (same energy identity and scaling as Euler) with Schwartz data and no global mild solution — finite-time blowup for an equation obeying the supercritical scaling, the central "barrier" result. The mechanism is a delayed abrupt energy transition iterated across scales. Dyadic and shell models realize the same idea concretely: Katz–Pavlovic-type chains (`math/0410380`) and Cheskidov's dyadic blowup for $\alpha < 1/3$ via a Lyapunov argument (`math/0601074`), with the matching global-regularity side at the optimal dissipation $\int ds/(s\,g(s)) = \infty$ (`0906.3070`, `1407.6734`). **Convex-integration non-uniqueness.** Buckmaster–Vicol (`1709.10033`) prescribe the energy profile of a weak solution; the wild-solution gluing / $h$-principle machinery (`1809.00600`) and its sharp Ladyzhenskaya–Prodi–Serrin endpoints (`2009.06596`, sharp at $L^p_t L^\infty_x$, $p<2$; `2412.09637`) follow. Recent work pushes to Leray–Hopf solutions: non-uniqueness with force (`2112.03116`), in $C_t L^2(\mathbb{R}^3)$ (`2412.10404`), in $\mathrm{BMO}^{-1}$ with two distinct global *smooth* solutions (`2503.14699`), infinitely many suitable Leray–Hopf solutions from one datum (`2509.25116`), and 2D smooth non-uniqueness (`2602.19074`). **Ill-posedness and blowup scenarios.** Strong ill-posedness / norm inflation for Euler in $H^s$, $0<s<5/2$ and NSE in $H^s$, $0<s<1/2$ (`2404.07813`) and in Besov spaces (`2504.08288`); Type I blowup constructions (`2511.09556`); conditional exclusion of Type II singularities under LPS-type bounds (`2402.13229`, `2507.08733`); and a PINN-based computational search for unstable self-similar Euler singularities (`2509.14185`). **Cross-graph.** Self-contained in the registry; the dyadic-model nodes (`math/0410380`, `math/0601074`) connect the PDE-blowup and infinite-dimensional-dynamics literatures.
Polynomial Freiman-Ruzsa Conjecture Proof DAG
# Polynomial Freiman–Ruzsa The proof of the Polynomial Freiman–Ruzsa conjecture (Marton's conjecture) over $\mathbb{F}_2^n$, its entropic method, and downstream work. **Main theorem** — Gowers–Green–Manners–Tao (`2311.05762`): if $A \subseteq \mathbb{F}_2^n$ has $|A+A| \le K|A|$, then $A$ is covered by at most $K^{12}$ translates of a subgroup $H$ with $|H| \le |A|$ — polynomial dependence on $K$, the conjectured form. The proof is entropic: it works with the Ruzsa distance $d[X;Y]$ between random variables and runs a "$\tau$-functional" descent that produces a subgroup from a near-minimizer. **Method and improvement.** The generalized Ruzsa equivalences between sumset and entropic inequalities (`2312.11017`) underpin the translation. A sharpening (`2404.09639`) gives entropic PFR with constant $8$ and Marton's conjecture with $C = 9$. This proof was the object of Tao's 2023 Lean formalization (the "blueprint"). **Extensions.** Function-field / general-torsion PFR (`2501.11580`); approximate-group structure ($\varepsilon$-approximate groups, `2406.10872`); the quasi-polynomial covering bound $\exp(C_\varepsilon \log(2K)^{1+\varepsilon})$ (`2512.11217`); and applications of the entropic method to randomness extractors for sumset sources (`2405.10297`) and to Reed–Muller capacity (`2411.13493`). Self-contained in the registry (no current cross-graph edges); included as the additive-combinatorics anchor and the worked counterpart to the PFR Lean blueprint.