AdjointInjection #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the `(J3)` adjoint leg of the localization `J`-injection #

ABK26: the lambda-gate chain, and the injection display e.J.sensitivity.apppp, read at the transposed representative a^t.

What is delivered, and why it is not a rearrangement #

The manuscript prints the localization J-injection only at the primal coefficient, while the buckle's deep J-sum T2 needs it at a^t.

The transpose statement is not obtained by a deterministic rearrangement of the primal one. This is a precise claim and not a claim that no deterministic transpose-response identity exists: one does, it is proved, it is in this file's closure, and it is disclosed below (responseJ_transpose_neg_right in Section24/Sensitivity/Provider/DhBound/Discharge/AdjointResponse.lean, J(U, a^t, p, -q) = J(U, a, p, q) + 2 p . q). What that identity cannot do is close the injection, because it is off-diagonal: at the manuscript's own loadings p = shom^{-1/2} v, q = shom^{1/2} v it relates the transposed value at v to the primal value at the loading (p(v), q(-v)), which is (p(w), q(w)) for no w at all -- that would force w = v and w = -v simultaneously -- while the primal injection endpoint prices only the diagonal pair. So the deterministic route is genuinely unavailable and the law-level route is genuinely required. That route is a symmetry of the law, and exactly the one (J3) supplies; it is the route taken here:

negating every layer, j_n |-> -j_n, transposes the lower-infinite field, because each layer is antisymmetric and a_m = nu Id + k_m with k_m skew: this is the proved pointwise identity Cutoff.coefficientCutoff_negateCutoffSample_eq_adjoint;
the joint law is negation invariant: this is the proved Cutoff.map_negateCutoffSample_cutoffSampleLaw, which descends from the frozen M.J3.negation (a.j.iso);
hence the adjoint site at omega is almost surely the primal site at the negated sample, and every quantity the primal endpoint prices -- the W-underline^{2,infinity} gauge, the good local event, the lambda observable -- is negation invariant, so the price is carried at the SAME level.

Nothing here re-derives the sensitivity engine at a negated perturbation field: the primal endpoint is consumed verbatim and evaluated at the negated sample.

1. The `(J3)` invariance layer (section 1 below) #

The layer the composition needs, in the order it is built:

the three exact L-infinity shell gauges are negation invariant (unitCubeDerivNorm_negate, unitCubeSecondDerivNorm_negate, and the proved Cutoff.localCubeControl_negate for the zeroth order), hence so are underlineW2Gauge and BadEvents.cubeOscGauge, hence so is the good event's own gauge incrementOscGauge₂;
the cutoff triadic family at the negated sample is a.e. the adjoint family (coefficientCutoffTriadicCoeffFamily_negateCutoffSample_aeEq), so lambdaSq is negation invariant (lambdaSq_negateCutoffSample, through the proved CoarseEllipticity.lambdaSq_adjointFamily);
therefore the good local event Q(l,n,z) is negation invariant almost surely (mem_goodLocalEvent_negateCutoffSample_ae): its sensitivity clause exactly, its ellipticity clause through the measurable representative's own a.e. identification BadEvents.cubeLowerEllipticity_ae_eq_literal. The representative cubeLowerEllipticity is an A.mk choice, so this clause is genuinely only almost sure -- which is all the consumer needs, since the endpoint is itself an almost-sure statement.

3. The transposed priced endpoint (section 3 below) #

responseJ_transpose_injection_priced_forall_loads_of_primal carries the primal per-(l,z) priced injection display to the transposed representative, at the same loadings p = shom_{l-h}^{-1/2} v, q = shom_{l-h}^{1/2} v, the same leading constant 3 and the same remainder

324 C_resp (16 Ccg + 8 Ccg^2) cstar^{-1} cgamma 3^{4l - 2 cgamma l}
  ||k_m - k_{l-h}||^2_{W-underline^{2,infinity}(z+cu_l)} ,

The scale gate on `m0` #

The landmark premise carried by every statement below is mStarStar M < m0, not the printed m0 in (mstar, infty) cap Z. Nothing else moved: the premise is forwarded verbatim to the proved statements consumed here, no proof step here consumes it, and no frozen statement changes -- Algsuperdiff.Frozen.Section3.diffusivity_asymptotics keeps the printed mStar M < m0 and reaches the weaker-gated chain a fortiori through Provider.Scales.mStarStar_le_mStar.

The c >= 0 amplitude-scaling twins Stream.unitCubeDerivNorm_scale_of_nonneg and Stream.unitCubeSecondDerivNorm_scale_of_nonneg are not usable here: ShellField.negate = ShellField.scale (-1), and the sign hypothesis 0 <= c fails at c = -1. The route taken instead is the sharp characterization pair Stream.unitCubeDerivNorm_le_iff / Stream.unitCubeSecondDerivNorm_le_iff' composed with ShellField.matrixDerivativeNorm_neg, which is exact. Its second-derivative companion matrixSecondDerivativeNorm_neg is proved below, from ShellField.matrixSecondDerivativeNorm_le_iff in both directions.

References #

ABK26, l.localization.mathcalE and its lambda-gate, e.J.sensitivity.apppp, the adjoint deep J-sum, (J3), a.j.iso, e.good.local.events.
ABK26: the manuscript makes the same inference explicitly there, deducing khom_m(U) = 0 from e.adjoint.redundant and the assumption a.j.iso that a_m has the same law as a_m^t. The step this file performs at the localization display --- a_m and a_m^t are equidistributed by (J3), hence a priced primal statement transfers to the transpose at the same level --- is that same move at a different functional; nothing in the route depends on it.
negateCutoffSample is exactly the whole-sequence action.

1. The `(J3)` invariance layer #

In ABK26, negation acts on the whole shell sequence and preserves the joint law. This section proves that every quantity the injection prices is invariant under that action.

AdjointInjection #

Provider: the (J3) adjoint leg of the localization J-injection #

What is delivered, and why it is not a rearrangement #

1. The (J3) invariance layer (section 1 below) #

3. The transposed priced endpoint (section 3 below) #

The scale gate on m0 #

Related statements elsewhere #

References #

1. The (J3) invariance layer #

1.1 The exact shell gauges #

1.2 The coefficient carrier and the multiscale observable #

1.3 Almost-sure transport along the two carrier actions #

1.4 The good local event #

3. The transposed priced injection endpoint #

Provider: the `(J3)` adjoint leg of the localization `J`-injection #

1. The `(J3)` invariance layer (section 1 below) #

The scale gate on `m0` #

1. The `(J3)` invariance layer #