PrincipalResponseSwitchTransport #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the gauge switch of ABK26 Step 3, transported to z + cu_n #
Source displays in ABK26:
l.approximate.recurrence.formula(label), Step 3;- the gauge-switch chain of Step 3, whose closing line is sub-step (i) of
e.lower.bound.principal.one.pre(label); l.J.sensitivity(label), applied atdelta := (1/2) 3^{-(1/4)(m-h-n)};e.J.by.means.of.bfA(label);e.good.local.events(label; display).
What this module supplies #
ApproximateRecurrence.PrincipalResponseSensitivitySwitch proves the chain at
the unit cube square_0, because that is the carrier of the frozen
Algsuperdiff.Frozen.Section24.responseJ_sensitivity. Its own module
docstring names two gaps. This module closes the first of them: the transport
of that chain to the manuscript's localization cube z + cu_n.
The transport is an equality transport -- no constant is created or lost --
and it is assembled from the same two CoarseGraining interfaces that
Provider.BadEvents.LambdaCovariance and Provider.Multiscale.JCarrierRescale
already use for lambda_{s,q} and for J:
- dilation:
Ch02.coarseBlockMatrix_dilateatdilateCube (-m) (originCube d m) = originCube d 0; - translation: the proved one-cube covariance
Provider.BadEvents.coarseBlockMatrix_cutoff_translateCutoffSample, read throughCh02.coarseBlockMatrix_eq_ofAEEqso that the carrier is the repository's ownCutoff.coefficientCutoffTriadicCoeffFamily.
The resulting identity coarseBlockMatrix_unitRescaledCutoffCoeff is the exact
analogue, for the doubled coarse block matrix bfA, of the proved
unitCubeLambda_unitRescaledCutoffCoeff (for lambda) and
responseJ_unitRescaledCutoffCoeff (for J).
The second gap it names -- absorption of the Young remainder using the size of
the centered shell and of lambda_{3/8,2} on the good event -- is performed in
the second half of this module, and the result is stated cube by cube, with the
good event carried as a per-cube family.
Nothing here asserts that the principal-response step of
l.approximate.recurrence.formula, its sub-step (i), or e.lower.bound.principal.one.pre
is closed: the composed statement is one sub-step of those displays and is itself
conditional on the two binders described under "Binders the caller must supply" below.
The 3/2, and why the printed 1 + 3^{-(1/4)(m-h-n)} is optimistic #
ABK26 prints the switch factor 1 + 3^{-(1/4)(m-h-n)}, i.e. 1 + 2 delta at
the manuscript's own delta = (1/2) 3^{-(1/4)(m-h-n)}. Obtaining it needs C |grad h| lambda^{-1} <= delta. What the event e.good.local.events supplies
is its second inequality,
C_sens sup_{L >= n} 3^{2m} ||grad(k_L - k_n)|| <= 3^{-(1/4)(n-m)_+} lambda_{1/8,2} ,
i.e. C |grad h| lambda^{-1} <= Delta = 2 delta, because the factor 1/2 of
the display sits in the middle term (against shom_{n-1}) and not in the
lambda bound. The honest switch factor is therefore 1 + delta + Delta = 1 + (3/2) Delta, which is what is carried below. The discrepancy is a constant
factor 3/2 in a quantity the manuscript immediately relaxes to cgamma^6; it
is absorbed as soon as gamma <= 2/3, by
three_halves_mul_rpow_three_neg_recurrenceGap_div_four_le_gamma_pow_six.
This is recorded as an observation about a printed constant, not as a defect of
the argument.
Binders the caller must supply #
Two quantitative inputs are not proved here and are disclosed binders on every statement that needs them.
hgrad-- the discounted gradient gateC |grad h| <= Delta lambda_{3/8,2}(z+cu_n; a_{m-h})for the centered shellh - (h)_{z+cu_n}. For the literal incrementk_m - k_{m-h}it is proved:responseSensitivityConst_mul_gradientW1Infinity_le_of_mem_goodLocalEvent_aederives it, almost surely, from membership inProvider.BadEvents.goodLocalEventtogether with the proved lambda-transferProvider.BadEvents.lambda_transfer_ae, given the caller's comparison of the centered field's gradient gauge with the literal one. Centering by a constant does not change a gradient, but the two carriers are distinct objects in this repository and that identification is not available here.hshell-- the centered-shell size||h - (h)_{z+cu_n}||^2 <= Delta^2 shom_{m-h} lambda_{3/8,2}. ABK26 obtains it from the middle term ofe.good.local.events(theshom_{n-1}bound) together with a Poincare estimate onz + cu_nfor the centered field ande.cg.ellip.lower(label). This repository has no Poincare centering estimate on a triadic cube, sohshellstays an explicit hypothesis; it is never assumed in any other form and never derived from an unproved lemma.
Neither binder is a predecessor's conclusion and neither smuggles a proof step: both are quantitative statements about the data (the shell increment and the coarse ellipticity), exactly as uses them.
Per-cube good events #
No union over the grid is formed anywhere in this module.
Carriers and readings #
- The localization cube is a free
TriadicCube d;n = m - h - 16 ceil|log_3 gamma|ofe.recurrence.params(label) is never hard-coded. - The scale gap
G = m - h - nis never fixed to a numeral. It enters asscaleGapPos R.scale lowScaleinresponseSensitivityConst_mul_gradientW1Infinity_le_of_mem_goodLocalEvent_ae, and as the freerecurrenceGap a gammaofthree_halves_mul_rpow_three_neg_recurrenceGap_div_four_le_gamma_pow_six. - Nothing about that reading is restated here: the transported statement simply
carries
Ch02.lambdaSq Q (3/8) 2where the unit-cube statement carriesunitCubeLambda (3/8) 2. cstardoes not occur in this module.
Main results #
coarseBlockMatrix_originCube_dilatecubeSet_eq_translateSet_originCube_triadicCubeShiftcoarseBlockMatrix_cutoff_family_translateCutoffSamplecoarseBlockMatrix_unitRescaledCutoffCoeffblockVecDot_coarseBlockMatrix_le_gauge_switch_cube_of_sensitivityGateblockVecDot_coarseBlockMatrix_nonnegabs_vecDot_le_half_weighted_vecNormSq_addgaugeSwitchYoungAbsorbprincipalSwitchLoadConst,principalSwitchLoadConst_posblockVecDot_coarseBlockMatrix_le_switch_absorbed_cuberesponseSensitivityConst_mul_gradientW1Infinity_le_of_mem_goodLocalEvent_aethree_halves_mul_rpow_three_neg_recurrenceGap_div_four_le_gamma_pow_six
Scale normalization of the doubled coarse block matrix #
Scale normalization of bfA. The doubled coarse block matrix of a triadic
family on the centered scale-m cube is that of its 3^{-m}-dilation on the
unit cube. This is the bfA analogue of the proved
lambdaSq_originCube_dilate and responseJ_originCube_dilate.
Unconditional: no caller-supplied proposition enters.
The triadic geometry of the base-point translation #
The half-open realization of a triadic cube Q = z + square_m is the
translate, by the real base point z = triadicCubeShift Q, of the centered
cube of the same scale. This is the cubeSet counterpart of CoarseGraining's
openCubeSet_eq_translateSet_originCube_of_triadicCube, at arbitrary (possibly
negative) scale.
Unconditional: no caller-supplied proposition enters.
Translation covariance at the repository's own family carrier #
One-cube translation covariance of the doubled coarse block matrix for the
actual coefficient cutoff, stated at
Cutoff.coefficientCutoffTriadicCoeffFamily: if the half-open realization of
T is the translate by v of that of R, then bfA(T; a_m) equals
bfA(R; a_m) for the translated sample.
This is the proved
Provider.BadEvents.coarseBlockMatrix_cutoff_translateCutoffSample read
through Ch02.coarseBlockMatrix_eq_ofAEEq; the two coefficient objects have the
same coefficient field and differ only in their ellipticity witnesses.
: this statement holds only under the proposition supplied by its binder
hset, the triadic geometry of the translation. It is a provider A, not a
source-facing frozen declaration.
The transport #
The bfA carrier transport. The frozen unit-cube doubled coarse block
matrix of the rescaled coefficient object is the doubled coarse block matrix of
the cutoff on the cube Q = z + square_m itself:
bfA(square_0; a_n(z + 3^m .)) = bfA(z + square_m; a_n) .
This is the exact analogue, for bfA, of the proved
unitCubeLambda_unitRescaledCutoffCoeff and
responseJ_unitRescaledCutoffCoeff.
Unconditional: no caller-supplied proposition enters.
ABK26 at the manuscript's own cube Q = z + cu_n, at a free sensitivity
parameter delta in (0,1].
Every carrier is the localization cube: both doubled coarse block matrices are
bfA(z + cu_n; .), and the ellipticity gauge is the manuscript's own
lambda_{3/8,2}(z + cu_n; a_{lowScale}). The dimension-only constant
responseSensitivityConst d is unchanged by the transport, which is a chain of
equalities.
The manuscript's a_m is the cutoff at highScale and its a_{m-h} is the
cutoff at lowScale; the load X is P_z and the constant antisymmetric
matrix hbar is (h)_{z+cu_n} (built and proved skew in
ApproximateRecurrence.PrincipalResponseShellAverage). The two 2 X_1 . X_2
terms are the manuscript's 2 p_z . q_z, derived in
ApproximateRecurrence.PrincipalResponseSensitivityAlgebra; they are kept
explicit rather than absorbed. The Young remainder is likewise not absorbed at
this stage; the absorption is
blockVecDot_coarseBlockMatrix_le_switch_absorbed_cube below.
: this statement holds only under the propositions supplied by its binders --
dimension (the paper-wide 2 <= d), hskew (antisymmetry of the averaged
shell), hshift (the manuscript's own field decomposition a_{lowScale} + hfield = a_{highScale} - hbar at the rescaled unit-cube carrier), hgate
(e.J.sensitivity.smallness.condition, label, for the centered perturbation)
and the range hdelta, hdelta1 of delta. It is a provider A, not a
source-facing frozen declaration.
Two elementary facts about the doubled block form #
The doubled coarse block quadratic form is nonnegative. CoarseGraining's
Ch02.blockCoarseMatrixTheory gives BlockPosDef (coarseBlockMatrix U a),
which is strict positivity off the origin; the origin contributes 0.
Unconditional: no caller-supplied proposition enters.
: this statement holds only under the proposition supplied by its binder hS,
positivity of the weight. It is a provider A, not a source-facing frozen
declaration.
The absorption, as real arithmetic #
The absorption, as a real inequality.
Reading the variables at the Step 3 carrier: E is P_z . bfA_m(z+cu_n) P_z,
B is G_{-(h)} P_z . bfA_{m-h}(z+cu_n) G_{-(h)} P_z, t is p_z . q_z,
nrm1 and nrm2 are |p_z|^2 and |q_z|^2, C is the frozen dimension-only
sensitivity constant, g and w are the gradient and value gauges of the
centered shell, lam is lambda_{3/8,2}(z+cu_n; a_{m-h}), S is
shom_{m-h}, and Delta is 3^{-(1/4)(m-h-n)_+}. hchain is the conclusion
of the transported gauge switch at the manuscript's own delta = (1/2) Delta.
The three moves are the manuscript's: the two 2 p_z . q_z pairings cancel down
to 2 (delta + C g lam^{-1}) (p_z . q_z); the pairing is folded into the load
by Young at the weight S; and the two remainder terms are folded in using
hgrad and hshell.
: this statement holds only under the propositions supplied by its binders --
the sign and range conditions, hpair (Young at weight S), hgrad (the
discounted gradient gate of e.good.local.events), hshell (the
centered-shell size), and hchain (the transported gauge switch). It is a
provider A, not a source-facing frozen declaration.
The load constant #
The dimension-only constant multiplying the ellipticity load `shom_{m-h}|p_z|^2
- shom_{m-h}^{-1}|q_z|^2
in the absorbed form, normalized so that it multiplies the switch excess(3/2) Delta` itself. It is built from the frozen response-sensitivity constant alone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Positivity of the load constant.
: this statement holds only under the proposition supplied by its binder
dimension, the paper-wide 2 <= d. It is a provider A, not a source-facing
frozen declaration.
The normalization identity behind principalSwitchLoadConst.
Unconditional: no caller-supplied proposition enters.
The closing line of ABK26, at the manuscript's own cube.
P_z . bfA_m(z+cu_n) P_z
<= (1 + (3/2) Delta) G_{-(h)} P_z . bfA_{m-h}(z+cu_n) G_{-(h)} P_z
+ C_load(d) (3/2) Delta ( S |p_z|^2 + S^{-1} |q_z|^2 ) ,
with Delta the manuscript's 3^{-(1/4)(m-h-n)} (free here) and S the
manuscript's shom_{m-h} (free here). See the module docstring for why the
switch factor carries 3/2 rather than the printed 1.
: this statement holds only under the propositions supplied by its binders --
dimension; hskew and hshift, the carrier facts of the averaged fresh
shell and the source's own field decomposition; the ranges hDelta0,
hDelta1, hS0, hlam0; and the two good-event inputs hgrad and hshell
described in the module docstring. It is a provider A, not a source-facing
frozen declaration.
The discounted gradient gate, from the good event #
The discounted gradient gate of e.good.local.events, transferred to the
frozen lambda_{3/8,2}.
On the event cQ(n, m-h, z) -- here goodLocalEvent M Ccg R lowScale at the
localization cube R of scale n and the coarse scale lowScale = m-h -- the
manuscript's second inequality reads
C_sens 3^{2n} ||grad (k_L - k_{m-h})||_{W^{1,infinity}(z+cu_n)}
<= 3^{-(1/4)(m-h-n)_+} lambda_{1/8,2}(z+cu_n; a_{m-h}) ,
and the proved lambda-transfer replaces lambda_{1/8,2} by the frozen
lambda_{3/8,2}(z+cu_n; a_{m-h}). The hypothesis hcentered is the only
remaining input: it compares the gradient gauge of the caller's centered field
with that of the literal rescaled increment.
: this statement holds only under the propositions supplied by its binders --
hL (m-h <= m), membership in the good event, and hcentered. It is a
provider A, not a source-facing frozen declaration.
The cgamma^6 gate at the corrected recurrence gap #
The switch-factor gate at the corrected gap, with the 3/2 of the module
docstring. At the multiplier a >= 28 the switch excess (3/2) 3^{-(1/4)(m-h-n)} of the absorbed form is below the cgamma^6 that
e.lower.bound.principal.one.pre prints, as soon as gamma <= 2/3.
It is a provider A, not a source-facing frozen declaration.