PrincipalResponseLamWire #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
NOTE: this module is an ordinary Provider helper / conditional A. The binder inventories below are informal descriptions only.
The lower-ellipticity gauge on the good event, and the per-cube display with #
the shell size and the ellipticity budget both supplied #
Source displays in ABK26:
l.approximate.recurrence.formula(label), Step 3;- the gauge-switch chain, whose Young remainder is absorbed;
e.lower.bound.principal.one.pre(label; display);- The ellipticity budget quoted from
e.nablaw.in.L.eight(label; display); e.good.local.events(label; display), instantiated ascQ_z:= cQ(n, m-h, z);e.cg.ellip.lower(label), the source of the constantCcg;e.recurrence.params(label; display);e.Pz.def(label; display) ande.def.w(label).
What this module supplies #
Two things.
The lower-ellipticity gauge is positive, with nothing assumed.
lambdaSq_coefficientCutoffTriadicCoeffFamily_posis0 < lambda_{3/8,2}(z+cu_n; a_{m-h})at every sample, for every cube and every scale. The good event is not used: CoarseGraining'sCh02.lambdaSq_posis positive for every coefficient family at every admissible exponent pair, and3/8 > 0,q = 2 >= 1are admissible. The binder thatApproximateRecurrence.PrincipalResponseSwitchActualPerCubeandApproximateRecurrence.PrincipalResponseSwitchActualDisplaycallhlam0asks for exactly this proposition restricted to the samples of the good event, so it is supplied here in a strictly stronger unconditional form.The composed per-cube display. The final theorem of this module,
exists_constant_principalEnergy_bound_of_centering, is the display at the manuscript's own loadP_zofe.Pz.def, in which none ofhswitch,hshell,hellip,hellipInt,hlam0is a binder:hswitchwas already discharged insideApproximateRecurrence.PrincipalResponseSwitchActualDisplay;hlam0is discharged from item 1;hshellis discharged fromApproximateRecurrence.PrincipalResponseCentre.shell_hypothesis_of_centeringConst_aeatK = centeringConst d = d^3;hellipis discharged fromexists_const_descendantsAverage_integral_switchEllipLoad_principalPz_le;hellipIntis discharged from the pointwiseX <= 1/2 + X^2/2together with the two per-cube data conditionshmeasRandhintR, exactly as inApproximateRecurrence.PrincipalResponseEllipBudget.
The almost-sure quantifier, and why the chain is rebuilt here #
shell_hypothesis_of_centeringConst_ae delivers the shell-size bound almost
surely on the cutoff sample law, because the transfer between the measurable
representative of lambda_{1/8,2} carried by goodLocalEvent and the frozen
lambda_{3/8,2} (Provider.BadEvents.lambda_transfer_ae) is almost sure and
no pointwise information about the representative exists. The proved
switchCubeEnergy_indicator_le_ae and the proved display consumer take that
bound pointwise on the good event, so they cannot consume it.
The two intermediate steps of this module are therefore the same two proved
statements with the shell-size binder weakened from pointwise to almost sure
and with hlam0 removed; both are private, both use only public proved
inputs (blockVecDot_coarseBlockMatrix_le_switch_absorbed_cube,
responseSensitivityConst_mul_gradientW1Infinity_centeredFreshShell_le_ae,
centeredFreshShellUnitCube_shift, freshShellCubeAverage_skew,
three_halves_switch_excess_le_gamma_pow_six_of_model,
gridSwitchDiscount_eq_rpow_recurrenceGap and the-generalized display
descendantsAverage_integral_goodEventEnergy_le_annealedCube_family), and
neither weakens the conclusion. No proved file is edited.
The manuscript's S, and what survives of the threshold #
The manuscript's weight in the ellipticity load is S = shom_{m-h}, and that
is the weight used here: shellSizeThreshold M Ccg (centeringConst d) (m-h) <= shom_{m-h} is the residual data condition that
ApproximateRecurrence.PrincipalResponseSwitchActualShellSize records. It is
not carried raw. Written out it is
d^6 Ccg^{-1} shom_{m-h-1} / (2 C_sens^2) <= shom_{m-h} ,
and shellSizeThreshold_centeringConst_le_sigmaBar reduces it, using the
proved one-scale comparison shom_{j} <= 4 shom_{i} for j <= i <= m0
(Provider.Multiscale.sigmaBar_le_four_mul_sigmaBar, which reads the frozen
induction state Algsuperdiff.Frozen.Section3.inductionState already carried
by the consumer) at j = m-h-1, i = m-h, to the single scale-free inequality
2 d^6 <= Ccg . C_sens^2 .
That inequality is the one surviving data condition of the composition. It
involves no sample, no scale and no corrector: it is a numerical lower bound on
the constant C_{e.cg.ellip.lower} in terms of the dimension and the joint
sensitivity constant C_sens = sensitivityConstMax d of l.J.sensitivity. It
is a statement about the data of the recurrence of the same kind as
e.cg.ellip.lower itself, it is a hypothesis and never a derived fact, and it
is not a step of the manuscript's proof. Nothing else about Ccg is assumed:
0 < Ccg is derived from it, because d >= 1 already makes the left side at
least 2 while C_sens^2 > 0.
The complete census of the final theorem's binders #
Parameter gates and typing data: hd (2 <= d); M.gamma <= gamma0; the
frozen induction state; 0 < hgap, m - hgap <= m0, hgap <= 6 cstar cgamma^{-1} (/7183), 10^10 cgamma^{-1} <= K - m (e.recurrence.params); the
two direction bounds |e|, |e'| <= 1; recurrenceGapMultiplierFloor <= a and
the mesoscale identification; m - hgap <= highScale; the free integers n,
highScale; the free reals Ccg; the two corrector families wD, wN
together with hwD, hwN, which say that they solve the two problems of
e.def.w; the free family W.
Data conditions: hccg (the threshold residue described above); hmeasR and
hintR (per-cube measurability of the load and integrability of its square,
the two data conditions of the budget); hgoodInt and hcubeInt (the two
remaining integrability families).
Residuals of the manuscript's own text: hindep, the independence replacement;
hbudget, the numerical smallness in which "increasing M in
e.cgamma.constraints if necessary" is made quantitative.
Deferred obligations, named. The earlier sentence here -- "No binder of the final theorem is a step of the manuscript's proof" -- was false as written and is withdrawn. The exact position is:
hindepis the conclusion of the independence sentence, not a premise of it: it asserts the equality, cube by cube, of the expectation of the gauge-conjugated coarse quadratic form with the annealed quadratic form at a free familyW. It is a deferred proof obligation of this module, it is carried as a caller-supplied hypothesis, and it is discharged nowhere in this module or in any module of its import cone.hbudgetis a numerical step of the manuscript's own argument ("increasingMine.cgamma.constraintsif necessary") rather than a source premise. It is a binder here only; it is discharged one module downstream, inApproximateRecurrence.PrincipalResponseBudgetWire, by shrinking this theorem's own existential thresholdgamma0.- the four measurability and integrability data conditions
hmeasR,hintR,hgoodInt,hcubeIntare conditional A obligations of this provider helper. They are not premises of the pinned source statement and are not discharged here.
Every other binder is parameter data, typing data, a standing gate of
e.recurrence.params //7183, the numerical gate 2 d^6 <= Ccg C_sens^2, a
direction bound, or the e.def.w solution property of the two corrector
families.
The 3/2 #
The switch factor carried through is the honest 1 + (3/2) Delta rather than
the printed 1 + Delta, declared by
ApproximateRecurrence.PrincipalResponseSwitchActualPerCube; it enters only
through hbudget, unchanged.
Main results #
exists_constant_principalEnergy_bound_of_centering
References #
- ABK26, (Step 3 of
l.approximate.recurrence.formula, label);e.lower.bound.principal.one.pre(label; display); quotinge.nablaw.in.L.eight(label);e.good.local.events(label; display);e.cg.ellip.lower(label);e.recurrence.params(label; display);e.Pz.def(label);e.def.w(label).
The lower-ellipticity gauge is positive, unconditionally #
hlam0, in a strictly stronger unconditional form.
The frozen lower multiscale ellipticity lambda_{3/8,2}(z+cu_n; a_r) of the
cutoff coefficient family is strictly positive at every sample, for every cube
and every cutoff scale.
Unconditional: no caller-supplied proposition enters. The binder hlam0 of
ApproximateRecurrence.PrincipalResponseSwitchActualPerCube is the restriction
of this statement to the samples of the good event, so it is supplied by
fun _ _ omega _ => lambdaSq_coefficientCutoffTriadicCoeffFamily_pos M R r omega.
The per-cube switch with the shell size taken almost surely #
The closing line, cube by cube and almost surely, with the shell-size input
weakened to the almost-sure form in which
ApproximateRecurrence.PrincipalResponseCentre supplies it, and with hlam0
discharged from lambdaSq_coefficientCutoffTriadicCoeffFamily_pos.
This is the proved switchCubeEnergy_indicator_le_ae with one binder removed
and one binder weakened; the conclusion is unchanged.
The display consumer with the shell size taken almost surely #
The threshold comparison of
ApproximateRecurrence.PrincipalResponseSwitchActualShellSize, at the
manuscript's own S = shom_{m-h} and at K = centeringConst d.
Written out, shellSizeThreshold M Ccg (centeringConst d) lowScale <= shom_{lowScale} is
d^6 Ccg^{-1} shom_{lowScale-1} / (2 C_sens^2) <= shom_{lowScale} ,
and the proved one-scale comparison shom_j <= 4 shom_i for j <= i <= m0
reduces it to the scale-free 2 d^6 <= Ccg C_sens^2.
: this statement holds only under the propositions supplied by its binders --
hstate, the frozen induction state; hlow, the reading-scale gate lowScale <= m0; and hccg, the numerical lower bound on the constant of
e.cg.ellip.lower (label). It is a provider A, not a source-facing frozen
declaration.
The composed consumer #
The good-event energy display at the actual cutoff carrier, with the switch, the lower-ellipticity gauge, the centered-shell size and the ellipticity budget all supplied.
Every object is the manuscript's own: the grid is the triadic descendants of
cu_K at a free depth j, the sample carrier is Cutoff.CutoffSample d under
(Cutoff.cutoffSampleLaw M).toMeasure, the event is the per-cube cQ_z = cQ(n, m-h, z) through principalBadEvent M Ccg. (m-h), the load is P_z of
e.Pz.def built from a sample family of solutions of e.def.w, and the weight
is S = shom_{m-h}.
None of hswitch, hlam0, hshell, hellip, hellipInt is a binder; the
module docstring names the producer of each and gives the complete census of the
binders that remain.
hd-- the paper-wide2 <= d;M.gamma <= gamma0, and the induction stateAlgsuperdiff.Frozen.Section3.inductionState M m0 Eind;0 < hgap,m - hgap <= m0,hgap <= 6 cstar cgamma^{-1}(/7183) and10^10 cgamma^{-1} <= K - m(e.recurrence.params);- the two direction bounds
vecNorm e <= 1,vecNorm e' <= 1; 2 d^6 <= Ccg C_sens^2-- the one surviving data condition, a numerical lower bound on the constant ofe.cg.ellip.lower(label) described in the module docstring;0 < Ccgis derived from it;hle : m - hgap <= highScale, the scale ordering of the switch;- the two solution families
hwD,hwNofe.def.w; hmeasR,hintR-- the two per-cube data conditions of the budget;hgoodInt,hcubeInt-- the two remaining integrability families;hindep-- the independence replacement;hbudget-- the numerical smallness in which "increasingMine.cgamma.constraintsif necessary" is made quantitative, at the produced constantCell.
It is a provider A, not a source-facing frozen declaration; it does not derive
e.lower.bound.principal.one.pre or any sub-step of
l.approximate.recurrence.formula.
Reaches exactly the one frozen theorem
Algsuperdiff.Frozen.External.calderon_zygmund, a proved external.