PrincipalResponseBudgetWire #
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 Young-remainder smallness, supplied rather than assumed #
Sources in ABK26:
- The sentence "Therefore, by independence of
bfA_{m-h}andG_{-(h)_{z+cu_n}} P_z(the latter is a function ofk_m - k_{m-h}), increasingMin\eqref{e.cgamma.constraints}if necessary,"; e.cgamma.constraints(label; display), which readscgamma <= E^{-5}andE >= M cstar^{-1}"for a constantM = M(d) < inftyto be determined below";e.recurrence.params(label; display);e.lower.bound.principal.one.pre(label; display), the display the consumer produces.
What this module supplies #
One bridge and one consumer.
principalSwitchLoadConst_mul_gridSwitchDiscount_mul_le_half_gamma_pow_sixturns the numerical smallness
into the exact proposition thatC_load(d) . (3/2) . Cell . cgamma <= 1/2ApproximateRecurrence.PrincipalResponseLamWirebinds ashbudget,
at the manuscript's own mesoscaleC_load(d) . ( (3/2) Delta ) . Cell <= cgamma^6 / 2 , Delta = gridSwitchDiscount cu_K j (m-h) ,n = m - h - a ceil|log_3 cgamma|.
exists_smallCoupling_principalEnergy_bound_of_centering
is the direct successor and consumer of PrincipalResponseLamWire's
exists_constant_principalEnergy_bound_of_centering,
with hbudget gone and every other binder unchanged, in the same order,
with the same types. Nothing replaces it: no binder is added, and the two
binders W and hindep that the consumer also carries are left exactly as
they were.
The smallness is discharged by shrinking the theorem's own already-existential
threshold gamma0. PrincipalResponseLamWire produces a pair
(Cell, gamma0); this module keeps that Cell and returns the smaller
threshold
min gamma0 ( (1/2) / ( C_load(d) . (3/2) . Cell ) ) ,
which is positive, still at most 1/4, and at most gamma0.
The implication runs in one direction only, and this is the direction:
every model satisfying the new, smaller threshold M.gamma <= min gamma0 ((1/2) / (C_load(d). (3/2). Cell)) also satisfies the old threshold
M.gamma <= gamma0. Hence PrincipalResponseLamWire's theorem is
available at every model this theorem quantifies over, and at those models
the smallness holds by construction. The converse is false, and the cost is
recorded rather than hidden: the statement produced here is applied at
fewer models than the statement it re-states, not at the same ones. An
earlier version of this paragraph asserted that the produced statement "is
applied at every model it was applied at before"; that reversed the
implication and is withdrawn.
This is the manuscript's own device and no other: e.cgamma.constraints
bounds cgamma by E^{-5} with E >= M cstar^{-1}, so "increasing M if
necessary" is a threshold on cgamma depending on the dimension and on
the already-produced constants. The dependence here is exactly that: d
and Cell, both fixed before the threshold is chosen.
Why the constant Cell disappears from the statement #
In PrincipalResponseLamWire's consumer, Cell occurs in hbudget and nowhere
else. Once hbudget is discharged, Cell occurs nowhere in the statement, so
the leading ∃ Cell : ℝ, 0 < Cell ∧ _ is an existential over a variable its
body does not mention and is dropped. Dropping it is a logical equivalence, not
a strengthening or a weakening.
What this module is not #
It is not a bridge from the proved Section 3.4 Budget chain
(...PrincipalResponseBudget{,Moment,Scales,Descent}). That chain bounds a
different quantity, the annealed probe defect
cubeAnnealedProbeDefect M L n Ev <= C 3^{2K} E^2 |log cgamma|^2 cgamma
(cubeAnnealedProbeDefect_le_logSq_budget), which is the input of the proved
...PrincipalResponseSwitch.annealedCubeBlockQuadratic_le_annealedLimitBlockQuadratic
and does not occur in hbudget. The hbudget binder is a
scale-and-sample-free numerical inequality among C_load(d), the grid switch
discount Delta and the grid ellipticity budget constant Cell. The two are
different displays of the manuscript and are not interchanged here.
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 the
bridge unchanged, as the literal factor (3/2).
Main results #
principalSwitchLoadConst_mul_gridSwitchDiscount_mul_le_half_gamma_pow_six
exists_smallCoupling_principalEnergy_bound_of_centering
References #
- ABK26, (the sentence quoted above);
e.cgamma.constraints(label; display);e.recurrence.params(label; display);e.lower.bound.principal.one.pre(label; display).
The bridge: the smallness at the grid switch discount #
The consumer that no longer binds hbudget #
The good-event energy display at the actual cutoff carrier, with the Young-remainder smallness supplied.
This is
ApproximateRecurrence.PrincipalResponseLamWire.exists_constant_principalEnergy_bound_of_centering
with its binder hbudget removed and nothing put in its place. Every other
binder is unchanged, in the same order and at the same type; the two binders
W and hindep in particular are untouched. Because Cell occurred only in
hbudget, the leading existential ∃ Cell : ℝ, 0 < Cell ∧ _ no longer mentions
its own variable and is dropped; that is a logical equivalence.
The threshold produced here is the one produced there, intersected with (1/2) / (C_load(d). (3/2). Cell). Shrinking an existential threshold is the
manuscript's own "increasing M in e.cgamma.constraints if necessary" (
with e.cgamma.constraints at label): the returned threshold depends only on
the dimension and on the constant Cell that PrincipalResponseLamWire had
already produced before any model is named.
: this statement holds only under the propositions supplied by its binders,
which are those of the consumer it re-states, minus hbudget:
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 numerical lower bound on the constant ofe.cg.ellip.lower(label) described inPrincipalResponseLamWire;hle : m - hgap <= highScale, the scale ordering of the switch;- the two solution families
hwD,hwNofe.def.w(label); hmeasR,hintR,hgoodInt,hcubeInt-- the four measurability and integrability data conditions;hindep-- the independence replacement, at the free familyW.
Deferred obligations, named. The earlier sentence here -- "No binder is a step of the manuscript's proof" -- was false as written and is withdrawn. Five of the binders above are deferred obligations of this provider helper rather than premises of the pinned source statement:
hindepis the conclusion of the independence sentence, not a premise of it, carried here at a free familyW. It is discharged nowhere in this module or in any module of its import cone.hmeasR,hintR,hgoodInt,hcubeIntare conditional A obligations: the sample measurability of the ellipticity load, the integrability of its square, and the two per-cube integrability families. None of them is discharged here.
hbudget -- itself a numerical step of the manuscript's argument rather than a
source premise -- is the one obligation this module does discharge, and it is
accordingly no longer a binder. Every remaining binder is parameter data,
typing data, a standing scale gate, a direction bound, the numerical gate
2 d^6 <= Ccg C_sens^2, or the e.def.w solution property of the two
corrector families.
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 (label).
Reaches exactly the one frozen theorem
Algsuperdiff.Frozen.External.calderon_zygmund, a proved external,
inherited from the consumer it re-states.