PrincipalResponseSensitivitySwitch #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the gauged coefficient switch of ABK26 Step 3, at the unit cube #
Source displays in ABK26:
l.J.sensitivity(label; statement), applied atdelta:= (1/2) 3^{-(1/4)(m-h-n)};e.J.by.means.of.bfA(label; display);- the chain of Step 3 of
l.approximate.recurrence.formula.
This module proves the whole chain as one inequality, at the carrier where the frozen sensitivity lemma lives.
What is proved #
Write U for the unit cube domain cubeDomain (originCube d 0), a for the
coarse field (a_{m-h} after rescaling), hfield for the perturbation
((k_m - k_{m-h}) - hbar, the fresh shell with its cube average removed, after
rescaling), am for the field a_m and hbar for the constant antisymmetric
average. Then, with Y = bfG_{-hbar} X,
X . bfA(U; am) X
<= (1 + delta + C ||grad hfield||_{W^{1,inf}} lambda_{3/8,2}^{-1})
* ( Y . bfA(U; a) Y + 2 X_1 . X_2 )
+ 2 C delta^{-1} ( |X_1|^2 ||hfield||_{W^{1,inf}}^2 lambda_{3/8,2}^{-1}
+ |X_1 . X_2| ||grad hfield||_{W^{1,inf}}^2
lambda_{3/8,2}^{-2} )
- 2 X_1 . X_2 .
At X = P_z the left-hand side is P_z . bfA_m(z+cu_n) P_z and the bracket is
bfG_{-hbar} P_z . bfA_{m-h}(z+cu_n) bfG_{-hbar} P_z; the two leftover
pairings are the manuscript's 2 p_z . q_z terms, kept explicit rather than
absorbed. The manuscript's own conclusion follows by bounding 2 delta |p_z. q_z| and the Young remainder -- an absorption step that is not performed
here, because it needs the size of hfield and of lambda_{3/8,2} on the good
event.
The three readings this makes explicit #
- The pairing term. The second equality of Step 3 carries
- 2 p_z . q_z; see the module docstring ofApproximateRecurrence.PrincipalResponseSensitivityAlgebra, where it is derived. The chain below carries it, and the manuscript's absorption consumes it. - The frozen statement
Algsuperdiff.Frozen.Section24.responseJ_sensitivityalready reflects both, and nothing is restated here.
Why this is conditional, and on exactly what #
Two hypotheses are explicit binders and the declarations are named
..._of_sensitivityGate accordingly.
hgateise.J.sensitivity.smallness.conditionfor the centered perturbation. ABK26 derives it from the good eventQ_z = Q(n, m-h, z)ofe.good.local.events. The repository's event-wired form,Provider.BadEvents.responseJ_sensitivity_of_mem_goodLocalEvent_of_lambdaTransfer, opens the gate for the literal rescaled incrementk_L - k_n(incrementUnitCube₂); Step 3 needs it for the increment with its cube average removed, which is what makes the||hfield||_{W^{1,inf}}^2term of the remainder small. Bridging the two is a Poincare-type centering estimate on the localization cube that this repository does not yet have, and it is not assumed here in any other form.- The carrier is the unit cube, because that is where
Algsuperdiff.Frozen.Section24.responseJ_sensitivityis stated. Transport toz + cu_nneeds the scale-and-translation covariance ofresponseJand ofcoarseBlockMatrix, together with the lambda-transfer already named in the module header ofProvider.BadEvents.GoodLocalEvents. Neither is available here.
Everything else is a source premise: hbar constant antisymmetric (proved for
the actual carrier in
ApproximateRecurrence.PrincipalResponseShellAverage), and hshift, the
field decomposition a_{m-h} + hfield = a_m - hbar. No proof step is carried
as a hypothesis, and no predecessor's conclusion is copied into a binder.
ABK26 at the unit-cube carrier, conditional on the smallness gate hgate
of l.J.sensitivity for the centered perturbation.
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 into the remainder.