Step1Assembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The assembly of Step 1: e.good.simplex.consequence at the cube carrier #
CrudeResponseBound.lean proves the middle of Step 1 of
p.bfA.multiscalebound (ABK26): the two crude response legs at a_L,
transported to the multiscale gauges Lambda_{1/4,2}(z + square_j; a_j) and
lambda^{-1}_{1/4,2}(z + square_j; a_j) of the containing cube.
JResponseApplication.lean proves the polarization split and the
running-diffusivity comparison. This module proves local cube-carrier results
by supplying the two missing links and running the final arithmetic:
- the arithmetic, with the
cstar^{-1}correction.
The manuscript's unnamed Cs, made explicit #
Every constant below is explicit and dimension-free except the one frozen
Lambda-sensitivity constant bigLambdaSensitivityConst d:
p̂leg:80. 3^{(j-k)/2} (1 + 8 C_{Lambda} cstar^{-1} gamma 3^{-2 gamma j} ||k_L - k_j||^2);q̂leg:40 . 3^{(j-k)/2} . 3^{gamma (i - j)};- assembled: four times each, by the polarization split.
The q̂ leg's factor (1 + C_lambda |grad (k_L - k_j)| lambda^{-1}_{3/8,2}),
which the manuscript hides inside C, is collapsed to 2 by the proved
e.we.can.apply.cg gate (lambdaGateFactor_le_one_of_notMem_bad_ae); the p̂
leg's Lambda and lambda^{-1} gauges are collapsed by the two halves of not B_loc; the two sigmabar ratios are the proved
sigmaBar_le_four_mul_sigmaBar and sigmaBar_le_four_mul_rpow_mul_sigmaBar
(constant 4 each).
Why the statements are almost-sure #
e.Bloc.def is stated against the measurable representatives
cubeLowerEllipticityInv / cubeUpperEllipticity built by A.mk, of which no
pointwise information is available; transporting either to the Chapter 2 gauge
Ch02.lambdaSq / Ch02.LambdaSq that the sensitivity conclusions carry
therefore costs one null set. This is the same carrier phenomenon as in
LambdaTransfer.lean and JSmallness.lean, and all proved smallness gates are
already discharged, so no gate hypothesis appears anywhere below (reading,
for the q̂ leg).
Main results #
cubeUpperEllipticityLiteral_eq_LambdaSq: theLambda-half literal identification, the mirror ofcubeLowerEllipticityInvLiteral_inv_eq_lambdaSq.cubeUpperEllipticity_le_ten_mul_sigmaBar_of_notMem_badLoc,LambdaSq_quarter_le_ten_mul_sigmaBar_of_notMem_badLoc_ae: theLambda-half ofnot B_loc, at the representative and at the Chapter 2 gauge.lambdaSq_quarter_inv_le_ten_mul_inv_sigmaBar_of_notMem_badLoc_ae: itslambda-mirror at the same carrier.inv_sigmaBar_sq_le_four_mul_inv_cstar_mul_gamma_mul_rpow: thecstar^{-1}correction.lambdaGateFactor_le_one_of_notMem_bad_ae: thee.we.can.apply.cggate as the factor bound theq̂leg consumes.cubeLowerEllipticityInvLiteral_eq_lambdaSq_inv: thelambda-half literal identification, reading the literal lower observable aslambda^{-1}_{s,q}of the Chapter 2 family.
References #
- ABK26,
e.good.simplex.consequence, Step 1 ofp.bfA.multiscalebound,e.shom.h.bounds,e.Bloc.def,e.SW.def.
The Lambda-half literal identification #
The Lambda-half literal identification. The literal upper observable of
CubeEllipticity.lean is CoarseGraining's Ch02.LambdaSq of the compatible
triadic family of the actual cutoff. This is the exact mirror of the proved
cubeLowerEllipticityInvLiteral_inv_eq_lambdaSq of LambdaTransfer.lean, and
it is what moves the second disjunct of e.Bloc.def onto the carrier at which
e.big.Lambda.sensitivity is stated.
The literal lower observable, read directly as lambda^{-1}_{s,q} of the
Chapter 2 family. This is the proved
cubeLowerEllipticityInvLiteral_inv_eq_lambdaSq with the inverse moved to the
right side.
The two halves of not B_loc #
The Lambda-half of not B_loc, at the representative (ABK26, the
second disjunct of e.Bloc.def): off B_loc(z + square_j) the coarse-grained
upper ellipticity of a_j on the cube is at most 10 sigmabar_j. This is the
exact mirror of the proved
sigmaBar_le_ten_mul_cubeLowerEllipticity_of_notMem_badLoc of
JSmallness.lean; no positivity binder is needed on this side, because nothing
is inverted.
The Lambda-half of not B_loc, at the Chapter 2 gauge. Almost surely,
off B_loc(z + square_j),
Lambda_{1/4,2}(z + square_j; a_j) <= 10 sigmabar_j .
The transport from the measurable representative to Ch02.LambdaSq is
cubeUpperEllipticity_ae_eq_literal composed with
cubeUpperEllipticityLiteral_eq_LambdaSq; the null set is the representative's
own, exactly as for the lambda half.
The lambda-half of not B_loc, at the Chapter 2 gauge (ABK26, the
first disjunct of e.Bloc.def). Almost surely, off B_loc(z + square_j),
lambda^{-1}_{1/4,2}(z + square_j; a_j) <= 10 sigmabar_j^{-1} .
(The proved sigmaBar_le_ten_mul_cubeLowerEllipticity_of_notMem_badLoc is a
cousin at the representative cubeLowerEllipticity; this proof does NOT use it
— it negates badLoc's first disjunct directly;.)
The cstar^{-1} correction #
The lower branch of e.shom.h.bounds (ABK26) gives sigmabar_m^2 >= (1/4) cstar gamma^{-1} 3^{2 gamma m}, hence
sigmabar_m^{-2} <= 4 cstar^{-1} gamma 3^{-2 gamma m} ,
for every scale m <= m0. The factor cstar^{-1}, absent from the printed
display, cannot be absorbed into a dimension-only constant: the standing
assumptions bound cstar only from above.
The gate of e.we.can.apply.cg, read as a factor bound (ABK26). Almost
surely, on not B_osc(z + square_j) and not B_loc(z + square_j) and under the
induction state, the multiplicative sensitivity defect of the q̂ leg is at
most 1, for every L >= j:
C_{(e.lambda.sensitivity)} |grad (k_L - k_j)| lambda^{-1}_{3/8,2}(z+square_j;a_j)
<= 1 .
This is the proved
gradientW1Infinity_incrementUnitCube_le_lambdaGate_notMem_bad_ae divided by
the (strictly positive) gauge; it is what collapses the manuscript's hidden C
on the q̂ leg to the explicit factor 2.