SwitchNormalization #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the comparator switch shom_m -> shom_{l-h} of the localization lemma #
The printed display is
J(z+cu_l, shom_m^{-1/2}e, shom_m^{1/2}e; a_m) 1_{Q(l,l-h,z)}
<= shom_m^{-1} shom_{l-h} J(z+cu_l, shom_{l-h}^{-1/2}e, shom_{l-h}^{1/2}e; a_m)
+ 2 shom_m^{-1} shom_{l-h} (shom_m shom_{l-h}^{-1} - 1)^2 shom_{l-h}
|s_{m,*}^{-1}(z+cu_l)| 1_{Q(l,l-h,z)}
<= 2 J(z+cu_l, shom_{l-h}^{-1/2}e, shom_{l-h}^{1/2}e; a_m)
+ C min{cgamma^2 (m-l+h)^2, 3^{2 cgamma (m-l+h)}} + C E^4 cgamma^2 |log cgamma|^4 .
The coefficient stays a_m on both sides; only the comparator moves.
The two corrections implemented #
The remainder shape. The printed remainder is false for large gaps: since
u^2 <= 3^{2u}foru >= 0, the printedmin{cgamma^2 Delta^2, 3^{2 cgamma Delta}}is identicallycgamma^2 Delta^2, whereas the step's own quoted inpute.switchtheshoms.betterer.againcarries an un-cancelled3^{cgamma Delta}ande.shaking.lambdasquares it. The corrected per-cube remainder, delivered by every statement below, isC min{cgamma^2 Delta^2, 1} 3^{2 cgamma Delta} + C E^4 cgamma^2 |log cgamma|^4 3^{2 cgamma Delta} , Delta = m - l + h .The honest uniform constant is delivered here:
2 rhowhereshom_{l-h} <= rho shom_m, i.e.4at the manuscript's ownrho = 2and8at therho = 4thatl.shom.continuity's quarter comparison actually yields (therho = 4window comes from the recurrence-stage continuity route, which is exactly the second conjunct of the provedshom_continuity). The printed proof additionally needs, silently, a small-gap hypothesis|shom_m shom_{l-h}^{-1} - 1| <= 1/3for itsmanuscrip t-literal constant2.
What is here #
sigmaStarInv_quadForm_le_of_normSq_le_two— the gate transported to the loading ball (the source of the honest factor2in every remainder).responseJ_comparator_switch_le—e.shaking.lambdaatlam = shom_m shom_{l-h}^{-1},eps-form, at free comparators.responseJ_comparator_switch_of_gate— the uniform regimedelta = 1, the honest constant2 rho.sigmaStarInv_gate_of_lambdaGate,sigmaStarInv_transpose_gate_of_lambdaGate— the printedlambda_{s,2}gate carrier, primal and adjoint.responseJ_shom_switch_of_defect— the switch at the corrected remainder.shom_switch— the display at the running comparatorsshom_m,shom_{l-h}, consumingl.shom.continuity.breakdownLeg{A,B}_le_of_switch— the interface against the proved transport, at free leading constantKc, deep boundc0and remainderrem.breakdownLeg{A,B}_le_of_shom_switch— the actual composition:shom_switchfed into that interface atsigma := shom_m,sigmaDeep:= shom_n.
The loading carrier: vecNormSq v <= 2, not |e| = 1 #
Every statement below is proved for every v with vecNormSq v <= 2. The
step is pointwise in the loading; only its additive sigma_*^{-1} remainder
doubles, which is why every remainder below carries the honest factor 2 in
front of the gate level Cev (the printed display, stated at |e| = 1,
carries 1).
The lambda-gate is a conditional input #
ABK26 justifies the last inequality by the chain
|s_{m,*}^{-1}(z+cu_l)| 1_Q <= lambda_{1/8,2}^{-1}(z+cu_l; a_m) 1_Q
<= 2 lambda_{1/8,2}^{-1}(z+cu_l; a_{l-h}) 1_Q
<= C shom_{l-h}^{-1} ,
whose middle step is l.lambda.sensitivity on the good event Q(l,l-h,z) and
whose last step is the ellipticity clause of e.good.local.events. It enters
every statement below as a named hypothesis in exactly the shape those
producers deliver, namely the clamped form
hgate : shom_{l-h} * (lambdaSq (z+cu_l) (1/8) (.finite 2) a_m)^{-1} <= Cev
(the hgate binder of sigmaStarInv_gate_of_lambdaGate), or, one step more
primitive and carrier-free,
hgate : shom_{l-h} * matrixNorm (sigmaStarInvCoarse U A) <= Cev
(responseJ_comparator_switch_of_gate). Nothing in this module asserts that
either holds.
So the gate above is exactly shom_{l-h} lambda_{1/8,2}^{-1}(z+cu_l; a_m) <= Cev, the last line of the printed chain, in the repository's own spelling.
The cross-unit remainder shape, and where the bridge lives #
shom_switch (here) | AggregationRemainder.switchRemainder | |
|---|---|---|
| min order | min 1 (cgamma^2 Delta^2) | min (cgamma^2 (j+h)^2) 1 |
| rpow exponent | 3 ^ (2 * (cgamma * Delta)) | 3 ^ (2 * cgamma * (j+h)) |
| structure | distributed (two summands) | factored (one product) |
| index | Delta = (m:R) - (n:R), m n : Z | (j:R) + (h:R), j h : N |
The min order here follows the proved shom_continuity display
(ShomContinuity.lean); the sibling's follows the manuscript. The two shapes
are equal, not merely comparable — the whole glue is min_comm, one ring
normalization of the rpow exponent, and push_cast for the Z -> R reindex at
n := m - j - h. The assembly must consume it, not re-derive it. Nothing
on this side of the seam is restated for it: shom_switch's statement is
unchanged.
The scale gate on m0 (-bin statement change) #
The landmark premise carried by every public below is mStarStar M < m0,
not the printed m0 in (mstar, infty) cap Z. Nothing else moved: the
premise is forwarded verbatim to Provider.Localization.shom_continuity, 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.
References #
- ABK26: the switch display; the
lambda-gate chain, quoted as a hypothesis here;e.shaking.lambda;e.good.local.events.
1. Real-variable arithmetic for the corrected remainder #
Three elementary facts, isolated so that no numeric tactic is ever run on a
Real.rpow or a Real.log atom.
2. The sigma_*^{-1} quadratic form on the loading ball #
The gate, transported to the loading ball. If sn |s_*^{-1}(U;A)| is
clamped by Cev, then sn times the s_*^{-1} quadratic form at every
loading of squared length at most 2 is clamped by 2 Cev.
The factor 2 is the entire cost of the vecNormSq v <= 2 carrier that (ii)
makes binding; the printed display, stated at |e| = 1, carries 1 here.
3. e.shaking.lambda at lam = shom_m shom_{l-h}^{-1} #
The pure gauge algebra, at a bare Domain/CoeffOn pair so that the same
statement serves the primal leg and the transposed leg of the breakdown display.
The comparators are free positive scalars; no shom, no nu, no floor.
The comparator switch, eps-form. For positive comparators sm
(the working one, shom_m) and sn (the deep one, shom_{l-h}) and any Young
parameter delta > 0,
J(U, sm^{-1/2}v, sm^{1/2}v; A)
<= (1+delta) (sn sm^{-1}) J(U, sn^{-1/2}v, sn^{1/2}v; A)
+ ((1+delta^{-1})/2) (sn sm^{-1}) (sm sn^{-1} - 1)^2 (sn (v . s_*^{-1} v)) .
This is e.shaking.lambda at lam = sm sn^{-1} and base loading (sn^{-1/2}v, sn^{1/2}v), in the pre-optimization form of the printed proof. It is an
identity-level rearrangement of the proved
Shaking.responseJ_shaking_lambda_normalizedLoading_epsilon: nothing is
estimated, so the printed J-coefficient lam^{-1} is visibly the delta -> 0 limit, and visibly unattainable.
The comparator switch, uniform regime (delta = 1), with the
sigma_*^{-1} remainder clamped by the disclosed gate.
J(U, sm^{-1/2}v, sm^{1/2}v; A)
<= 2 rho J(U, sn^{-1/2}v, sn^{1/2}v; A) + 2 rho K^2 Cev
whenever sn sm^{-1} <= rho, |sm sn^{-1} - 1| <= K and
sn |s_*^{-1}(U;A)| <= Cev, for every v with vecNormSq v <= 2.
The printed 2 is not obtainable from e.shaking.lambda without a smallness
restriction on |sm sn^{-1} - 1|.
The two 2s are different: on the J-term it is the Young factor 1 + delta
at delta = 1; on the remainder it is the loading-ball factor of
sigmaStarInv_quadForm_le_of_normSq_le_two (the Young remainder coefficient
(1 + delta^{-1})/2 is exactly 1 at delta = 1).
hgate is a conditional A obligation, not a source premise of this module:
it is the lambda-gate step, whose producers are
Provider/BadEvents/GoodLocalEvents.lean and
Provider/BadEvents/LambdaTransfer.lean.
4. The gate at the printed lambda_{s,2} carrier #
ABK26 clamps |s_{m,*}^{-1}(z+cu_l)| through lambda_{1/8,2}^{-1}(z+cu_l; a_m).
The two bridges below convert a gate stated at that carrier into the matrix-norm
gate the switch consumes, on the primal and on the transposed representative.
The exponents s, q are free, so the lambda-gate step may discharge at the
printed (1/8, 2) or at any other admissible pair.
From the printed lambda-gate to the switch's gate, primal leg.
CoarseGraining's one-cube ordering e.ellipticities.monotone.ordered
(oneCube_sigmaStarInv_le_lambdaSq_finite_inv) is exactly the printed step
|s_{m,*}^{-1}(z+cu_l)| <= lambda_{s,2}^{-1}(z+cu_l; a_m).
From the printed lambda-gate to the switch's gate, adjoint leg. Both
sides of the gate are adjoint-invariant: sigma_*^{-1}(U; a^t) = sigma_*^{-1}(U; a) and lambda_{s,q}(Q; a^t) = lambda_{s,q}(Q; a) (proved
publics of Provider/CoarseEllipticity/DoubledAdjointEllipticity.lean), so the
same printed gate serves breakdownLegB.
5. The corrected remainder #
Threading the squared shom-defect through the switch algebra of Section 3.
The per-cube switch at the corrected remainder.
Given the e.shom.m.vs.shom.n defect display in its proved shape
|sm sn^{-1} - 1| <= Cd min{1, a + b} 3^t ,
the uniform switch at rho = 4 (the shom_continuity ratio cap) yields, for
every v with vecNormSq v <= 2,
J(U, sm^{-1/2}v, sm^{1/2}v; A)
<= 8 J(U, sn^{-1/2}v, sn^{1/2}v; A)
+ 16 Cd^2 Cev min{1, a^2} 3^{2t}
+ 16 Cd^2 Cev b^2 3^{2t} .
At a = t = cgamma (m - l + h) and b = E^2 cgamma |log cgamma|^2 this is
exactly the corrected remainder: C min{cgamma^2 Delta^2, 1} 3^{2 cgamma Delta} +^4 cgamma^2 |log cgamma|^4 3^{2 cgamma Delta}, with b^2 = E^4 cgamma^2 |log cgamma|^4 and the 3^{2 cgamma Delta} un-cancelled on both
summands.
Constant accounting, term by term:
- the remainder prefactor
16 = (rho = 4) * (2 from vecNormSq v <= 2) * (2 from the squared-defect splitmin_one_add_sq_le), the Young remainder coefficient(1 + delta^{-1})/2being exactly1atdelta = 1.
Every constant is explicit; Cd is whatever the defect display supplies
(dimension-only, when that display is shom_continuity's).
6. The shom instance: consuming l.shom.continuity #
Of the three shom inputs the (i) consumer probe exhibited at n := l - h,
the switch step itself consumes exactly two: the second conjunct of the proved
shom_continuity (the ratio cap 4, the honest reading of the printed
shom_m^{-1} shom_{l-h} <= 2) and the fifth (the e.shom.m.vs.shom.n defect
display). The third — the fourth conjunct, the short-range cap 12 at cgamma (m-n) <= 1 — is not used here; it belongs to the lambda-gate step,
whose printed clamp runs through the good event's shom_{l-h-1} and must
return to shom_{l-h}.
The switch-normalization step at the running comparators, at the corrected remainder and the honest constant.
On the l.shom.continuity premise list, for every pair of scales n <= m <= m0
(the intended instance is n := l - h, so that m - n = m - l + h = Delta),
every domain/coefficient pair, every gate level Cev clamping the
sigma_*^{-1} size at the deep comparator, and every loading v with
vecNormSq v <= 2:
J(U, shom_m^{-1/2}v, shom_m^{1/2}v; A)
<= 8 J(U, shom_n^{-1/2}v, shom_n^{1/2}v; A)
+ Cs Cev min{1, cgamma^2 (m-n)^2} 3^{2 cgamma (m-n)}
+ Cs Cev E^4 cgamma^2 |log cgamma|^4 3^{2 cgamma (m-n)} .
hgate is the lambda-gate conditional input; it is stated at the
deep comparator shom_n because that is the scale the printed clamp
lambda_{1/8,2}^{-1}(z+cu_l; a_m) <= C shom_{l-h}^{-1} produces. Use
sigmaStarInv_gate_of_lambdaGate (or its adjoint twin) to feed it from the
printed lambda_{1/8,2} form.
7. Discharging the transport's consumption interface #
The switch is pointwise inside the response, so it is discharged inside the
hypothesis h of breakdownLeg{A,B}_le_of_originCube_translate_bound at
sigma:= Annealed.sigmaBar M m — instantiating sigma:= shom_{l-h} would
produce a leg at the wrong comparator for
Breakdown.cutoffHomogenizationError_sq_ae_le_breakdown ((i)).
The primal breakdown leg from the switch plus a deep-comparator bound.
If, at the translated origin cube, the response at the deep comparator is
bounded by c0 over the whole loading ball, and the switch moves the working
comparator onto it at leading constant Kc and additive remainder rem, then
breakdownLegA at the working comparator is bounded by Kc c0 + rem.
hdeep's producer (disclosure). hdeep is not produced anywhere in this
module, and unlike hgate it is not a subnode either: it is the assembly's
own obligation. hswitch's producer, by contrast, is in this file —
shom_switch, composed here as breakdownLegA_le_of_shom_switch.
The adjoint twin of breakdownLegA_le_of_switch; the transported
representative is the transpose, exactly as in
breakdownLegB_le_of_originCube_translate_bound.
hswitch's producer is shom_switch itself, composed here as
breakdownLegB_le_of_shom_switch.
The composed endpoints #
shom_switch emits the left-associated three-term 8 * J + A + B, while
breakdownLeg{A,B}_le_of_switch's hswitch demands the two-term Kc * J + rem. Over the reals those are equal but not syntactically so, and an exact
composition of the two headline endpoints of this module fails with a Type mismatch (8 * J + A + B against 8 * J + (A + B)). The two theorems below
exhibit the composition once and for all, with the linarith bridge discharged
here rather than at every call site, at the development instantiation sigma:= shom_m, sigmaDeep:= shom_n (i). They are the actual content of the header's
claim that breakdownLeg{A,B}_le_of_switch is "the composition with the proved
transport". No statement of shom_switch or of either leg lemma is changed.
The primal breakdown leg, straight from shom_switch.
The full chain of this module in one statement: on the l.shom.continuity
premise list, for every pair of scales n <= m <= m0, every translated origin
cube of the breakdown display, every gate level Cev clamping the
sigma_*^{-1} size at the deep comparator shom_n, and every deep-response
bound c0 over the loading ball vecNormSq v <= 2,
breakdownLegA R (a_L omega) (isotropic (shom_m))
<= 8 c0
+ (Cs Cev min{1, cgamma^2 (m-n)^2} 3^{2 cgamma (m-n)}
+ Cs Cev E^4 cgamma^2 |log cgamma|^4 3^{2 cgamma (m-n)}) .
The adjoint breakdown leg, straight from shom_switch. The adjoint
twin of breakdownLegA_le_of_shom_switch; the gate is stated at the transposed
representative, which sigmaStarInv_transpose_gate_of_lambdaGate supplies from
the same printed lambda-gate by adjoint invariance.