EdBridgeFolds #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The three folds between the anchored one-step and the Step-4 slot #
The anchored interior one-step delivers the one-step contraction
with the anchor's four printed legs on the right. The iteration anchor's own
per-scale hypothesis (e.Ej.decay.assumption, named IterationDecay by the
Step-5 provider) asks instead for
E(u, U_{j-h}) ≤ θ^h E(u, U_j) + ε_j |∇ℓ_j| + δ_j , θ = 3^{-1/4} .
This module is the scalar/geometric part of that conversion — residues 1, 2
and 4, each as a standalone atom, with the window bookkeeping of residue 3 left
to EdBridgeStepFour.
The three atoms #
- The good-event cap fold (residue 1).
rpow_neg_four_mul_le_of_capis the multiplicationC s^{-4} · 𝓔 · X ≤ C · C_cap · s^{-3} · δ^{1/2} · X, valid at anyX ≥ 0once the provedOneStepGoodScales.ae_errorRepresentative_le_goodEventDeltaSlotsupplies𝓔 ≤ C_cap s δ^{1/2}on the supply event. It is the printeds^{-1/2} δ^{1/2}ofe.excess.decay.one.stepread at the re-pins^{-4}. - The oscillation-to-excess fold (residue 2).
normalizedL2On_sub_average_truncatedWindow_leturns the anchor's leg-1 carrier‖u − (u)_{W}‖_{L²(W)}on a truncated windowW = (z+□_j) ∩ □_minto3^j · C_i(d) · (E(u,W) + |∇ℓ(u,W)|), by the proved endpoint comparison at the window's own aspect-1/9sandwich (SlopeStabilityEndpoints.endpoint_comparisons_of_axisCubeSandwich) and the proved normalizer comparison (AffineExcess.rpow_normalizer_bounds). TheeLpNorm-shaped version is the one the anchor's display literally carries. - The contraction absorption (residue 4).
exists_edBridgeStepproduces the step sizek₀(d): for everyk ≥ k₀,C_t(d) · C_sch(d) · κ(d,2) · κ(d,1) · (3^{-k})^{1/2} ≤ ½ · 3^{-(k+1)/4} ,κ(d,1) = windowRatioConst d 1being the price of the excess quasi-monotonicityE(u,U_{j-1}) ≤ κ(d,1) E(u,U_j)that residue 3 pays for the one-scale re-index.
References #
- ABK26,
l.excess.decay.good.scales, the printed one-step, the oscillation-to-excess comparison and the good-event cap;t.regularityStep 4.
1. The good-event cap fold #
** residue 1: the good-event cap fold.**
On the supply event the proved good-event cap
OneStepGoodScales.ae_errorRepresentative_le_goodEventDeltaSlot gives 𝓔 ≤ C_cap · s · δ^{1/2}. Substituting it into the anchor's leg prefactor C s^{-4} 𝓔 turns the whole leg into C · C_cap · s^{-3} · δ^{1/2} times its
(nonnegative) carrier — the printed 3^{(1+d/2)k} s^{-1/2} δ^{1/2} slot, at
the ε-re-pin's s^{-4}.
2. The oscillation-to-excess fold on a truncated window #
** residue 2, on the window carrier.** The volume-normalized oscillation of
u on a truncated window is controlled by the excess and the slope of any
affine minimizer there, at the proved endpoint constant C_i(d) = endpointConst d (1/9) of the aspect-1/9 sandwich.
** residue 2, on the anchor's own carrier.** The un-normalized mean-subtracted
L² norm — the anchor's leg-1 object — in terms of the excess and the slope:
‖u − (u)_{(z+□_j)∩□_m}‖_{L²((z+□_j)∩□_m)}
≤ 3^j · C_i(d) · ( E(u,(z+□_j)∩□_m) + |∇ℓ| ) .
The factor 3^j is the proved normalizer comparison |W|^{-1/d} ≥ 3^{-j} on
the window's own volume sandwich; no sharper aspect ratio than the printed
3^{-2} is used.
** residue 2, in the anchor's printed shape.** The same fold with the
left-hand side written as the toReal of an eLpNorm against the normalized
volume measure — the literal carrier of the anchor's leg 1.
3. The contraction absorption #
** residue 4: the contraction absorption.**
There is a step size k₀(d) ≥ 3 beyond which the one-step's contraction prefactor — including
the quasi-monotonicity price κ(d,1) that the one-scale re-index of residue 3 pays — is
absorbed into half of the iteration anchor's ratio θ^{k+1} = 3^{-(k+1)/4}. The remaining
half is what the good-event cap fold of residue 1 is gated against.