Step5Basket #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-5 analytic basket: the gate, the re-sited gauge, and the defect binder #
Closure.JunctionDischargeStepFiveDisplay.step5GaugeEndpoint_of_correctors_gauge
reduces Closure.Step5GaugeEndpoint to a list of named legs, read at a
per-cube forcing gauge. Closure.StepProducers.step5GaugeEndpoint_closureFamilies_of_legs
discharges, at the closure's own corrector families and at that per-cube gauge,
the seven legs that are statements about those families rather than displays of
the manuscript. This module
- discharges three more legs outright ---
hgate,hmemGaugeandhdefect--- at the gaugefun R omega => 3^nmesh * shellDerivNormSum n (n+h) (triadicCubeShift R) omega; - assembles all ten into
step5GaugeEndpoint_closureFamilies_of_gaugeLegs, which isClosure.Step5GaugeEndpointat the closure families with exactly the residual analytic basket left as binders; - assembles those into
step5GaugeEndpoint_closureFamilies_of_momentLegs, in whichhshellandhgradMare read at the two explicit grid fourth moments the Hoelder step produces.
What is proved #
| leg | content | route |
|---|---|---|
hCdef | 0 <= Cdef at Cdef = step5CrossDefectConst d | |
Step5DefectGauge.step5CrossDefectConst_nonneg | ||
hgate | step5CrossDefectConst d * cgamma^15 <= 2 | |
step5CrossDefectConst_mul_gamma_pow_fifteen_le_two_of_regime: the regime's own C c⋆^{-1} <= E | ||
and cgamma <= E^{-5}, at the d-dependent threshold step5GateConst d = 1 + d^3, exactly the | ||
enlargement device of Closure.ClosureFinalArithmetic | ||
hgauge0 | the gauge is nonnegative | discharged inline by Closure.StepProducers; also |
available here as step5Gauge_nonneg | ||
hmemGauge | the per-cube gauge is L^4 in the sample | memLp_four_step5Gauge: |
LocalizationOscillationDisplay.integrable_shellDerivNormSum_rpow_four on M.P, transported to | ||
(cutoffSampleLaw M) along the measurable embedding | ||
Provider.Stream.measurableEmbedding_cutoffSample_val and Cutoff.map_cutoffSampleLaw_val | ||
hdefect | the per-cube step at the closure's grid | step5CrossDefect_le_step5Gauge: |
Step5DefectGauge.step5CrossDefect_le_meshOscillationCell at R.scale = K - j = nmesh <= n | ||
hD, hN | e.def.w at the two closure families | Closure.ClosureAssembly |
hmemD, hintD, hsampN, hsampG | the four Dirichlet spatial/sample routes | |
Closure.StepProducers | ||
hprod, hgrad0 | the Hoelder split on the grid | |
descendantsAverage_integral_vecNormSq_matVecMul_le: |A_R v_R|^2 <= ||A_R||^2 |v_R|^2, | ||
| Cauchy--Schwarz in the sample at the second moment, then Cauchy--Schwarz on the finite grid | ||
hsampX, hsampS | the two remaining per-cube sample integrabilities | |
integrable_vecDot_matVecMul_of_memLp_four, integrable_vecNormSq_matVecMul_of_memLp_four, from | ||
| the same two fourth-moment legs plus measurability |
The gate is the same device Closure.ClosureFinalArithmetic already uses for
the two regime facts: step5CrossDefectConst d is dimensional and absolute, `E
= 2C/3
andcgamma <= E^{-1}givecgamma^15 <= (2C/3)^{-1}, andC >= 1 + d^3 >= 2 step5CrossDefectConst dcloses it. No smallness of the manuscript is assumed: the threshold is *produced*, and it is consumed only inside`Closure.ClosureRegime`.
The residual basket #
step5GaugeEndpoint_closureFamilies_of_momentLegs still carries, as binders,
exactly the legs that this lane did not reach:
hintP,hsampDef--- two integrability side conditions on the cube and on the sample;hmeasX,hmeasS--- the sample measurability of the two per-cube pairings. Both legs are now proved at the full sigma-algebra, at the closure's own families, asClosure.Step5InputSideConditions.aestronglyMeasurable_step5PairingXand...aestronglyMeasurable_step5PairingS, and it is those that the downstream assembly consumes. They remain binders of this module only because this module sits belowClosure.Step5InputSideConditionsin the import order;hAmem,hvmem--- theL^4sample membership of the per-cube shell and gradient averages;hmemOsc--- theL^4sample membership of the mesh oscillation cell;hosc---e.lower.bound.oscillations, whose re-sited shape is exactlyexists_gamma0_freshShellDirichlet_step5MeshOscillationResited_le_gamma_pow_fifteenand whose own binders (hmem8, the octic grid envelopeE, the recurrence gates) are not discharged here;hshell,hgradM--- the two moment inputse.km.kn.Lpande.nablaw.in.L.eight, read at the two explicit grid fourth moments.
Nothing below papers over any of them. In particular no
Closure.ClosureStep5Input is produced by this module: the residual basket
above is still carried as binders here.
The second reason previously given --- that Closure.ClosureStep5Input "is
quantified over every d with NeZero d, whereas the re-sited oscillation
endpoint. is available only for 2 <= d" --- is obsolete and was never an
obstruction: Closure.ClosureFinal.ClosureStep5Input d is defined as 2 <= d ->., so the 2 <= d restriction of the Step-5 inputs is exactly the
hypothesis that statement supplies. The residual basket, not the dimension
quantifier, is the whole reason this module stops short; and that basket is
itself discharged downstream, in Closure.Step5Input (nine legs) and
Closure.Step5SampDef (the tenth), which together produce
Closure.ClosureStep5Input d for every d with NeZero d.
References #
- ABK26,
e.lower.bound.pre2; the Step-5 estimate;e.nablaw.oscillations;e.lower.bound.oscillations.
The gate Cdef cgamma^15 <= 2 #
The absolute, dimension-dependent threshold at which the manuscript's
standing hypotheses C c⋆^{-1} <= E and cgamma <= E^{-5} already deliver the
Step-5 defect gate. It is the Step-5 analogue of
Closure.closureRegimeConst.
Equations
Instances For
The geometric constant of the per-cube defect step is at most half the threshold.
hgate, from the regime's own antecedents.
Closure.ClosureRegime carries C c⋆^{-1} <= E and cgamma <= E^{-5}. At
the absolute threshold step5GateConst d these already force Cdef cgamma^15 <= 2 for the geometric constant Cdef = step5CrossDefectConst d of the
per-cube step. This is the same enlargement device
Closure.gamma_le_exp_neg_one_of_regime and
Closure.three_mul_switchBudget_le_one_of_regime use, with a d-dependent
threshold in place of an absolute one.
hmemGauge: the re-sited forcing gauge is L^4 in the sample #
Unconditional. L^p membership transports from the shell-sequence law
to the cutoff sample law along the sample inclusion, which is a measurable
embedding pushing the sample law forward onto M.P.
The forcing gauge of e.nablaw.oscillations is L^4 on the shell-sequence
law: its fourth power is integrable by the weak-Orlicz tail
e.nabla.km.kn.infty.
hmemGauge at the re-sited gauge, on the closure's own sample
carrier.
hdefect at the closure's grid #
hdefect at the mesh grid descendantsAtDepth cu_K j.
Every cube of that grid has scale K - j; at nmesh = K - j <= n the per-cube
step, proved in Closure.Step5DefectGauge, is literally the binder, the
forcing gauge being read at each cube's own base point.
The Step-5 endpoint at the closure families, at the re-sited gauge #
Closure.Step5GaugeEndpoint at the closure's own corrector families and
at the per-cube forcing gauge, with nine legs discharged.
This adds, to the seven family legs already discharged by
Closure.StepProducers.step5GaugeEndpoint_closureFamilies_of_legs, the three
legs hCdef, hdefect and hmemGauge, all proved: the gauge is sited at
each cube's own base point, which is exactly what makes hdefect
dischargeable.
What remains are exactly the residual analytic legs listed in the module
docstring. No smallness, no normalization and no bound of ABK26 is assumed
here: hgate is supplied by the caller from
step5CrossDefectConst_mul_gamma_pow_fifteen_le_two_of_regime, i.e. from
Closure.ClosureRegime itself.
hprod: the grid/sample Hoelder split #
Closure.ShellProductControl does the scale bookkeeping once hprod is granted
at some pair (shellMoment, gradMoment). The manuscript's own choice is
Hoelder, which fixes the pair to the two grid fourth moments below; the three
lemmas of this section carry that split out, so that hprod and hgrad0 are
proved and the two moment binders that remain are literally e.km.kn.Lp and
e.nablaw.in.L.eight read on the closure's grid.
The square of a nonnegative L^4 function is L^2.
Cauchy--Schwarz in the sample at the second moment, in the fourth-moment spelling.
Hoelder on the grid at a pair of square roots.
hprod, proved: the grid average of the sample mean of |A_R v_R|^2 is at
most the product of the square roots of the two grid fourth moments, of the
operator norms and of the vector norms. This is the Hoelder step, at the
closure's grid carrier.
hsampS and hsampX from the same two fourth-moment legs #
hsampS, from the two fourth-moment legs and the measurability of the
quantity itself.
hsampX, from the two fourth-moment legs and the measurability of the
quantity itself.
The endpoint at the two grid fourth moments #
Closure.Step5GaugeEndpoint at the closure families, with the Hoelder split
carried out.
Relative to step5GaugeEndpoint_closureFamilies_of_gaugeLegs this discharges
four more legs --- hprod, hgrad0, hsampX and hsampS --- from the two
grid fourth-moment memberships hAmem, hvmem and two measurability side
conditions, and restates hshell and hgradM at the explicit grid fourth
moments the manuscript's Hoelder step produces:
hshellise.km.kn.Lpread as(avsum_ ||(k_{n+h} - k_n)_R||^4)^{1/2} <= h 3^{2 cgamma (n+h)};hgradMise.nablaw.in.L.eightread as(avsum_ |(grad w_D)_R|^4)^{1/2} <= shom_n^{-2} h 3^{2 cgamma (n+h)}.
The residual basket is therefore hintP, hsampDef, hmeasX, hmeasS,
hAmem, hvmem, hmemOsc, hosc, hshell, hgradM.