ConclusionAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The layer series of p.bfA.multiscalebound, Step 3, at the corrected density #
ABK26, proof of Proposition p.bfA.multiscalebound, Step 3. After the
per-layer estimates are in place the manuscript sums over the Whitney layer
index k,
sum_k 3^{-k} ( C 3^{gamma (k + h_k)}
+ C 3^{2 b (k + h_k)} ( bad density of layer k ) )
<= C 3^{gamma (hsep + k_0)} ( 1 + 3^{2 b (hsep + k_0)}
( exp(-c E^{-2} gamma^{-1}) + 3^{-k_0/2} ) ) ,
and then collapses the k_0-dependent factor.
What changes against the printed Step 3 #
l.bad.cubes.density is available here only in its mass form,
Provider.Whitney.sum_cubeMassRatio_badFamilyLayer_le: the bad mass of layer
k relative to cu_m. The printed Step 3 weights that quantity by the
layer's own mass fraction 3^{-k} a second time, and with only the mass form
the resulting k-sum of the exp(-c E^{-2} gamma^{-1}) leg diverges.
Concretely, layerContrib below weights
- the good leg by the layer's own mass
Mass k(bounded byCmass 3^{-k}), and - the collar leg by the bad mass
Bad kitself -- no second3^{-k}-- usingBad k <= min{Cmass 3^{-k}, eps + 3^{-(k + h_k)/2}} <= sqrt(Cmass) 3^{-k/2} (eps + 3^{-(k+h_k)/2})^{1/2}.
The 3^{-k/2} that survives degrades the series ratio from the printed
3^{-3/4} to 3^{-1/4} (three_rpow_layerQuantity_collar_decay) and forces the
square-root collapse k0_sqrt_collapse with its exponent 1/36 in place of the
printed 1/4. Both are in Provider.Multiscale.ConclusionArithmetic.
The layer-mass A input and its downstream producer #
LayerMassBound m hn Cmass -- "the Whitney layer k carries mass at most
Cmass 3^{-k} inside cu_m" -- is not proved in this file and is carried as
an explicit A hypothesis wherever it is needed. It is a purely combinatorial
statement about Provider.Whitney.whitneyLayer: the layer-k cubes sit under
the depth-(k-1) descendants of cu_m that touch ∂cu_m, of which there are
at most 2 d 3^{(k-1)(d-1)} out of 3^{d(k-1)}, so the expected constant is
Cmass = 6 d. The downstream file LayerMass.lean now proves and applies
this bound at that constant. The declarations here retain the abstract input
and therefore remain conditional; the downstream discharge is not a premise of
the source statement and does not turn this file into a node closure.
What is not here #
In this file, the 3^{gamma hsep} prefactor reduction stops after its
deterministic half's display three_rpow_le_two_add_indicator (in
ConclusionArithmetic), and the bridge from the manuscript's 3^{gamma hsep}
to the proved tail Provider.Percolation.isBigOWith_gammaSigma_three_rpow_hsep
(which is stated at 3^{b hsep}, at the amplitude hsepAmplitude sigma b
rather than the printed 1) is three_rpow_gamma_hsep_le_three_rpow_b_hsep.
The remaining Orlicz half -- e.indc.O.sigma for the indicator and
e.multGammasig for the product -- is assembled only in later multiscale
providers.
References #
- ABK26,
p.bfA.multiscalebound, Step 3.
The Whitney layer quantity k + h_k #
ABK26's layer quantity k + h_k as a real, at the proved scale profile
Provider.Whitney.whitneyScaleSeq (`h_k = ceil(b (1-b)^{-1} k) + hsep
- k_0`).
Equations
- Algsuperdiff.Section3.Provider.Multiscale.layerQuantity b hs k₀ k = ↑k + ↑(Algsuperdiff.Section3.Provider.Whitney.whitneyScaleSeq b hs k₀ k)
Instances For
Every Whitney layer sits above the tuning scale: k + h_k >= k_0.
Slow growth of the layer quantity (e.hn.def summed): from
h_k = ceil(b (1-b)^{-1} k) + hsep + k_0 and ceil t < t + 1,
k + h_k <= (1-b)^{-1} k + (hsep + k_0 + 1).
The two layer decays #
The printed layer decay. For alpha >= 0 with 4 alpha <= 1 - b, the
layer mass 3^{-k} beats the growth 3^{alpha (k+h_k)} at the printed rate
3^{-3k/4}. Applied at alpha = gamma (the good leg of
e.good.simplex.consequence) and at alpha = 2 b (the collar amplification of
e.bounds.on.slopes.when.bad).
The corrected collar decay. After the Cauchy-Schwarz step only
half of the layer mass, 3^{-k/2}, is available against the collar
amplification 3^{2 b (k+h_k)}, and the surviving ratio is 3^{-1/4} rather
than the printed 3^{-3/4}. The hypothesis 9 b <= 1 is exactly what
4 (2 b) <= 1 - b demands -- the same gate as k0_sqrt_collapse.
The per-layer contribution #
The printed Step 3 puts an extra 3^{-k} in front of the collar leg shows it
is not available.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The termwise bound at the density. Each layer contributes at most an
explicit constant times (3^{-1/4})^k; the collar constant carries (eps + 3^{-k_0/2})^{1/2}, exponentially small in k_0.
The layer series converges at the ratio 3^{-1/4}.
The Step-3 payload #
Crucially it carries no 3^{2 b k_0} — the load-bearing property of this constant.
Equations
Instances For
sum_k (layer k) <= C ( 3^{gamma hsep} ( 1 + 3^{2 b hsep} exp(-k_0/36) ) ) ,
with C = layerSumConst free of k_0 in its 3^{2b(.)} factor. Against the
printed display the only differences are the two recorded: the collapse
exponent 1/36 in place of 1/4 (absorbed by relabelling c in the
manuscript's own k_0 := c E^{-2} gamma^{-1}) and the absolute constant
inflation geomSeriesInflation from the ratio change 3^{-3/4} |-> 3^{-1/4}.
The hypothesis hεk0 : eps <= exp(-k_0) is the manuscript's selection
k_0 := c E^{-2} gamma^{-1} read against the density constant.
Instantiation at the proved Whitney carriers #
l.bad.cubes.density at the layer quantity. The proved mass form
Provider.Whitney.sum_cubeMassRatio_badFamilyLayer_le, with its threshold
rewritten at k + h_k = layerQuantity and in the exponent convention that
layerContrib_le consumes.
The bridge to the proved e.hsep.tails #
This is the gamma <= b step.