PrincipalComplementEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The complement-energy leg of the principal response, per grid cube #
The good-event display bounds the grid average of switchCubeEnergy against
the complement indicator of the per-cube bad event
principalBadEvent M Ccg R (m - h). This module supplies the other half: the
same grid average against the bad event itself.
Nothing here is common to all cubes. The envelope B, the load V and the
event all vary with the grid cube R, and the tail is the per-cube estimate of
exists_badEventEstimate_perCube_dimFloor_ofFrozen at the same
floor-normalized constant Cbase the good leg uses. That estimate is derived
from the frozen Algsuperdiff.Frozen.Section3.bad_event_estimate through the
scale-shift bridge, and it carries the union-bound factor 2, which is absorbed
here through the Hoelder power: (2 s) ^ (3/8) = 2 ^ (3/8) . s ^ (3/8), and
2 ^ (3/8) folds into the exported envelope constant C, which is enlarged to
2 ^ (3/8) . max C₀ Kgate. No binder and no public statement changes: the
enlargement only strengthens the premises the caller already supplies at C,
and the dimension-only gate Kgate ≤ E⁻² gamma⁻¹ of the frozen application is
derived here from the window premise
gamma / 2 + exp (-(C⁻¹ E⁻² gamma⁻¹)) ≤ gamma together with
gamma ≤ 1 / 1089.
Visibility #
Exactly one declaration of this module is visible outside it, the grid-average
endpoint
exists_const_descendantsAverage_integral_switchCubeEnergy_badEvent_le. Every
other declaration here stays private.
That endpoint returns the bad leg's per-cube integrability on the conclusion
side, alongside its estimate. The integrability is not a new hypothesis and
nothing new is proved for it: the Hoelder split already establishes
MemLp X (8/5) for the cube energy, and on this finite measure that membership
read at exponent one is exactly the integrability, which then rides the
conclusion chain outward through the per-cube estimate. A direct consumer needs
it to recombine the bad leg with the complement leg.
Elementary real bounds #
The scale gap and the oscillation rate both need t * logb 3 t⁻¹ to be small
for small t. The crude log y ≤ y - 1 is far too weak here (it only gives
t * logb 3 t⁻¹ ≤ (log 3)⁻¹, which the gap budget cannot absorb); applying it
at the square root instead gives a bound that vanishes with t. This is stated
over abstract reals, away from any rpow-laden goal.
The moment leg #
The cube-independent operator envelope #
The centred operator envelope B at the centred cube of a given scale: 2 (sigma⁻¹ Lambda_{s,q} + sigma lambda⁻¹_{s,q}).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two endpoint identifications, at independent domain and cutoff scales #
Promotion from the cube scale to the field scale #
Transport along the base-point translation #
The per-cube complement energy #
The grid average of the complement energy #
The bad-event leg at the grid average.
On a grid of depth-j triadic descendants of Q whose common scale Q.scale - j is the recurrence mesoscale, the discrete Cauchy--Schwarz step of
gridAverage_badEventEnergy_le turns the per-cube square roots of the previous
estimate into the square root of the grid average, which is the left-hand side
of the fourth-moment display. The tail is the same for every cube of the grid,
since every cube of the grid has the same scale.
Cv enters as the fourth root of the grid average of the load moment, a named
binder: nothing here estimates that average. The three well-definedness binders
are the per-cube ones of the previous estimate.
: this statement holds only under the propositions supplied by its binders.