BadEventScaleShiftBridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The scale-shift bridge from the frozen bad-event estimate to the dimension floor #
Algsuperdiff.Frozen.Section3.bad_event_estimate publishes only 1 ≤ Ccg about
its existential witness, while the Section 3.4 good half needs
(d : ℝ) ^ 6 ≤ Ccg at the same constant, and goodLocalEvent is not
monotone in that constant: its threshold
goodLocalThreshold M C m n = (1/2) * C⁻¹ * 3 ^ (-(1/2) * scaleGapPos m n) * sigmabar
is antitone in C, so the sensitivity clause tightens and the ellipticity
clause loosens as C grows. An earlier disclosure in this cone concluded from
this that no transfer exists. That conclusion was wrong, and this module
proves the transfer.
The mechanism #
The constant can be traded against the cube scale, because the oscillation
gauge is more strongly scale-weighted than the threshold. At a common centre
(cubeBasePoint (originCube d ell) = 0 for every ell),
cubeOscGauge (originCube d j) h
= max (3 ^ (2 j) * ‖∇²h‖_{L∞(cu_j)}) (3 ^ j * ‖∇h‖_{L∞(cu_j)}) ,
so enlarging the cube from scale m to mu multiplies the sup upwards but the
weights by 3 ^ (-2 (mu - m)) resp. 3 ^ (-(mu - m)), giving
cubeOscGauge_originCube_le_zpow_mul(L1):cubeOscGauge (originCube d m) h ≤ 3 ^ (m - mu) * cubeOscGauge (originCube d mu) h,
whereas the threshold only gains 3 ^ ((mu - m)/2). With mu = m + 2k the two
weights combine to an exact identity
goodLocalThreshold_scaleShift:3 ^ (m - (m + 2k)) * goodLocalThreshold M (2 C) (m + 2k) n = goodLocalThreshold M (2 * 3 ^ k * C) m n,
whence the two clause inclusions
goodLocalSensitivity_scaleShift_subset_le:Sens (2 C, cu_{m+2k}, n) ⊆ Sens (2 * 3 ^ k * C, cu_m, n);goodLocalEllipticity_const_mono:Elliponly grows with the constant;
and their combination
goodLocalEvent_inter_subset_scaleShift_le:good (2C, cu_m, n) ∩ good (2C, cu_{m+2k}, n) ⊆ good (2 * 3 ^ k * C, cu_m, n).
The dimension shift #
badEventScaleShiftExp d := 6 * d is dimension-only and elementary: d < 3 ^ d
gives (d : ℝ) ^ 6 ≤ 3 ^ (6 * d), which is all the floor (d : ℝ) ^ 6 ≤ Cbase
needs. No logarithm and no ceiling occurs.
Scope #
This module proves the geometric core of the bridge, verified in Lean. The
consuming step -- applying Algsuperdiff.Frozen.Section3.bad_event_estimate
twice at the same translate triadicCubeShift R, once at the cube scale
R.scale and once at R.scale + 2 * badEventScaleShiftExp d, and combining by
the union bound -- is proved in
Provider.Diffusivity.ApproximateRecurrence.BadEventFrozenApplication, which
is what the Section 3.4 bad-event leg consumes.
The clause inclusions are therefore stated in the full regime m ≤ n
(goodLocalThreshold_scaleShift_le, goodLocalSensitivity_scaleShift_subset_le,
goodLocalEvent_inter_subset_scaleShift_le), not only when the enlarged scale
m + 2 k still sits below n: the Section 3.4 grid is indexed by a free
recurrence multiplier and offers no headroom at its degenerate end, so the
consumer discharges the two frozen n < m gates on their own terms instead.
The exact threshold identity at the original gate m + 2 k ≤ n is kept as
goodLocalThreshold_scaleShift.
References #
- ABK26,
l.bad.event.lemma;e.good.local.events.
The gauge at an origin cube #
(L1) Cube-scale monotonicity of the oscillation gauge at a common centre.
Enlarging the origin cube from scale m to mu ≥ m gains the factor
3 ^ (m - mu) ≤ 1: the sup can only grow, but the gauge weights 3 ^ (2 j) and
3 ^ j grow strictly faster. This is the lemma that makes the constant of
e.good.local.events tradeable against the cube scale.
The threshold identity and the two clause inclusions #
The exact threshold identity behind the scale shift: the cube-scale gain of
the gauge and the loss of the threshold combine to the constant 3 ^ k.
The threshold scale shift as an inequality, in the full regime m ≤ n.
The exact identity of goodLocalThreshold_scaleShift needs the enlarged scale
m + 2 k to sit below the field scale n. When it does not, the enlarged
threshold saturates at its own gap 0 while the original one keeps the factor
3 ^ (-(1/2)(n - m)), and the shifted comparison survives as an inequality
because n - m ≤ 2 k on that branch. Only this inequality is used downstream,
so the bridge applies at every cube of the Section 3.4 grid, not only at those
with 2 k scales of headroom.
The scale shift on the sensitivity clause. Membership at the enlarged
cube and the small constant implies membership at the original cube and the
constant multiplied by 3 ^ k. Stated in the full regime m ≤ n, through
goodLocalThreshold_scaleShift_le.
The ellipticity clause only grows when the constant grows, because the threshold it lower-bounds is antitone in the constant.
The scale-shift bridge at the level of the good local event. The two
frozen-reachable events at the small constant, one at the cube scale and one at
the enlarged scale, together imply the event at the enlarged constant. Stated
in the full regime m ≤ n: no headroom between the enlarged scale and the field
scale is required.
The dimension-only scale shift #
The dimension-only scale shift: 3 ^ (6 d) clears the floor (d : ℝ) ^ 6
by the elementary d < 3 ^ d. No logarithm and no ceiling occurs.
Equations
Instances For
(d : ℝ) ^ 6 ≤ 3 ^ badEventScaleShiftExp d.