claimroutineinferred_dep

Interior density lower bound by Gaussian inversion

Gives density lower bound

m_X

on the

h

-ball around each center

pointwise density bound feeding the interior energy bound

Claim·§5 Estimating the energy on a fixed fiber·inside propEnergy barrier on a fixed fiber

Statement (paper)

Let

(X,P,Z)

be a center with

|W|\le\gamma

and

|Q|\le1/400

. Then, provided

K\gamma

and

K

are sufficiently large, the ball of radius

h

in the

3n

real spatial coordinates about this center lies in

|W|\le2\gamma

|Q|\le1/100

, and the density at every point of this ball is at least

m_X=c_\gamma(hs)^{-d}\sigma^{-m}e^{-C_2\gamma^2\sigma}|g_T(X)|^2

In plain English

For a center

(X,P,Z)

with

|W|\le\gamma

and

|Q|\le1/400

, and with

K\gamma

and

K

large enough, the

h

-ball around it in the

3n

real spatial coordinates stays inside

|W|\le2\gamma

|Q|\le1/100

. At every point of this ball the density is at least

m_X=c_\gamma(hs)^{-d}\sigma^{-m}e^{-C_2\gamma^2\sigma}|g_T(X)|^2

Why it's here

This gives a pointwise lower bound for the density on a whole ball around each center, in terms of the local value

|g_T(X)|^2

. The proof inverts the Gaussian structure of the density, and the ball stays in the region where the wall-decay and density bounds of the previous claim apply. The lower bound is then integrated over the ball to give the interior lower bound on the energy

\mathcal F(T,\tau)

in the next claim, which leads to .

Classified routine:

A direct pointwise estimate obtained by inverting the Gaussian form of the density from the wave-current construction (prop-current) and checking that the ball stays in the region covered by the bounds of claim-prop-fixed-barrier-2. It is bookkeeping inside the barrier proposition.

Uses

propWave current is positive and divergence-freeclaimCurrent and density bounds with wall decay

Used by

claimInterior energy lower bound via ball quadratic

Figures

Panel (a) draws the fiber in modulus coordinates: the horizontal axis is $|W|$ with tick $w_0$, and the vertical axis is $|Q|=|\Phi|/a$ with ticks $1/20$ and $1/10$. A quarter-ellipse arc labeled $r=0$ runs from $(0,1/10)$ to $(w_0,0)$ and bounds the shaded region $r<0$. A dotted line at height $1/20$ meets the arc, and the part of the arc below it is drawn heavy and labeled "flux wall". A small dashed box near the origin, containing a smaller solid box, is marked (b). Panel (b) enlarges that corner: a dashed rectangle $|W|\le2\gamma$, $|Q|\le1/100$, labeled "Gaussian inversion, $g(Q)=1$", contains a darker solid rectangle $|W|\le\gamma$, $|Q|\le1/400$, labeled "centers". The figure shows that the region where the wall flux lives is separated from the central region where the Gaussian multiplier is inverted. — Figure 1schematicp. 19
The fixed fiber in modulus coordinates. The wave flux through $r=0$ is supported on the heavy arc, where $|Q|\le1/20$ and hence $|W|\ge\sqrt{3}\,w_0/2$ . This separation gives Gaussian decay $e^{-cs/h}$ even for $|v|\le w_0/3$ . In the enlargement (b), once $K\gamma$ is large, the radius- $h$ balls about the marked centers project into the dashed patch. There $|W-v|\le4\gamma$ on the enlarged cap $|v|\le2\gamma$ , so Gaussian inversion costs at most $e^{C\gamma^2s/h}$ . The aperture $\gamma$ is fixed independently of $h$ ; its size relative to $w_0$ is schematic.
What it shows
Panel (a) draws the fiber in modulus coordinates: the horizontal axis is $|W|$ with tick $w_0$ , and the vertical axis is $|Q|=|\Phi|/a$ with ticks $1/20$ and $1/10$ . A quarter-ellipse arc labeled $r=0$ runs from $(0,1/10)$ to $(w_0,0)$ and bounds the shaded region $r<0$ . A dotted line at height $1/20$ meets the arc, and the part of the arc below it is drawn heavy and labeled "flux wall". A small dashed box near the origin, containing a smaller solid box, is marked (b). Panel (b) enlarges that corner: a dashed rectangle $|W|\le2\gamma$ , $|Q|\le1/100$ , labeled "Gaussian inversion, $g(Q)=1$ ", contains a darker solid rectangle $|W|\le\gamma$ , $|Q|\le1/400$ , labeled "centers". The figure shows that the region where the wall flux lives is separated from the central region where the Gaussian multiplier is inverted.
Read from the image by claude-opus-5.5 · confidence 85%
SupportspropEnergy barrier on a fixed fiberclaimCurrent and density bounds with wall decayclaimInterior density lower bound by Gaussian inversionclaimInterior energy lower bound via ball quadraticclaimChoosing gamma and K yields the barrier inequalities

Sources

PaperOpen

Section: §5 Estimating the energy on a fixed fiber
Page: —
Label: —
Line: sections/barrier.tex:170

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Interior density lower bound by Gaussian inversion" rests on prop:current
info
inferred_dep
outline: "Interior density lower bound by Gaussian inversion" rests on claim-prop-fixed-barrier-2