LocalizationFluctuationSplitFoldArithmetic #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The regime arithmetic of the Step-2 annealed Hoelder fold #
The discrepancy this module settles #
ABK26 quotes the ellipticity moment of the annealed Hoelder fold as C cgamma^{-1}.
The proved producer
LocalizationFluctuationNumericEllipticity.
integral_gaugedEllipticitySum_pow_four_ancestorAtScale_le
delivers instead
E[ (gauged ellipticity sum)^4 ] <= ( C * cstar^{-1} * cgamma^{-1} )^4 ,
Since cstar is a property of the model and not an absolute constant, the
extra factor cannot simply be folded into the c1, c2 of
LocalizationFluctuationGammaFold.exists_gamma_threshold_holder_fold: those
must be uniform in the model, otherwise the produced gamma-threshold
would depend on M and the closure's ∀ M quantifier would be violated.
The resolution, and the exact cost #
The manuscript's own standing regime supplies the two facts that absorb it. At
one admissible pair (n, n+h) the closure reads
C * (cstar M)^{-1} <= E--- the largeness gate, at a thresholdCthe producer names (ClosureRegime's third clause), andcgamma <= E^{-5}--- the induction parameter's own smallness (ClosureRegime's fourth clause), with1 <= E.
Together, E <= cgamma^{-1/5} <= cgamma^{-1}, hence
C * cstar^{-1} * cgamma^{-1} <= E * cgamma^{-1} <= cgamma^{-2} .
So the ellipticity leg of the fold costs cgamma^{-2}, not the printed
cgamma^{-1}: exactly one extra power of cgamma. The fold's printed margin
is three powers (cgamma^{-1} * cgamma^{14} = cgamma^{13} against the target
cgamma^{10}), so one extra power is affordable, and the numerical obligation
moves from c1 cgamma^13 + c2 cgamma^27 <= cgamma^10 to
c1 cgamma^12 + c2 cgamma^24 <= cgamma^10 ,
which exists_gamma_threshold_regime_holder_fold discharges for every pair of
nonnegative absolute constants once cgamma is small. The absorption does
not fail; the only change is the pair of numerals, and both are still strictly
above 10.
gammaRegime_ellipticityLeg_pow_four_le records the same statement at the
fourth power, which is the shape the L^4 leg of
LocalizationFluctuationGammaFold.integral_mul_mul_le_L4_L4_L2 consumes.
The regime also supplies the ellipticity producer's own premises #
integral_gaugedEllipticitySum_pow_four_ancestorAtScale_le asks for max (exp (2 C)) (cstar M)^{-1} <= E and E <= cgamma^{-1/5}. Both come from the same
two regime clauses once the producer's threshold is chosen large enough:
gammaRegime_E_le_rpow_neg_fifth is the second, and gammaRegime_max_exp_le
is the first, using the proved absolute cap
Provider.Disorder.cstar_le_three_halves to convert the product gate C' cstar^{-1} <= E into the plain gate exp (2 C) <= E. The threshold
regimeEllipticityConst C produced here is the value a consumer must pass as
the Csplit of the split input.
Nothing below is a source display: this module is arithmetic, and it is deliberately separated from the fold assembly so that the numerals above can be verified on their own.
Binders #
Every statement is real arithmetic under the regime's own clauses (1 <= E, 0 < cgamma, the two gates) plus, where stated, the proved positivity and
absolute cap of cstar. No smallness gate is assumed: the two
gamma-thresholds are produced. Nothing about the corrector, the
coefficient field or the sample space occurs.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2,e.lower.bound.localization.terms,e.cg.ellip.upper,e.recurrence.params,e.cgamma.constraints.
The induction parameter under the regime's smallness clause #
E <= cgamma^{-1}. The crude form of the previous statement, which is
all the fold arithmetic needs.
Conditional on 1 <= E, 0 < cgamma and the regime's smallness clause.
The cstar^{-1} absorption #
The ellipticity leg of the fold costs cgamma^{-2}.
This is the exact statement whose failure would break the fold; it does not fail.
Conditional on 1 <= E, 0 < cgamma and the two regime gates.
The fourth power of the previous statement, in the shape the L^4 leg of
LocalizationFluctuationGammaFold.integral_mul_mul_le_L4_L4_L2 consumes:
E[ (gauged ellipticity sum)^4 ] <= ( C cstar^{-1} cgamma^{-1} )^4
<= ( cgamma^8 )^{-1} .
exactly as gammaRegime_ellipticityLeg_le, plus 0 <= C.
The numerical obligation #
The annealed Hoelder fold at the regime exponents.
ABK26 combines the ellipticity moment, the load moment C and the oscillation
moment C cgamma^{14}. With the ellipticity leg at cgamma^{-2}
(gammaRegime_ellipticityLeg_le) rather than the printed cgamma^{-1}, the
cross term is c1 cgamma^{12} and the quadratic term c2 cgamma^{24}; their
sum is below cgamma^{10} for every pair of nonnegative constants once
cgamma is small.
This is LocalizationFluctuationGammaFold.exists_gamma_threshold_holder_fold
with its numerals (13, 27) replaced by (12, 24); both are still strictly
above 10, which is the whole content. The threshold is produced, not
assumed.
The producer threshold the split input must name #
The threshold a consumer passes as the split input's own Csplit in order that
the regime's largeness gate imply the proved ellipticity producer's plain gate
exp (2 C) <= E. The factor 3/2 is the proved absolute cap
Provider.Disorder.cstar_le_three_halves.
Equations
Instances For
The regime's product gate implies the ellipticity producer's plain gate.
integral_gaugedEllipticitySum_pow_four_ancestorAtScale_le asks for max (exp (2 C)) cstar^{-1} <= E, while ClosureRegime supplies the product gate
Csplit cstar^{-1} <= E. With Csplit = regimeEllipticityConst C and the
proved absolute cap cstar <= 3/2 the two coincide: cstar^{-1} >= 2/3, so
the product gate already forces E >= (2/3) * (3/2) (exp (2 C) + 1) > exp (2 C), and cstar^{-1} <= E follows because regimeEllipticityConst C >= 1.
Conditional on the proved positivity and cap of cstar and on the gate.
The ellipticity producer's exponential gate #
The proved producer's fourth premise, cgamma / 2 + exp (-(C^{-1} (E^{-1})^2 cgamma^{-1})) <= cgamma, says that an exponentially small quantity sits below
cgamma / 2. Under the regime's smallness clause the exponent is at least
C^{-1} cgamma^{-1/2} --- because E^4 cgamma <= E^5 cgamma <= 1 forces
E^{-2} >= sqrt cgamma --- and exp t >= t^3 / 27, so the left-hand side is
O(cgamma^{3/2}). The gate therefore holds once cgamma is small, and the
threshold is produced.
The regime forces the ellipticity producer's exponential gate.
For every C > 0 there is a threshold below which, at every E >= 1 obeying the
regime's smallness clause cgamma <= E^{-5},
cgamma / 2 + exp (-(C^{-1} (E^{-1})^2 cgamma^{-1})) <= cgamma .
This is verbatim the fourth premise of
integral_gaugedEllipticitySum_pow_four_ancestorAtScale_le.
The threshold is produced, not assumed.
The ellipticity leg of the fold, under the regime alone #
The Step-2 ellipticity moment, with all four of the proved producer's premises replaced by the regime's own two clauses.
integral_gaugedEllipticitySum_pow_four_ancestorAtScale_le
carries four ad-hoc premises (the induction state, a max gate, an rpow
smallness bound and an exponential gate). Under the two clauses
Cell * cstar^{-1} <= E and cgamma <= E^{-5} of the closure's own regime, at
the produced threshold Cell and below a produced gamma0, all four hold,
and the resulting bound is the absolute (cgamma^8)^{-1}:
E[ (gauged ellipticity sum at the scale-m ancestor)^4 ] <= cgamma^{-8} .
Neither the producer's constant nor cstar survives. This is the ellipticity
leg of the annealed Hoelder fold, discharged.
Proved from the frozen theorem coarse_ellipticity_bounds, through its
producer.